+ llassert (exprNode_isDefined (body));
+
+ DPRINTF (("Checking body: %s", exprNode_unparse (body)));
+
+ /*
+ if we're not going to be printing any errors for buffer overflows
+ we can skip the checking to improve performance
+
+ FLG_DEBUGFUNCTIONCONSTRAINT controls wheather we perform the check anyway
+ in order to find potential problems like assert failures and seg faults...
+ */
+
+ if (!(context_getFlag (FLG_DEBUGFUNCTIONCONSTRAINT)
+ || context_getFlag (FLG_BOUNDSWRITE)
+ || context_getFlag (FLG_BOUNDSREAD)
+ || context_getFlag (FLG_LIKELYBOUNDSWRITE)
+ || context_getFlag (FLG_LIKELYBOUNDSREAD)
+ || context_getFlag (FLG_CHECKPOST)
+ || context_getFlag (FLG_ALLOCMISMATCH)))
+ {
+ exprNode_free (body);
+ context_exitInnerPlain();
+ return;
+ }
+
+ exprNode_generateConstraints (body); /* evans 2002-03-02: this should not be declared to take a
+ dependent... fix it! */
+
+ c = uentry_getFcnPreconditions (ue);
+
+ if (constraintList_isDefined (c))
+ {
+ DPRINTF (("Function preconditions are %s", constraintList_unparseDetailed (c)));
+
+ body->requiresConstraints =
+ constraintList_reflectChangesFreePre (body->requiresConstraints, c);
+
+ c2 = constraintList_copy (c);
+ fix = constraintList_makeFixedArrayConstraints (body->uses);
+ c2 = constraintList_reflectChangesFreePre (c2, fix);