- 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);
-
- DPRINTF ( (message ("The body has the required cosntraints: %s", constraintList_printDetailed (t) ) ) );
- t = constraintList_mergeEnsures (c, body->ensuresConstraints);
-
- body->ensuresConstraints = constraintList_copy (t);
+ if (constraintList_isDefined(c))
+ {
+ DPRINTF ((message ("The Function %s has the preconditions %s",
+ uentry_unparse(ue), constraintList_unparseDetailed(c))));
+ }
+ else
+ {
+ DPRINTF((message ("The Function %s has no preconditions", uentry_unparse(ue))));
+ }
+
+ if (context_getFlag (FLG_IMPBOUNDSCONSTRAINTS))
+ {
+ constraintList implicitFcnConstraints = context_getImplicitFcnConstraints (ue);
+
+ if (constraintList_isDefined (implicitFcnConstraints))
+ {
+ DPRINTF (("Implicit constraints: %s", constraintList_unparse (implicitFcnConstraints)));
+
+ body->requiresConstraints = constraintList_reflectChangesFreePre (body->requiresConstraints,
+ implicitFcnConstraints);
+ constraintList_free (implicitFcnConstraints);
+ }
+ else
+ {
+ DPRINTF (("No implicit constraints"));
+ }
+ }
+
+ body->requiresConstraints = constraintList_sort (body->requiresConstraints);
+
+ constraintList_printError(body->requiresConstraints, g_currentloc);
+
+ post = uentry_getFcnPostconditions (ue);
+
+ if (context_getFlag (FLG_CHECKPOST))
+ {
+ if (constraintList_isDefined (post))
+ {
+ constraintList post2;
+
+ DPRINTF ((message ("The declared function postconditions are %s \n\n\n\n\n",
+ constraintList_unparseDetailed (post) ) ) );
+
+ post = constraintList_reflectChangesFreePre (post, body->ensuresConstraints);
+
+ post2 = constraintList_copy (post);
+ fix = constraintList_makeFixedArrayConstraints (body->uses);
+ post2 = constraintList_reflectChangesFreePre (post2, fix);
+ constraintList_free(fix);
+ if ( context_getFlag (FLG_ORCONSTRAINT) )
+ {
+ t = constraintList_reflectChangesOr (post2, body->ensuresConstraints);
+ }
+ else
+ {
+ t = constraintList_reflectChanges(post2, body->ensuresConstraints);
+ }
+
+ constraintList_free(post2);
+ constraintList_free(post);
+ post = t;
+
+ printf("Unresolved post conditions\n");
+ constraintList_printErrorPostConditions(post, g_currentloc);
+ }
+ }
+
+ if (constraintList_isDefined (post))
+ {
+ constraintList_free (post);
+ }