constraint constraint_copy (/*@temp@*/ /*@observer@*/ constraint c)
{
- constraint ret;
-
- llassert (constraint_isDefined (c));
-
- ret = constraint_makeNew ();
- ret->lexpr = constraintExpr_copy (c->lexpr);
- ret->ar = c->ar;
- ret->expr = constraintExpr_copy (c->expr);
- ret->post = c->post;
- /*@-assignexpose@*/
- ret->generatingExpr = c->generatingExpr;
- /*@=assignexpose@*/
-
- if (c->orig != NULL)
- ret->orig = constraint_copy (c->orig);
- else
- ret->orig = NULL;
-
- if (c->or != NULL)
- ret->or = constraint_copy (c->or);
+ if (!constraint_isDefined (c))
+ {
+ return constraint_undefined;
+ }
else
- ret->or = NULL;
-
- ret->fcnPre = c->fcnPre;
-
- return ret;
+ {
+ constraint ret = constraint_makeNew ();
+ ret->lexpr = constraintExpr_copy (c->lexpr);
+ ret->ar = c->ar;
+ ret->expr = constraintExpr_copy (c->expr);
+ ret->post = c->post;
+ /*@-assignexpose@*/
+ ret->generatingExpr = c->generatingExpr;
+ /*@=assignexpose@*/
+
+ if (c->orig != NULL)
+ ret->orig = constraint_copy (c->orig);
+ else
+ ret->orig = NULL;
+
+ if (c->or != NULL)
+ ret->or = constraint_copy (c->or);
+ else
+ ret->or = NULL;
+
+ ret->fcnPre = c->fcnPre;
+
+ return ret;
+ }
}
/*like copy except it doesn't allocate memory for the constraint*/
constraint constraint_addGeneratingExpr (/*@returned@*/ constraint c, /*@exposed@*/ exprNode e)
{
-
- llassert (constraint_isDefined (c) );
+ if (!constraint_isDefined (c))
+ {
+ return c;
+ }
if (c->generatingExpr == NULL)
{
constraint_makeEnsuresOpConstraintExpr (/*@only@*/ constraintExpr c1, /*@only@*/ constraintExpr c2,
fileloc sequencePoint, arithType ar)
{
- constraint ret = constraint_makeNew ();
- llassert (constraintExpr_isDefined (c1) && constraintExpr_isDefined (c2));
- ret->lexpr = c1;
- ret->ar = ar;
- ret->post = TRUE;
- ret->expr = c2;
- ret->lexpr = constraintExpr_setFileloc (ret->lexpr, sequencePoint);
- return ret;
+ if (constraintExpr_isDefined (c1) && constraintExpr_isDefined (c2))
+ {
+ constraint ret = constraint_makeNew ();
+ ret->lexpr = c1;
+ ret->ar = ar;
+ ret->post = TRUE;
+ ret->expr = c2;
+ ret->lexpr = constraintExpr_setFileloc (ret->lexpr, sequencePoint);
+ return ret;
+ }
+ else
+ {
+ return constraint_undefined;
+ }
}
static constraint
constraint constraint_makeEnsureEqual (exprNode e1, exprNode e2, fileloc sequencePoint)
{
- if (FALSE) /* (!ctype_almostEqual (exprNode_getType (e1), exprNode_getType (e2))) */
- {
- /* If the types are not identical, need to be careful the element sizes may be different. */
- //! return (constraint_makeEnsuresOp (e1, e2, sequencePoint, CASTEQ));
- BADBRANCH;
- }
- else
- {
- return (constraint_makeEnsuresOp (e1, e2, sequencePoint, EQ));
- }
+ return (constraint_makeEnsuresOp (e1, e2, sequencePoint, EQ));
}
/* make constraint ensures e1 < e2 */
void constraint_free (/*@only@*/ constraint c)
{
- llassert (constraint_isDefined (c));
-
-
- if (constraint_isDefined (c->orig))
- constraint_free (c->orig);
- if ( constraint_isDefined (c->or))
- constraint_free (c->or);
+ if (constraint_isDefined (c))
+ {
+ constraint_free (c->orig);
+ c->orig = NULL;
-
- constraintExpr_free (c->lexpr);
- constraintExpr_free (c->expr);
+ constraint_free (c->or);
+ c->or = NULL;
- c->orig = NULL;
- c->or = NULL;
- c->lexpr = NULL;
- c->expr = NULL;
+ constraintExpr_free (c->lexpr);
+ c->lexpr = NULL;
- free (c);
-
+ constraintExpr_free (c->expr);
+ c->expr = NULL;
+
+ free (c);
+ }
}
cstring arithType_print (arithType ar) /*@*/
case EQ:
st = cstring_makeLiteral ("==");
break;
- case CASTEQ:
- st = cstring_makeLiteral ("(!)==");
- break;
case NONNEGATIVE:
st = cstring_makeLiteral ("NONNEGATIVE");
break;
cstring genExpr;
bool isLikely;
- llassert (constraint_isDefined (c) );
+ llassert (constraint_isDefined (c));
if (!c->post)
{
st = message ("Block Post condition:\nThis function block has the post condition %q", constraint_unparseDeep (c));
}
- isLikely = constraint_isConstantOnly(c);
+ isLikely = constraint_isConstantOnly (c);
if (isLikely)
{
if (constraint_hasMaxSet (c))
{
- temp = cstring_makeLiteral ("Likely out-of-bounds store:\n");
+ temp = cstring_makeLiteral ("Likely out-of-bounds store: ");
}
else
{
- temp = cstring_makeLiteral ("Likely out-of-bounds read:\n");
+ temp = cstring_makeLiteral ("Likely out-of-bounds read: ");
}
}
else
if (constraint_hasMaxSet (c))
{
- temp = cstring_makeLiteral ("Possible out-of-bounds store:\n");
+ temp = cstring_makeLiteral ("Possible out-of-bounds store: ");
}
else
{
- temp = cstring_makeLiteral ("Possible out-of-bounds read:\n");
+ temp = cstring_makeLiteral ("Possible out-of-bounds read: ");
}
}
constraint constraint_preserveOrig (/*@returned@*/ constraint c) /*@modifies c @*/
{
- DPRINTF (("Doing constraint_preserverOrig for %q", constraint_printDetailed (c)));
- llassert (constraint_isDefined (c));
-
- if (c->orig == constraint_undefined)
+ if (constraint_isDefined (c))
{
- c->orig = constraint_copy (c);
- }
- else if (c->orig->fcnPre)
- {
- constraint temp = c->orig;
+ DPRINTF (("Doing constraint_preserverOrig for %q", constraint_printDetailed (c)));
- /* avoid infinite loop */
- c->orig = NULL;
- c->orig = constraint_copy (c);
- /*drl 03/2/2003 if c != NULL then the copy of c will != null*/
- llassert (constraint_isDefined (c->orig) );
-
- if (c->orig->orig == NULL)
+ if (c->orig == constraint_undefined)
+ {
+ c->orig = constraint_copy (c);
+ }
+ else if (c->orig->fcnPre)
{
- c->orig->orig = temp;
- temp = NULL;
+ constraint temp = c->orig;
+
+ /* avoid infinite loop */
+ c->orig = NULL;
+ c->orig = constraint_copy (c);
+ /*drl 03/2/2003 if c != NULL then the copy of c will != null*/
+ llassert (constraint_isDefined (c->orig) );
+
+ if (c->orig->orig == NULL)
+ {
+ c->orig->orig = temp;
+ temp = NULL;
+ }
+ else
+ {
+ llcontbug ((message ("Expected c->orig->orig to be null")));
+ constraint_free (c->orig->orig);
+ c->orig->orig = temp;
+ temp = NULL;
+ }
}
else
{
- llcontbug ((message ("Expected c->orig->orig to be null")));
- constraint_free (c->orig->orig);
- c->orig->orig = temp;
- temp = NULL;
+ DPRINTF (("Not changing constraint"));
}
}
- else
- {
- DPRINTF (("Not changing constraint"));
- }
-
+
DPRINTF ((message ("After Doing constraint_preserverOrig for %q ", constraint_unparseDetailed (c))));
return c;
}