/* #define DEBUGPRINT 1 */
-# include <ctype.h> /* for isdigit */
# include "splintMacros.nf"
# include "basic.h"
# include "cgrammar.h"
# include "cgrammar_tokens.h"
-
# include "exprChecks.h"
# include "exprNodeSList.h"
-
-static /*@only@*/ cstring constraint_unparseDetailedPostCondition (/*@observer@*/ /*@temp@*/ constraint p_c);
+static /*@only@*/ cstring
+constraint_unparseDetailedPostCondition (/*@observer@*/ /*@temp@*/ constraint p_c);
static /*@notnull@*/ /*@special@*/ constraint constraint_makeNew (void)
/*@post:isnull result->or, result->orig, result->generatingExpr, result->fcnPre @*/
reader_checkChar (s, '@');
}
-# if 0
-static constraint makeConstraintParse2 (constraintExpr l, lltok relOp, exprNode cconstant)
-{
- char *t;
- int c;
- constraint ret;
- ret = constraint_makeNew ();
- llassert (constraintExpr_isDefined (l));
-
- ret->lexpr = constraintExpr_copy (l);
-
-
- if (relOp.tok == GE_OP)
- ret->ar = GTE;
- else if (relOp.tok == LE_OP)
- ret->ar = LTE;
- else if (relOp.tok == EQ_OP)
- ret->ar = EQ;
- else
- llfatalbug (message ("Unsupported relational operator"));
-
-
- t = cstring_toCharsSafe (exprNode_unparse (cconstant));
- c = atoi ( t);
- ret->expr = constraintExpr_makeIntLiteral (c);
-
- ret->post = TRUE;
- DPRINTF (("GENERATED CONSTRAINT:"));
- DPRINTF ((message ("%s", constraint_unparse (ret))));
- return ret;
-}
-# endif
-
bool constraint_same (constraint c1, constraint c2)
{
llassert (c1 != NULL);
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@*/
-
- /*@i33 fix this*/
- 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 expect it doesn't allocate memory for the constraint*/
+/*like copy except it doesn't allocate memory for the constraint*/
void constraint_overWrite (constraint c1, constraint c2)
{
else
c1->orig = NULL;
- /*@i33 make sure that the or is freed correctly*/
if (c1->or != NULL)
constraint_free (c1->or);
constraint constraint_addGeneratingExpr (/*@returned@*/ constraint c, /*@exposed@*/ exprNode e)
{
-
- llassert (constraint_isDefined (c) );
+ if (!constraint_isDefined (c))
+ {
+ return c;
+ }
if (c->generatingExpr == NULL)
{
fileloc constraint_getFileloc (constraint c)
{
-
llassert (constraint_isDefined (c) );
if (exprNode_isDefined (c->generatingExpr))
- return (fileloc_copy (exprNode_getfileloc (c->generatingExpr)));
+ return (fileloc_copy (exprNode_loc (c->generatingExpr)));
- return (constraintExpr_getFileloc (c->lexpr));
-
-
+ return (constraintExpr_loc (c->lexpr));
}
static bool checkForMaxSet (constraint c)
-{
-
- llassert (constraint_isDefined (c) );
-
- if (constraintExpr_hasMaxSet (c->lexpr) || constraintExpr_hasMaxSet (c->expr))
- return TRUE;
-
- return FALSE;
+{
+ llassert (constraint_isDefined (c));
+ return (constraintExpr_hasMaxSet (c->lexpr) || constraintExpr_hasMaxSet (c->expr));
}
bool constraint_hasMaxSet (constraint c)
{
-
llassert (constraint_isDefined (c) );
if (checkForMaxSet (c))
po = po;
ind = ind;
ret->lexpr = constraintExpr_makeMaxReadExpr (po);
- ret->ar = GTE;
- ret->expr = constraintExpr_makeValueExpr (ind);
+ ret->ar = GTE;
+ ret->expr = constraintExpr_makeValueExpr (ind);
ret->post = FALSE;
return ret;
}
-constraint constraint_makeWriteSafeInt ( exprNode po, int ind)
+constraint constraint_makeWriteSafeInt (exprNode po, int ind)
{
constraint ret = constraint_makeNew ();
-
-
ret->lexpr =constraintExpr_makeMaxSetExpr (po);
ret->ar = GTE;
ret->expr = constraintExpr_makeIntLiteral (ind);
- /*@i1*/return ret;
+ /*@i1*/ return ret;
}
constraint constraint_makeSRefSetBufferSize (sRef s, long int size)
{
- constraint ret = constraint_makeNew ();
- ret->lexpr = constraintExpr_makeSRefMaxset (s);
- ret->ar = EQ;
- ret->expr = constraintExpr_makeIntLiteral ((int)size);
- ret->post = TRUE;
- /*@i1*/
- return ret;
+ constraint ret = constraint_makeNew ();
+ ret->lexpr = constraintExpr_makeSRefMaxset (s);
+ ret->ar = EQ;
+ ret->expr = constraintExpr_makeIntLiteral ((int)size);
+ ret->post = TRUE;
+ return ret;
}
constraint constraint_makeSRefWriteSafeInt (sRef s, int ind)
{
constraint ret = constraint_makeNew ();
-
-
ret->lexpr = constraintExpr_makeSRefMaxset ( s);
ret->ar = GTE;
- ret->expr = constraintExpr_makeIntLiteral (ind);
+ ret->expr = constraintExpr_makeIntLiteral (ind);
ret->post = TRUE;
- /*@i1*/
return ret;
}
/* drl added 01/12/2000
-
- makes the constraint: Ensures index <= MaxRead (buffer) */
+** makes the constraint: Ensures index <= MaxRead (buffer)
+*/
constraint constraint_makeEnsureLteMaxRead (exprNode index, exprNode buffer)
{
constraint constraint_makeWriteSafeExprNode (exprNode po, exprNode ind)
{
constraint ret = constraint_makeNew ();
-
ret->lexpr =constraintExpr_makeMaxSetExpr (po);
ret->ar = GTE;
}
-constraint constraint_makeReadSafeInt ( exprNode t1, int index)
+constraint constraint_makeReadSafeInt (exprNode t1, int index)
{
constraint ret = constraint_makeNew ();
ret->lexpr = constraintExpr_makeMaxReadExpr (t1);
- ret->ar = GTE;
- ret->expr = constraintExpr_makeIntLiteral (index);
+ ret->ar = GTE;
+ ret->expr = constraintExpr_makeIntLiteral (index);
ret->post = FALSE;
return ret;
}
constraint constraint_makeSRefReadSafeInt (sRef s, int ind)
{
constraint ret = constraint_makeNew ();
-
-
+
ret->lexpr = constraintExpr_makeSRefMaxRead (s);
ret->ar = GTE;
ret->expr = constraintExpr_makeIntLiteral (ind);
constraint constraint_makeEnsureMaxReadAtLeast (exprNode t1, exprNode t2, fileloc sequencePoint)
{
- constraint ret;
-
- ret = constraint_makeReadSafeExprNode (t1, t2);
- llassert (constraint_isDefined (ret) );
+ constraint ret = constraint_makeReadSafeExprNode (t1, t2);
+ llassert (constraint_isDefined (ret));
ret->lexpr = constraintExpr_setFileloc (ret->lexpr, sequencePoint);
ret->post = TRUE;
return ret;
}
-static constraint constraint_makeEnsuresOpConstraintExpr (/*@only@*/ constraintExpr c1, /*@only@*/ constraintExpr c2, fileloc sequencePoint, arithType ar)
+static constraint
+constraint_makeEnsuresOpConstraintExpr (/*@only@*/ constraintExpr c1, /*@only@*/ constraintExpr c2,
+ fileloc sequencePoint, arithType ar)
{
-
- constraint ret;
-
- llassert (constraintExpr_isDefined (c1) && constraintExpr_isDefined (c2));
-
- ret = constraint_makeNew ();
-
- 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_makeEnsuresOp (/*@dependent@*/ exprNode e1, /*@dependent@*/ exprNode e2, fileloc sequencePoint, arithType ar)
+static constraint
+constraint_makeEnsuresOp (/*@dependent@*/ exprNode e1, /*@dependent@*/ exprNode e2,
+ fileloc sequencePoint, arithType ar)
{
constraintExpr c1, c2;
- constraint ret;
- exprNode e;
-
- if (! (exprNode_isDefined (e1) && exprNode_isDefined (e2)))
+
+ if (!(exprNode_isDefined (e1) && exprNode_isDefined (e2)))
{
- llcontbug ((message ("null exprNode, Exprnodes are %s and %s",
- exprNode_unparse (e1), exprNode_unparse (e2))
- ));
+ llcontbug (message ("Invalid exprNode, Exprnodes are %s and %s",
+ exprNode_unparse (e1), exprNode_unparse (e2)));
}
-
- e = e1;
- c1 = constraintExpr_makeValueExpr (e);
- e = e2;
- c2 = constraintExpr_makeValueExpr (e);
+ c1 = constraintExpr_makeValueExpr (e1);
+ c2 = constraintExpr_makeValueExpr (e2);
- ret = constraint_makeEnsuresOpConstraintExpr (c1, c2, sequencePoint, ar);
-
- return ret;
+ return constraint_makeEnsuresOpConstraintExpr (c1, c2, sequencePoint, ar);
}
-
/* make constraint ensures e1 == e2 */
constraint constraint_makeEnsureEqual (exprNode e1, exprNode e2, fileloc sequencePoint)
{
- return ( constraint_makeEnsuresOp (e1, e2, sequencePoint, EQ));
+ return (constraint_makeEnsuresOp (e1, e2, sequencePoint, EQ));
}
-/*make constraint ensures e1 < e2 */
+/* make constraint ensures e1 < e2 */
constraint constraint_makeEnsureLessThan (exprNode e1, exprNode e2, fileloc sequencePoint)
{
constraintExpr t1, t2;
t1 = constraintExpr_makeValueExpr (e1);
t2 = constraintExpr_makeValueExpr (e2);
- /*change this to e1 <= (e2 -1) */
+ /* change this to e1 <= (e2 -1) */
t2 = constraintExpr_makeDecConstraintExpr (t2);
-
- t3 = constraint_makeEnsuresOpConstraintExpr (t1, t2, sequencePoint, LTE);
-
- t3 = constraint_simplify(t3);
+ t3 = constraint_makeEnsuresOpConstraintExpr (t1, t2, sequencePoint, LTE);
+ t3 = constraint_simplify (t3);
return (t3);
}
constraint constraint_makeEnsureLessThanEqual (exprNode e1, exprNode e2, fileloc sequencePoint)
{
- return ( constraint_makeEnsuresOp (e1, e2, sequencePoint, LTE));
+ return (constraint_makeEnsuresOp (e1, e2, sequencePoint, LTE));
}
constraint constraint_makeEnsureGreaterThan (exprNode e1, exprNode e2, fileloc sequencePoint)
t1 = constraintExpr_makeValueExpr (e1);
t2 = constraintExpr_makeValueExpr (e2);
-
/* change this to e1 >= (e2 + 1) */
t2 = constraintExpr_makeIncConstraintExpr (t2);
t3 = constraint_makeEnsuresOpConstraintExpr (t1, t2, sequencePoint, GTE);
-
t3 = constraint_simplify(t3);
return t3;
void constraint_free (/*@only@*/ constraint c)
{
- llassert (constraint_isDefined (c));
-
+ if (constraint_isDefined (c))
+ {
+ constraint_free (c->orig);
+ c->orig = NULL;
- if (constraint_isDefined (c->orig))
- constraint_free (c->orig);
- if ( constraint_isDefined (c->or))
- constraint_free (c->or);
+ constraint_free (c->or);
+ c->or = NULL;
-
- constraintExpr_free (c->lexpr);
- constraintExpr_free (c->expr);
+ constraintExpr_free (c->lexpr);
+ c->lexpr = NULL;
- c->orig = NULL;
- c->or = NULL;
- c->lexpr = NULL;
- c->expr = NULL;
-
- free (c);
-
+ constraintExpr_free (c->expr);
+ c->expr = NULL;
+
+ free (c);
+ }
}
cstring arithType_print (arithType ar) /*@*/
case LT:
st = cstring_makeLiteral ("<");
break;
- case LTE:
+ case LTE:
st = cstring_makeLiteral ("<=");
break;
- case GT:
+ case GT:
st = cstring_makeLiteral (">");
break;
- case GTE:
+ case GTE:
st = cstring_makeLiteral (">=");
break;
- case EQ:
+ case EQ:
st = cstring_makeLiteral ("==");
break;
- case NONNEGATIVE:
+ case NONNEGATIVE:
st = cstring_makeLiteral ("NONNEGATIVE");
break;
- case POSITIVE:
+ case POSITIVE:
st = cstring_makeLiteral ("POSITIVE");
break;
default:
fileloc errorLoc, temp;
string = constraint_unparseDetailedPostCondition (c);
-
errorLoc = loc;
-
loc = NULL;
temp = constraint_getFileloc (c);
-
- if (context_getFlag (FLG_BOUNDSCOMPACTERRORMESSAGES ) )
+ if (context_getFlag (FLG_BOUNDSCOMPACTERRORMESSAGES))
{
- string = cstring_replaceChar(string, '\n', ' ');
+ string = cstring_replaceChar (string, '\n', ' ');
}
if (fileloc_isDefined (temp))
{
errorLoc = temp;
- voptgenerror ( FLG_CHECKPOST, string, errorLoc);
+ voptgenerror (FLG_CHECKPOST, string, errorLoc);
fileloc_free (temp);
}
else
{
- voptgenerror ( FLG_CHECKPOST, string, errorLoc);
+ voptgenerror (FLG_CHECKPOST, string, errorLoc);
}
}
errorLoc = constraint_getFileloc (c);
ret = message ("constraint: %q @ %q", string, fileloc_unparse (errorLoc));
-
fileloc_free (errorLoc);
return ret;
fileloc errorLoc, temp;
bool isLikely;
-
llassert (constraint_isDefined (c) );
else
{
llassert (FALSE);
- DPRINTF (("constraint %s had undefined fileloc %s", constraint_unparse (c), fileloc_unparse (temp)));
+ DPRINTF (("constraint %s had undefined fileloc %s",
+ constraint_unparse (c), fileloc_unparse (temp)));
fileloc_free (temp);
errorLoc = fileloc_copy (errorLoc);
}
- if (context_getFlag (FLG_BOUNDSCOMPACTERRORMESSAGES ) )
+ if (context_getFlag (FLG_BOUNDSCOMPACTERRORMESSAGES))
{
string = cstring_replaceChar(string, '\n', ' ');
}
/*drl added 12/19/2002 print
a different error fro "likely" bounds-errors*/
- isLikely = constraint_isConstantOnly(c);
+ isLikely = constraint_isConstantOnly (c);
if (isLikely)
{
else
{
st = cstring_concatFree (st, message ("derived from: %q",
- constraint_unparseDeep (c->orig)));
+ constraint_unparseDeep (c->orig)));
}
}
cstring temp;
temp = message ("\nOriginal Generating expression %q: %s\n",
- fileloc_unparse ( exprNode_getfileloc (c->generatingExpr)),
+ fileloc_unparse (exprNode_loc (c->generatingExpr)),
genExpr);
st = cstring_concatFree (st, temp);
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: ");
}
}
return st;
}
-/*@only@*/ cstring constraint_unparse (constraint c) /*@*/
+/*@only@*/ cstring constraint_unparse (constraint c) /*@*/
{
cstring st = cstring_undefined;
cstring type = cstring_undefined;
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)
- {
- c->orig = constraint_copy (c);
- }
- else if (c->orig->fcnPre)
+ if (constraint_isDefined (c))
{
- constraint temp = c->orig;
+ DPRINTF (("Doing constraint_preserverOrig for %q", constraint_printLocation (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->orig = temp;
- temp = NULL;
+ c->orig = constraint_copy (c);
+ }
+ else if (c->orig->fcnPre)
+ {
+ 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;
}
andersk / splint.git / blobdiff