}
}
}
+
+ exprNode_checkFunction (context_getHeader (), body);
if (!checkret)
{
}
}
}
+/*drl modified */
void exprNode_checkFunction (/*@unused@*/ uentry ue, /*@only@*/ exprNode body)
{
constraintList c, t;
+ constraintList c2, fix;
-
- // return;
+ // return;
exprNode_generateConstraints (body);
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) );
+
+ t = reflectChanges (body->requiresConstraints, constraintList_copy (c2) );
+ body->requiresConstraints = constraintList_copy (t);
DPRINTF ( (message ("The body has the required cosntraints: %s", constraintList_printDetailed (t) ) ) );
- t = constraintList_mergeEnsures (c, body->ensuresConstraints);
+ t = constraintList_mergeEnsures (c, body->ensuresConstraints);
body->ensuresConstraints = constraintList_copy (t);
DPRINTF((message ("The Function %s has no preconditions", uentry_unparse(ue) ) ) );
}
- ConPrint (message ("Unable to resolve function constraints:\n%s", constraintList_printDetailed(body->requiresConstraints) ), g_currentloc);
+ 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);
+ // 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) );