# include "cgrammar_tokens.h"
# include "exprChecks.h"
-# include "aliasChecks.h"
# include "exprNodeSList.h"
-//# include "exprData.i"
/*@i33*/
-/*@-fcnuse*/
-/*@-assignexpose*/
/*@access exprNode @*/
-static /*@notnull@*/ /*@special@*/ constraint constraint_makeNew (void)
- /*@post:isnull result->or, result->orig, result->generatingExpr, result->fcnPre @*/ /*@defines result->or, result->generatingExpr, result->orig, result->fcnPre @*/;
+static /*@only@*/ cstring constraint_printDetailedPostCondition (/*@observer@*/ /*@temp@*/ constraint p_c);
+
+
+static /*@notnull@*/ /*@special@*/ constraint constraint_makeNew (void)
+ /*@post:isnull result->or, result->orig, result->generatingExpr, result->fcnPre @*/
+ /*@defines result->or, result->generatingExpr, result->orig, result->fcnPre @*/;
/* constraint makeConstraintParse (sRef x, lltok relOp, exprNode cconstant) */
/* return ret; */
/* } */
-constraint makeConstraintParse2 (constraintExpr l, lltok relOp, exprNode cconstant)
+
+static void
+advanceField (char **s)
+{
+ reader_checkChar (s, '@');
+}
+
+
+
+static constraint makeConstraintParse2 (constraintExpr l, lltok relOp, exprNode cconstant)
{
char *t;
int c;
constraint ret;
- ret = constraint_makeNew();
- llassert (l!=NULL);
+ ret = constraint_makeNew ();
+ llassert (constraintExpr_isDefined(l) );
ret->lexpr = constraintExpr_copy (l);
- #warning fix abstraction
+
if (relOp.tok == GE_OP)
ret->ar = GTE;
{
constraint ret;
ret = constraint_makeNew();
- llassert (l !=NULL);
+ llassert (constraintExpr_isDefined(l) );
ret->lexpr = constraintExpr_copy (l);
- #warning fix abstraction
if (relOp.tok == GE_OP)
ret->ar = GTE;
return ret;
}
-constraint constraint_copy (constraint c)
+constraint constraint_copy (/*@temp@*/ /*@observer@*/ constraint c)
{
constraint ret;
llassert (constraint_isDefined(c) );
- // TPRINTF((message("Copying constraint %q", constraint_print) ));
+ // DPRINTF((message("Copying constraint %q", constraint_print) ));
ret = constraint_makeNew();
ret->lexpr = constraintExpr_copy (c->lexpr);
ret->ar = c->ar;
ret->expr = constraintExpr_copy (c->expr);
ret->post = c->post;
- ret->generatingExpr = exprNode_fakeCopy(c->generatingExpr);
+ /*@-assignexpose@*/
+ ret->generatingExpr = c->generatingExpr;
+ /*@=assignexpose@*/
/*@i33 fix this*/
if (c->orig != NULL)
c1->or = NULL;
c1->fcnPre = c2->fcnPre;
-
+
+ /*@-assignexpose@*/
c1->generatingExpr = c2->generatingExpr;
+ /*@=assignexpose@*/
}
static /*@notnull@*/ /*@special@*/ constraint constraint_makeNew (void)
- /*@post:isnull result->or, result->orig, result->generatingExpr, result->fcnPre @*/ /*@defines result->or, result->generatingExpr, result->orig, result->fcnPre @*/
+ /*@post:isnull result->or, result->orig, result->generatingExpr, result->fcnPre @*/
+ /*@defines result->or, result->generatingExpr, result->orig, result->fcnPre @*/
{
constraint ret;
ret = dmalloc(sizeof (*ret) );
return ret;
}
-constraint constraint_addGeneratingExpr (/*@returned@*/ constraint c, exprNode e)
+constraint constraint_addGeneratingExpr (/*@returned@*/ constraint c, /*@exposed@*/ exprNode e)
{
if (c->generatingExpr == NULL)
{
- c->generatingExpr = exprNode_fakeCopy(e);
+ c->generatingExpr = e;
DPRINTF ((message ("setting generatingExpr for %s to %s", constraint_print(c), exprNode_unparse(e) ) ));
}
else
return c;
}
-
-
constraint constraint_setFcnPre (/*@returned@*/ constraint c )
{
else
{
c->fcnPre = TRUE;
- TPRINTF(( message("Warning Setting fcnPre directly") ));
+ // DPRINTF(( message("Warning Setting fcnPre directly") ));
}
return c;
}
bool constraint_hasMaxSet(constraint c)
{
+ if (checkForMaxSet(c) )
+ return TRUE;
+
if (c->orig != NULL)
{
if (checkForMaxSet(c->orig) )
return TRUE;
}
- return (checkForMaxSet(c) );
+ return FALSE;
}
-constraint constraint_makeReadSafeExprNode ( exprNode po, exprNode ind)
+constraint constraint_makeReadSafeExprNode ( exprNode po, exprNode ind)
{
constraint ret = constraint_makeNew();
// constraintTerm term;
- po = exprNode_fakeCopy(po);
- ind = exprNode_fakeCopy(ind);
+ po = po;
+ ind = ind;
ret->lexpr = constraintExpr_makeMaxReadExpr(po);
ret->ar = GTE;
ret->expr = constraintExpr_makeValueExpr (ind);
return ret;
}
-constraint constraint_makeWriteSafeInt (exprNode po, int ind)
+constraint constraint_makeWriteSafeInt ( exprNode po, int ind)
{
constraint ret = constraint_makeNew();
}
-constraint constraint_makeReadSafeInt ( exprNode po, int ind)
+constraint constraint_makeReadSafeInt ( exprNode t1, int index)
{
constraint ret = constraint_makeNew();
- po = exprNode_fakeCopy(po);
-
- ret->lexpr = constraintExpr_makeMaxReadExpr(po);
+ ret->lexpr = constraintExpr_makeMaxReadExpr(t1);
ret->ar = GTE;
- ret->expr = constraintExpr_makeIntLiteral (ind);
+ ret->expr = constraintExpr_makeIntLiteral (index);
ret->post = FALSE;
return ret;
}
/*@i1*/return ret;
}
-constraint constraint_makeEnsureMaxReadAtLeast (exprNode e1, exprNode t2, fileloc sequencePoint)
+constraint constraint_makeEnsureMaxReadAtLeast (exprNode t1, exprNode t2, fileloc sequencePoint)
{
constraint ret;
-
- e1 = exprNode_fakeCopy (e1);
- t2 = exprNode_fakeCopy (t2);
- ret = constraint_makeReadSafeExprNode(e1, t2);
+ ret = constraint_makeReadSafeExprNode(t1, t2);
ret->lexpr = constraintExpr_setFileloc (ret->lexpr, sequencePoint);
constraint ret;
- llassert(c1 && c2);
+ llassert(constraintExpr_isDefined(c1) && constraintExpr_isDefined(c2) );
// llassert(sequencePoint);
ret = constraint_makeNew();
return ret;
}
-static constraint constraint_makeEnsuresOp (exprNode e1, 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 (! (e1 && e2) )
+ if (! (exprNode_isDefined(e1) && exprNode_isDefined(e2) ) )
{
llcontbug((message("null exprNode, Exprnodes are %s and %s",
exprNode_unparse(e1), exprNode_unparse(e2) )
// llassert (sequencePoint);
- e = exprNode_fakeCopy(e1);
+ e = e1;
c1 = constraintExpr_makeValueExpr (e);
- e = exprNode_fakeCopy(e2);
+ e = e2;
c2 = constraintExpr_makeValueExpr (e);
ret = constraint_makeEnsuresOpConstraintExpr (c1, c2, sequencePoint, ar);
return dst;
}
+/* Makes the constraint e = e + f */
+constraint constraint_makeAddAssign (exprNode e, exprNode f, fileloc sequencePoint)
+{
+ constraintExpr x1, x2, y;
+ constraint ret;
+
+ ret = constraint_makeNew();
+
+ x1 = constraintExpr_makeValueExpr (e);
+ x2 = constraintExpr_copy(x1);
+ y = constraintExpr_makeValueExpr (f);
+
+ ret->lexpr = x1;
+ ret->ar = EQ;
+ ret->post = TRUE;
+ ret->expr = constraintExpr_makeAddExpr (x2, y);
+
+ ret->lexpr = constraintExpr_setFileloc (ret->lexpr, sequencePoint);
+
+ return ret;
+}
+
+
+/* Makes the constraint e = e - f */
+constraint constraint_makeSubtractAssign (exprNode e, exprNode f, fileloc sequencePoint)
+{
+ constraintExpr x1, x2, y;
+ constraint ret;
+
+ ret = constraint_makeNew();
+
+ x1 = constraintExpr_makeValueExpr (e);
+ x2 = constraintExpr_copy(x1);
+ y = constraintExpr_makeValueExpr (f);
+
+ ret->lexpr = x1;
+ ret->ar = EQ;
+ ret->post = TRUE;
+ ret->expr = constraintExpr_makeSubtractExpr (x2, y);
+
+ ret->lexpr = constraintExpr_setFileloc (ret->lexpr, sequencePoint);
+
+ return ret;
+}
+
constraint constraint_makeMaxSetSideEffectPostDecrement (exprNode e, fileloc sequencePoint)
{
constraint ret = constraint_makeNew();
//constraintTerm term;
- e = exprNode_fakeCopy(e);
+ // e = exprNode_fakeCopy(e);
ret->lexpr = constraintExpr_makeValueExpr (e);
ret->ar = EQ;
ret->post = TRUE;
constraint ret = constraint_makeNew();
//constraintTerm term;
- e = exprNode_fakeCopy(e);
+ // e = exprNode_fakeCopy(e);
ret->lexpr = constraintExpr_makeValueExpr (e);
ret->ar = EQ;
ret->post = TRUE;
}
-void constraint_free (/*@only@*/ /*@notnull@*/ constraint c)
+void constraint_free (/*@only@*/ constraint c)
{
llassert(constraint_isDefined (c) );
return st;
}
+void constraint_printErrorPostCondition (constraint c, fileloc loc)
+{
+ cstring string;
+ fileloc errorLoc, temp;
+
+ string = constraint_printDetailedPostCondition (c);
+
+ errorLoc = loc;
+
+ loc = NULL;
+
+ temp = constraint_getFileloc(c);
+
+ if (fileloc_isDefined(temp) )
+ {
+ errorLoc = temp;
+ voptgenerror ( FLG_CHECKPOST, string, errorLoc);
+ fileloc_free(temp);
+ }
+ else
+ {
+ voptgenerror ( FLG_CHECKPOST, string, errorLoc);
+ }
+}
+
+
+
+
void constraint_printError (constraint c, fileloc loc)
{
cstring string;
}
else
{
- voptgenerror (FLG_FUNCTIONCONSTRAINT, string, errorLoc);
+ if (constraint_hasMaxSet (c) )
+ voptgenerror (FLG_ARRAYBOUNDS, string, errorLoc);
+ else
+ voptgenerror (FLG_ARRAYBOUNDSREAD, string, errorLoc);
}
fileloc_free(temp);
+ errorLoc = NULL;
}
else
{
{
voptgenerror (FLG_FUNCTIONCONSTRAINT, string, errorLoc);
}
+ errorLoc = NULL;
}
}
-cstring constraint_printDeep (constraint c)
+static cstring constraint_printDeep (constraint c)
{
+ cstring genExpr;
cstring st = cstring_undefined;
st = constraint_print(c);
+
if (c->orig != constraint_undefined)
{
+ st = cstring_appendChar(st, '\n');
+ genExpr = exprNode_unparse(c->orig->generatingExpr);
if (!c->post)
{
if (c->orig->fcnPre)
- st = cstring_concatFree(st, (message(" derived from %s precondition: %q", exprNode_unparse(c->orig->generatingExpr), constraint_printDeep(c->orig) )
+ st = cstring_concatFree(st, (message(" derived from %s precondition: %q", genExpr, constraint_printDeep(c->orig) )
) );
else
- st = cstring_concatFree(st,(message(" needed to satisfy %q",
+ st = cstring_concatFree(st,(message(" needed to satisfy precondition:\n%q",
constraint_printDeep(c->orig) )
) );
}
-cstring constraint_printDetailed (constraint c)
+
+static /*@only@*/ cstring constraint_printDetailedPostCondition (/*@observer@*/ /*@temp@*/ constraint c)
{
cstring st = cstring_undefined;
+ cstring genExpr;
+
+ st = message ("Unsatisfied ensures constraint condition:\nLCLint is unable to verify the constraint %q", constraint_printDeep (c) );
- if (!c->post)
- {
- st = message ("Unresolved constraint:\nLclint is unable to resolve %q", constraint_printDeep (c) );
- }
- else
- {
- st = message ("Block Post condition:\nThis function block has the post condition %q", constraint_printDeep (c) );
- }
-
+ genExpr = exprNode_unparse (c->generatingExpr);
+
if (context_getFlag (FLG_CONSTRAINTLOCATION) )
{
cstring temp;
// llassert (c->generatingExpr);
temp = message ("\nOriginal Generating expression %q: %s\n", fileloc_unparse( exprNode_getfileloc (c->generatingExpr) ),
- exprNode_unparse(c->generatingExpr) );
+ genExpr );
st = cstring_concatFree (st, temp);
if (constraint_hasMaxSet(c) )
{
- temp = message ("\nHas MaxSet\n");
+ temp = message ("Has MaxSet\n");
st = cstring_concatFree (st, temp);
}
}
return st;
}
+cstring constraint_printDetailed (constraint c)
+{
+ cstring st = cstring_undefined;
+ cstring temp = cstring_undefined;
+ cstring genExpr;
+
+ if (!c->post)
+ {
+ st = message ("Unable to resolve constraint:\n%q", constraint_printDeep (c) );
+ }
+ else
+ {
+ st = message ("Block Post condition:\nThis function block has the post condition %q", constraint_printDeep (c) );
+ }
+
+ if (constraint_hasMaxSet(c) )
+ {
+ temp = cstring_makeLiteral("Possible out-of-bounds store. ");
+ }
+ else
+ {
+ temp = cstring_makeLiteral("Possible out-of-bounds read. ");
+ }
+
+ st = cstring_concatFree(temp,st);
+
+ genExpr = exprNode_unparse (c->generatingExpr);
+
+ if (context_getFlag (FLG_CONSTRAINTLOCATION) )
+ {
+ temp = message ("\nConstraint generated from expression: %s at %q\n",
+ genExpr,
+ fileloc_unparse( exprNode_getfileloc (c->generatingExpr) )
+ );
+ st = cstring_concatFree (st, temp);
+ }
+ return st;
+}
+
/*@only@*/ cstring constraint_print (constraint c) /*@*/
{
cstring st = cstring_undefined;
llassert (c !=NULL);
if (c->post)
{
- type = cstring_makeLiteral ("Ensures: ");
+ type = cstring_makeLiteral ("ensures: ");
}
else
{
- type = cstring_makeLiteral ("Requires: ");
+ type = cstring_makeLiteral ("requires: ");
}
st = message ("%q: %q %q %q",
type,
}
-constraint constraint_doFixResult (constraint postcondition, exprNode fcnCall)
+constraint constraint_doFixResult (constraint postcondition, /*@dependent@*/ exprNode fcnCall)
{
postcondition = constraint_copy (postcondition);
postcondition->lexpr = constraintExpr_doFixResult (postcondition->lexpr, fcnCall);
c->orig = NULL;
c->orig = constraint_copy (c);
if (c->orig->orig == NULL)
- c->orig->orig = temp;
+ {
+ c->orig->orig = temp;
+ temp = NULL;
+ }
else
- llcontbug((message("Expected c->orig->orig to be null" ) ));
+ {
+ llcontbug((message("Expected c->orig->orig to be null" ) ));
+ constraint_free(c->orig->orig);
+ c->orig->orig = temp;
+ temp = NULL;
+ }
}
else
{
/*@=assignexpose*/
/*@=czechfcns@*/
+
constraint constraint_togglePost (/*@returned@*/ constraint c)
{
c->post = !c->post;
return c;
}
+
+constraint constraint_togglePostOrig (/*@returned@*/ constraint c)
+{
+ if (c->orig != NULL)
+ c->orig = constraint_togglePost(c->orig);
+ return c;
+}
+
+bool constraint_hasOrig( /*@observer@*/ /*@temp@*/ constraint c)
+{
+ if (c->orig == NULL)
+ return FALSE;
+ else
+ return TRUE;
+}
+
+
+constraint constraint_undump (FILE *f)
+{
+ constraint c;
+ bool fcnPre;
+ bool post;
+ arithType ar;
+
+ constraintExpr lexpr;
+ constraintExpr expr;
+
+
+ char * s;
+
+ char *os;
+
+ s = mstring_create (MAX_DUMP_LINE_LENGTH);
+
+ os = s;
+
+ s = fgets(os, MAX_DUMP_LINE_LENGTH, f);
+
+ /*@i33*/ /*this should probably be wrappered...*/
+
+ 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);
+
+ reader_checkChar (&s, 'l');
+
+ lexpr = constraintExpr_undump (f);
+
+ s = fgets(os, MAX_DUMP_LINE_LENGTH, f);
+
+ reader_checkChar (&s, 'r');
+ expr = constraintExpr_undump (f);
+
+ c = constraint_makeNew();
+
+ c->fcnPre = fcnPre;
+ c->post = post;
+ c->ar = ar;
+
+ c->lexpr = lexpr;
+ c->expr = expr;
+
+ free(os);
+ c = constraint_preserveOrig(c);
+ return c;
+}
+
+
+void constraint_dump (/*@observer@*/ constraint c, FILE *f)
+{
+ bool fcnPre;
+ bool post;
+ arithType ar;
+
+ constraintExpr lexpr;
+ constraintExpr expr;
+
+
+ fcnPre = c->fcnPre;
+ post = c->post;
+ ar = c->ar;
+ lexpr = c->lexpr;
+ expr = c->expr;
+
+ fprintf(f, "%d@%d@%d\n", (int) fcnPre, (int) post, (int) ar);
+ fprintf(f,"l\n");
+ constraintExpr_dump (lexpr, f);
+ fprintf(f,"r\n");
+ constraintExpr_dump (expr, f);
+}
+
+
+int constraint_compare (/*@observer@*/ /*@temp@*/ constraint * c1, /*@observer@*/ /*@temp@*/ constraint * c2) /*@*/
+{
+ fileloc loc1, loc2;
+
+ int ret;
+
+ llassert(constraint_isDefined(*c1) );
+ llassert(constraint_isDefined(*c2) );
+
+ if (constraint_isUndefined(*c1) )
+ {
+ if (constraint_isUndefined(*c2) )
+ return 0;
+ else
+ return 1;
+ }
+
+ if (constraint_isUndefined(*c2) )
+ {
+ return -1;
+ }
+
+ loc1 = constraint_getFileloc(*c1);
+ loc2 = constraint_getFileloc(*c2);
+
+ ret = fileloc_compare(loc1, loc2);
+
+ fileloc_free(loc1);
+ fileloc_free(loc2);
+
+ return ret;
+}
+
+
andersk / splint.git / blobdiff