+
+
+ post = uentry_getFcnPostconditions (ue);
+
+ if ( context_getFlag (FLG_CHECKPOST) )
+ {
+ if (post)
+ {
+
+ constraintList post2;
+
+ DPRINTF ( (message ("The declared function postconditions are %s \n\n\n\n\n", constraintList_printDetailed (post) ) ) );
+
+ post = reflectChangesFreePre (post, body->ensuresConstraints);
+
+ post2 = constraintList_copy (post);
+ fix = constraintList_makeFixedArrayConstraints (body->uses);
+ post2 = reflectChangesFreePre (post2, fix);
+ constraintList_free(fix);
+ if ( context_getFlag (FLG_ORCONSTRAINT) )
+ {
+ t = reflectChangesOr (post2, body->ensuresConstraints);
+ }
+ else
+ {
+ t = reflectChanges (post2, body->ensuresConstraints);
+ }
+
+ constraintList_free(post2);
+
+ constraintList_free(post);
+ post = t;
+
+
+
+ printf("Unresolved post conditions\n");
+ constraintList_printErrorPostConditions(post, g_currentloc);
+ }
+ }
+
+ if (post)
+ constraintList_free(post);
+
+