/*
** Splint - annotation-assisted static program checker
-** Copyright (C) 1994-2002 University of Virginia,
+** Copyright (C) 1994-2003 University of Virginia,
** Massachusetts Institute of Technology
**
** This program is free software; you can redistribute it and/or modify it
# include "exprChecks.h"
# include "exprNodeSList.h"
-/*@i33*/
-
-/*@access exprNode@*/ /* !!! NO! Don't do this recklessly! */
-/*@-nullderef@*/ /* !!! DRL needs to fix this code! */
-/*@-nullstate@*/ /* !!! DRL needs to fix this code! */
-/*@-temptrans@*/ /* !!! DRL needs to fix this code! */
-
-static /*@only@*/ cstring constraint_printDetailedPostCondition (/*@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 @*/
ret->post = TRUE;
DPRINTF (("GENERATED CONSTRAINT:"));
- DPRINTF ((message ("%s", constraint_print (ret))));
+ DPRINTF ((message ("%s", constraint_unparse (ret))));
return ret;
}
# endif
/* ret->orig = ret; */
DPRINTF (("GENERATED CONSTRAINT:"));
- DPRINTF ((message ("%s", constraint_print (ret))));
+ DPRINTF ((message ("%s", constraint_unparse (ret))));
return ret;
}
void constraint_overWrite (constraint c1, constraint c2)
{
- llassert (constraint_isDefined (c1));
+ llassert (constraint_isDefined (c1) && constraint_isDefined (c2));
llassert (c1 != c2);
- DPRINTF ((message ("OverWriteing constraint %q with %q", constraint_print (c1),
- constraint_print (c2))));
+ DPRINTF ((message ("OverWriteing constraint %q with %q", constraint_unparse (c1),
+ constraint_unparse (c2))));
constraintExpr_free (c1->lexpr);
constraintExpr_free (c1->expr);
return ret;
}
+/*@access exprNode@*/
+
constraint constraint_addGeneratingExpr (/*@returned@*/ constraint c, /*@exposed@*/ exprNode e)
{
-
+
+ llassert (constraint_isDefined (c) );
+
if (c->generatingExpr == NULL)
{
c->generatingExpr = e;
- DPRINTF ((message ("setting generatingExpr for %s to %s", constraint_print (c), exprNode_unparse (e)) ));
+ DPRINTF ((message ("setting generatingExpr for %s to %s", constraint_unparse (c), exprNode_unparse (e)) ));
}
else
{
- DPRINTF ((message ("Not setting generatingExpr for %s to %s", constraint_print (c), exprNode_unparse (e)) ));
+ DPRINTF ((message ("Not setting generatingExpr for %s to %s", constraint_unparse (c), exprNode_unparse (e)) ));
}
return c;
}
+/*@noaccess exprNode@*/
constraint constraint_origAddGeneratingExpr (/*@returned@*/ constraint c, exprNode e)
{
-
+ llassert (constraint_isDefined (c) );
+
if (c->orig != constraint_undefined)
{
c->orig = constraint_addGeneratingExpr (c->orig, e);
}
else
{
- DPRINTF ((message ("constraint_origAddGeneratingExpr: Not setting generatingExpr for %s to %s", constraint_print (c), exprNode_unparse (e)) ));
+ DPRINTF ((message ("constraint_origAddGeneratingExpr: Not setting generatingExpr for %s to %s", constraint_unparse (c), exprNode_unparse (e)) ));
}
return c;
}
constraint constraint_setFcnPre (/*@returned@*/ constraint c)
{
+ llassert (constraint_isDefined (c) );
+
if (c->orig != constraint_undefined)
{
c->orig->fcnPre = TRUE;
fileloc constraint_getFileloc (constraint c)
{
+
+ llassert (constraint_isDefined (c) );
+
if (exprNode_isDefined (c->generatingExpr))
return (fileloc_copy (exprNode_getfileloc (c->generatingExpr)));
-
+
return (constraintExpr_getFileloc (c->lexpr));
-
+
}
static bool checkForMaxSet (constraint c)
{
+
+ llassert (constraint_isDefined (c) );
+
if (constraintExpr_hasMaxSet (c->lexpr) || constraintExpr_hasMaxSet (c->expr))
return TRUE;
bool constraint_hasMaxSet (constraint c)
{
+
+ llassert (constraint_isDefined (c) );
+
if (checkForMaxSet (c))
return TRUE;
ret->ar = EQ;
ret->expr = constraintExpr_makeIntLiteral ((int)size);
ret->post = TRUE;
- /*@i1*/return ret;
+ /*@i1*/
+ return ret;
}
constraint constraint_makeSRefWriteSafeInt (sRef s, int ind)
ret->ar = GTE;
ret->expr = constraintExpr_makeIntLiteral (ind);
ret->post = TRUE;
- /*@i1*/return ret;
+ /*@i1*/
+ return ret;
}
/* drl added 01/12/2000
ret->ar = GTE;
ret->expr = constraintExpr_makeIntLiteral (ind);
ret->post = TRUE;
- /*@i1*/return ret;
+ return ret;
}
constraint constraint_makeEnsureMaxReadAtLeast (exprNode t1, exprNode t2, fileloc sequencePoint)
{
constraint ret;
- ret = constraint_makeReadSafeExprNode (t1, t2);
+ ret = constraint_makeReadSafeExprNode (t1, t2);
+ llassert (constraint_isDefined (ret) );
+
ret->lexpr = constraintExpr_setFileloc (ret->lexpr, sequencePoint);
ret->post = TRUE;
constraint constraint_makeEnsureLessThan (exprNode e1, exprNode e2, fileloc sequencePoint)
{
constraintExpr t1, t2;
+ constraint t3;
t1 = constraintExpr_makeValueExpr (e1);
t2 = constraintExpr_makeValueExpr (e2);
/*change this to e1 <= (e2 -1) */
t2 = constraintExpr_makeDecConstraintExpr (t2);
-
- return ( constraint_makeEnsuresOpConstraintExpr (t1, t2, sequencePoint, LTE));
+
+ t3 = constraint_makeEnsuresOpConstraintExpr (t1, t2, sequencePoint, LTE);
+
+ t3 = constraint_simplify(t3);
+ return (t3);
}
constraint constraint_makeEnsureLessThanEqual (exprNode e1, exprNode e2, fileloc sequencePoint)
constraint constraint_makeEnsureGreaterThan (exprNode e1, exprNode e2, fileloc sequencePoint)
{
constraintExpr t1, t2;
+ constraint t3;
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 ( constraint_makeEnsuresOpConstraintExpr (t1, t2, sequencePoint, GTE));
+ return t3;
}
constraint constraint_makeEnsureGreaterThanEqual (exprNode e1, exprNode e2, fileloc sequencePoint)
}
-exprNode exprNode_copyConstraints (/*@returned@*/ exprNode dst, exprNode src)
-{
- constraintList_free (dst->ensuresConstraints);
- constraintList_free (dst->requiresConstraints);
- constraintList_free (dst->trueEnsuresConstraints);
- constraintList_free (dst->falseEnsuresConstraints);
-
- dst->ensuresConstraints = constraintList_copy (src->ensuresConstraints);
- dst->requiresConstraints = constraintList_copy (src->requiresConstraints);
- dst->trueEnsuresConstraints = constraintList_copy (src->trueEnsuresConstraints);
- dst->falseEnsuresConstraints = constraintList_copy (src->falseEnsuresConstraints);
- return dst;
-}
/* Makes the constraint e = e + f */
constraint constraint_makeAddAssign (exprNode e, exprNode f, fileloc sequencePoint)
cstring string;
fileloc errorLoc, temp;
- string = constraint_printDetailedPostCondition (c);
+ string = constraint_unparseDetailedPostCondition (c);
errorLoc = loc;
cstring string, ret;
fileloc errorLoc;
- string = constraint_print (c);
+ string = constraint_unparse (c);
errorLoc = constraint_getFileloc (c);
cstring string;
fileloc errorLoc, temp;
+ bool isLikely;
+
+ llassert (constraint_isDefined (c) );
+
/*drl 11/26/2001 avoid printing tautological constraints */
if (constraint_isAlwaysTrue (c))
{
}
- string = constraint_printDetailed (c);
+ string = constraint_unparseDetailed (c);
errorLoc = loc;
else
{
llassert (FALSE);
- DPRINTF (("constraint %s had undefined fileloc %s", constraint_print (c), fileloc_unparse (temp)));
+ DPRINTF (("constraint %s had undefined fileloc %s", constraint_unparse (c), fileloc_unparse (temp)));
fileloc_free (temp);
errorLoc = fileloc_copy (errorLoc);
}
string = cstring_replaceChar(string, '\n', ' ');
}
+ /*drl added 12/19/2002 print
+ a different error fro "likely" bounds-errors*/
+
+ isLikely = constraint_isConstantOnly(c);
- if (c->post)
+ if (isLikely)
+ {
+ if (c->post)
+ {
+ voptgenerror (FLG_FUNCTIONPOST, string, errorLoc);
+ }
+ else
+ {
+ if (constraint_hasMaxSet (c))
+ {
+ voptgenerror (FLG_LIKELYBOUNDSWRITE, string, errorLoc);
+ }
+ else
+ {
+ voptgenerror (FLG_LIKELYBOUNDSREAD, string, errorLoc);
+ }
+ }
+ }
+ else if (c->post)
{
voptgenerror (FLG_FUNCTIONPOST, string, errorLoc);
}
fileloc_free(errorLoc);
}
-static cstring constraint_printDeep (constraint c)
+static cstring constraint_unparseDeep (constraint c)
{
cstring genExpr;
- cstring st = cstring_undefined;
+ cstring st;
- st = constraint_print(c);
+ llassert (constraint_isDefined (c));
+ st = constraint_unparse (c);
if (c->orig != constraint_undefined)
{
if (c->orig->fcnPre)
{
st = cstring_concatFree (st, message (" derived from %s precondition: %q",
- genExpr, constraint_printDeep (c->orig)));
+ genExpr, constraint_unparseDeep (c->orig)));
}
else
{
st = cstring_concatFree (st, message (" needed to satisfy precondition:\n%q",
- constraint_printDeep (c->orig)));
+ constraint_unparseDeep (c->orig)));
}
}
else
{
st = cstring_concatFree (st, message ("derived from: %q",
- constraint_printDeep (c->orig)));
+ constraint_unparseDeep (c->orig)));
}
}
}
-static /*@only@*/ cstring constraint_printDetailedPostCondition (/*@observer@*/ /*@temp@*/ constraint c)
+static /*@only@*/ cstring constraint_unparseDetailedPostCondition (/*@observer@*/ /*@temp@*/ constraint c)
{
cstring st = cstring_undefined;
cstring genExpr;
-
- st = message ("Unsatisfied ensures constraint condition:\nSplint is unable to verify the constraint %q", constraint_printDeep (c));
+
+ llassert (constraint_isDefined (c) );
+
+ st = message ("Unsatisfied ensures constraint condition:\nSplint is unable to verify the constraint %q",
+ constraint_unparseDeep (c));
genExpr = exprNode_unparse (c->generatingExpr);
return st;
}
-cstring constraint_printDetailed (constraint c)
+cstring constraint_unparseDetailed (constraint c)
{
cstring st = cstring_undefined;
cstring temp = cstring_undefined;
cstring genExpr;
-
+ bool isLikely;
+
+ llassert (constraint_isDefined (c) );
+
if (!c->post)
{
- st = message ("Unable to resolve constraint:\n%q", constraint_printDeep (c));
+ st = message ("Unable to resolve constraint:\n%q", constraint_unparseDeep (c));
}
else
{
- st = message ("Block Post condition:\nThis function block has the post condition %q", constraint_printDeep (c));
+ st = message ("Block Post condition:\nThis function block has the post condition %q", constraint_unparseDeep (c));
}
- if (constraint_hasMaxSet (c))
+ isLikely = constraint_isConstantOnly(c);
+
+ if (isLikely)
{
- temp = cstring_makeLiteral ("Possible out-of-bounds store:\n");
+ if (constraint_hasMaxSet (c))
+ {
+ temp = cstring_makeLiteral ("Likely out-of-bounds store:\n");
+ }
+ else
+ {
+ temp = cstring_makeLiteral ("Likely out-of-bounds read:\n");
+ }
}
else
{
- temp = cstring_makeLiteral ("Possible out-of-bounds read:\n");
+
+ if (constraint_hasMaxSet (c))
+ {
+ temp = cstring_makeLiteral ("Possible out-of-bounds store:\n");
+ }
+ else
+ {
+ temp = cstring_makeLiteral ("Possible out-of-bounds read:\n");
+ }
}
genExpr = exprNode_unparse (c->generatingExpr);
return st;
}
-/*@only@*/ cstring constraint_print (constraint c) /*@*/
+/*@only@*/ cstring constraint_unparse (constraint c) /*@*/
{
cstring st = cstring_undefined;
cstring type = cstring_undefined;
type,
constraintExpr_print (c->lexpr),
arithType_print (c->ar),
- constraintExpr_print (c->expr)
- );
+ constraintExpr_print (c->expr));
}
else
{
type,
constraintExpr_print (c->lexpr),
arithType_print (c->ar),
- constraintExpr_print (c->expr)
- );
+ constraintExpr_print (c->expr));
}
return st;
}
-cstring constraint_printOr (constraint c) /*@*/
+cstring constraint_unparseOr (constraint c) /*@*/
{
cstring ret;
constraint temp;
ret = cstring_undefined;
+
+ llassert (constraint_isDefined (c) );
+
temp = c;
- ret = cstring_concatFree (ret, constraint_print (temp));
+ ret = cstring_concatFree (ret, constraint_unparse (temp));
temp = temp->or;
while ( constraint_isDefined (temp))
{
ret = cstring_concatFree (ret, cstring_makeLiteral (" OR "));
- ret = cstring_concatFree (ret, constraint_print (temp));
+ ret = cstring_concatFree (ret, constraint_unparse (temp));
temp = temp->or;
}
/*@only@*/ constraint constraint_doSRefFixBaseParam (/*@returned@*/ /*@only@*/ constraint precondition,
exprNodeList arglist)
{
+
+ llassert (constraint_isDefined (precondition) );
+
precondition->lexpr = constraintExpr_doSRefFixBaseParam (precondition->lexpr,
arglist);
precondition->expr = constraintExpr_doSRefFixBaseParam (precondition->expr,
constraint constraint_doFixResult (constraint postcondition, /*@dependent@*/ exprNode fcnCall)
{
postcondition = constraint_copy (postcondition);
+
+ llassert (constraint_isDefined (postcondition) );
+
+
postcondition->lexpr = constraintExpr_doFixResult (postcondition->lexpr, fcnCall);
postcondition->expr = constraintExpr_doFixResult (postcondition->expr, fcnCall);
{
precondition = constraint_copy (precondition);
+
+ llassert (constraint_isDefined (precondition) );
+
precondition->lexpr = constraintExpr_doSRefFixConstraintParam (precondition->lexpr, arglist);
precondition->expr = constraintExpr_doSRefFixConstraintParam (precondition->expr, arglist);
precondition->fcnPre = FALSE;
- return precondition;
+ return constraint_simplify(precondition);
}
constraint constraint_preserveOrig (/*@returned@*/ constraint c) /*@modifies c @*/
{
+ DPRINTF (("Doing constraint_preserverOrig for %q", constraint_printDetailed (c)));
+ llassert (constraint_isDefined (c));
- DPRINTF ((message ("Doing constraint_preserverOrig for %q ", constraint_printDetailed (c))));
-
if (c->orig == constraint_undefined)
- c->orig = constraint_copy (c);
-
+ {
+ c->orig = constraint_copy (c);
+ }
else if (c->orig->fcnPre)
{
- constraint temp;
-
- temp = c->orig;
+ 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;
}
else
{
- DPRINTF ((message ("Not changing constraint")));
+ DPRINTF (("Not changing constraint"));
}
- DPRINTF ((message ("After Doing constraint_preserverOrig for %q ", constraint_printDetailed (c))));
-
+ DPRINTF ((message ("After Doing constraint_preserverOrig for %q ", constraint_unparseDetailed (c))));
return c;
}
-/*@=fcnuse*/
-/*@=assignexpose*/
-/*@=czechfcns@*/
-
constraint constraint_togglePost (/*@returned@*/ constraint c)
{
+ llassert (constraint_isDefined (c));
c->post = !c->post;
return c;
}
constraint constraint_togglePostOrig (/*@returned@*/ constraint c)
{
+ llassert (constraint_isDefined (c));
+
if (c->orig != NULL)
- c->orig = constraint_togglePost (c->orig);
+ {
+ c->orig = constraint_togglePost (c->orig);
+ }
+
return c;
}
bool constraint_hasOrig ( /*@observer@*/ /*@temp@*/ constraint c)
{
- if (c->orig == NULL)
- return FALSE;
- else
- return TRUE;
+ llassert (constraint_isDefined (c));
+ return (c->orig != NULL);
}
constraint constraint_undump (FILE *f)
{
constraint c;
- bool fcnPre;
- bool post;
- arithType ar;
+ bool fcnPre, post;
+ arithType ar;
+ constraintExpr lexpr, expr;
+ char *s, *os;
- constraintExpr lexpr;
- constraintExpr expr;
-
-
- char * s;
-
- char *os;
-
os = mstring_create (MAX_DUMP_LINE_LENGTH);
-
s = fgets (os, MAX_DUMP_LINE_LENGTH, f);
- /*@i33*/ /*this should probably be wrappered...*/
+ if (!mstring_isDefined (s))
+ {
+ llfatalbug (message ("Library file is corrupted") );
+ }
fcnPre = (bool) reader_getInt (&s);
advanceField (&s);
post = (bool) reader_getInt (&s);
advanceField (&s);
ar = (arithType) reader_getInt (&s);
-
+
s = fgets (os, MAX_DUMP_LINE_LENGTH, f);
+ if (! mstring_isDefined(s) )
+ {
+ llfatalbug(message("Library file is corrupted") );
+ }
+
reader_checkChar (&s, 'l');
lexpr = constraintExpr_undump (f);
s = fgets (os, MAX_DUMP_LINE_LENGTH, f);
reader_checkChar (&s, 'r');
+
+ if (! mstring_isDefined(s) )
+ {
+ llfatalbug(message("Library file is corrupted") );
+ }
+
expr = constraintExpr_undump (f);
c = constraint_makeNew ();
constraintExpr lexpr;
constraintExpr expr;
-
+ llassert (constraint_isDefined (c) );
+
fcnPre = c->fcnPre;
post = c->post;
ar = c->ar;
static int constraint_getDepth (/*@observer@*/ /*@temp@*/ constraint c)
{
int l , r;
-
+
+ llassert (constraint_isDefined (c) );
+
l = constraintExpr_getDepth (c->lexpr);
r = constraintExpr_getDepth (c->expr);
if (l > r)
{
- DPRINTF (( message ("constraint depth returning %d for %s", l, constraint_print (c))));
+ DPRINTF (( message ("constraint depth returning %d for %s", l, constraint_unparse (c))));
return l;
}
else
{
- DPRINTF (( message ("constraint depth returning %d for %s", r, constraint_print (c))));
+ DPRINTF (( message ("constraint depth returning %d for %s", r, constraint_unparse (c))));
return r;
}
}
return FALSE;
}
+
+/*drl added 12/19/2002*/
+/*whether constraints consist only of
+ terms which are constants*/
+bool constraint_isConstantOnly (constraint c)
+{
+ bool l, r;
+
+ llassert (constraint_isDefined (c) );
+
+ l = constraintExpr_isConstantOnly(c->lexpr);
+ r = constraintExpr_isConstantOnly(c->expr);
+
+ if (l && r)
+ {
+ return TRUE;
+ }
+
+ else
+ {
+ return FALSE;
+ }
+
+}