}
}
}
+
+ /* drl added call*/
+ exprNode_checkFunction (context_getHeader (), body);
if (!checkret)
{
}
}
}
-
+/*drl modified */
+
+extern constraintList implicitFcnConstraints;
+
void exprNode_checkFunction (/*@unused@*/ uentry ue, /*@only@*/ exprNode body)
{
- /* drl added 8-8-2000 */
+ constraintList c, t;
+ constraintList c2, fix;
+
+ // return;
+
+ // context_setFlag(FLG_ORCONSTRAINT, TRUE);
exprNode_generateConstraints (body);
+
+ c = uentry_getFcnPreconditions (ue);
DPRINTF(("function constraints\n"));
- // constraintList_print (body->constraints);
- DPRINTF (("----\n"));
- // constraintList_resolve (body->constraints);
- exprNode_free (body);
-
- }
+ DPRINTF (("\n\n\n\n\n\n\n"));
+
+ context_enterInnerContext ();
+
+ if (c)
+ {
+ llassert (c);
+ DPRINTF ( (message ("Function preconditions are %s \n\n\n\n\n", constraintList_printDetailed (c) ) ) );
+
+ t = reflectChanges (body->requiresConstraints, constraintList_copy (c) );
+ body->requiresConstraints = constraintList_copy (t);
+
+ c2 = constraintList_copy (c);
+ fix = constraintList_makeFixedArrayConstraints (body->uses);
+ c2 = reflectChanges (c2, constraintList_copy(fix) );
+ if ( context_getFlag (FLG_ORCONSTRAINT) )
+ {
+ t = reflectChangesOr (body->requiresConstraints, constraintList_copy (c2) );
+ }
+ else
+ {
+ t = reflectChanges (body->requiresConstraints, constraintList_copy (c2) );
+ }
+ body->requiresConstraints = constraintList_copy (t);
+
+ DPRINTF ( (message ("The body has the required constraints: %s", constraintList_printDetailed (t) ) ) );
+ t = constraintList_mergeEnsures (c, body->ensuresConstraints);
+
+ body->ensuresConstraints = constraintList_copy (t);
+
+ DPRINTF ( (message ("The body has the ensures constraints: %s", constraintList_printDetailed (t) ) ) );
+ }
+
+ if (c)
+ {
+ DPRINTF((message ("The Function %s has the preconditions %s", uentry_unparse(ue), constraintList_printDetailed(c) ) ) );
+ }
+ else
+ {
+ DPRINTF((message ("The Function %s has no preconditions", uentry_unparse(ue) ) ) );
+ }
+
+ if ( implicitFcnConstraints)
+ {
+ if (context_getFlag (FLG_IMPLICTCONSTRAINT) )
+ {
+ body->requiresConstraints = reflectChanges (body->requiresConstraints, constraintList_copy (implicitFcnConstraints) );
+ }
+ }
+
+ constraintList_printError(body->requiresConstraints, g_currentloc);
+ constraintList_printError(body->ensuresConstraints, g_currentloc);
+
+ // ConPrint (message ("Unable to resolve function constraints:\n%s", constraintList_printDetailed(body->requiresConstraints) ), g_currentloc);
+
+ // ConPrint (message ("LCLint has found function post conditions:\n%s", constraintList_printDetailed(body->ensuresConstraints) ), g_currentloc);
+
+ // printf ("The required constraints are:\n%s", constraintList_printDetailed(body->requiresConstraints) );
+ // printf ("The ensures constraints are:\n%s", constraintList_printDetailed(body->ensuresConstraints) );
+
+ context_exitInnerPlain();
+ /* exprNode_free (body); */
+}
void exprChecks_checkEmptyMacroBody (void)
{