** constraint.c
*/
-//#define DEBUGPRINT 1
+/* #define DEBUGPRINT 1 */
# include <ctype.h> /* for isdigit */
# include "lclintMacros.nf"
# include "basic.h"
# include "cgrammar.h"
# include "cgrammar_tokens.h"
+
# include "exprChecks.h"
# include "exprNodeSList.h"
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) */
+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 @*/;
-/* { */
-/* char *t; */
-/* int c; */
-/* constraint ret; */
-/* ret = constraint_makeNew(); */
-/* llassert (sRef_isValid(x) ); */
-/* if (!sRef_isValid(x)) */
-/* return ret; */
-
-
-/* ret->lexpr = constraintExpr_makeTermsRef (x); */
-/* #warning fix abstraction */
-
-/* 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; */
-/* // ret->orig = ret; */
-/* DPRINTF(("GENERATED CONSTRAINT:")); */
-/* DPRINTF( (message ("%s", constraint_print(ret) ) ) ); */
-/* return ret; */
-/* } */
-
-
static void
advanceField (char **s)
{
reader_checkChar (s, '@');
}
-
-
+# if 0
static constraint makeConstraintParse2 (constraintExpr l, lltok relOp, exprNode cconstant)
{
char *t;
int c;
constraint ret;
- ret = constraint_makeNew();
+ ret = constraint_makeNew ();
llassert (constraintExpr_isDefined(l) );
ret->lexpr = constraintExpr_copy (l);
ret->expr = constraintExpr_makeIntLiteral (c);
ret->post = TRUE;
- // ret->orig = ret;
DPRINTF(("GENERATED CONSTRAINT:"));
DPRINTF( (message ("%s", constraint_print(ret) ) ) );
return ret;
}
+# endif
bool constraint_same (constraint c1, constraint c2)
{
-
- if (c1->ar != c2->ar)
- return FALSE;
+ llassert (c1 != NULL);
+ llassert (c2 != NULL);
+ if (c1->ar != c2->ar)
+ {
+ return FALSE;
+ }
+
if (!constraintExpr_similar (c1->lexpr, c2->lexpr) )
- return FALSE;
+ {
+ return FALSE;
+ }
if (!constraintExpr_similar (c1->expr, c2->expr) )
- return FALSE;
+ {
+ return FALSE;
+ }
return TRUE;
}
ret->orig = constraint_copy(ret);
ret = constraint_simplify (ret);
-
- // ret->orig = ret;
+ /* ret->orig = ret; */
+
DPRINTF(("GENERATED CONSTRAINT:"));
DPRINTF( (message ("%s", constraint_print(ret) ) ) );
return ret;
constraint ret;
llassert (constraint_isDefined(c) );
- // DPRINTF((message("Copying constraint %q", constraint_print) ));
-
+
ret = constraint_makeNew();
ret->lexpr = constraintExpr_copy (c->lexpr);
ret->ar = c->ar;
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)
else
{
c->fcnPre = TRUE;
- // DPRINTF(( 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 ret = constraint_makeNew();
- // constraintTerm term;
+
po = po;
ind = ind;
ret->lexpr = constraintExpr_makeMaxReadExpr(po);
constraint ret;
ret = constraint_makeReadSafeExprNode(t1, t2);
-
- ret->lexpr = constraintExpr_setFileloc (ret->lexpr, sequencePoint);
-
+ ret->lexpr = constraintExpr_setFileloc (ret->lexpr, sequencePoint);
ret->post = TRUE;
- // fileloc_incColumn (ret->lexpr->term->loc);
return ret;
}
constraint ret;
llassert(constraintExpr_isDefined(c1) && constraintExpr_isDefined(c2) );
- // llassert(sequencePoint);
ret = constraint_makeNew();
{
llcontbug((message("null exprNode, Exprnodes are %s and %s",
exprNode_unparse(e1), exprNode_unparse(e2) )
- ));
+ ));
}
- // llassert (sequencePoint);
-
e = e1;
c1 = constraintExpr_makeValueExpr (e);
constraint constraint_makeMaxSetSideEffectPostDecrement (exprNode e, fileloc sequencePoint)
{
constraint ret = constraint_makeNew();
- //constraintTerm term;
- // e = exprNode_fakeCopy(e);
ret->lexpr = constraintExpr_makeValueExpr (e);
ret->ar = EQ;
ret->post = TRUE;
ret->expr = constraintExpr_makeValueExpr (e);
ret->expr = constraintExpr_makeDecConstraintExpr (ret->expr);
-
ret->lexpr = constraintExpr_setFileloc (ret->lexpr, sequencePoint);
-// fileloc_incColumn ( ret->lexpr->term->loc);
-// fileloc_incColumn ( ret->lexpr->term->loc);
return ret;
}
constraint constraint_makeMaxSetSideEffectPostIncrement (exprNode e, fileloc sequencePoint)
{
constraint ret = constraint_makeNew();
- //constraintTerm term;
- // e = exprNode_fakeCopy(e);
ret->lexpr = constraintExpr_makeValueExpr (e);
ret->ar = EQ;
ret->post = TRUE;
ret->expr = constraintExpr_makeIncConstraintExpr (ret->expr);
ret->lexpr = constraintExpr_setFileloc (ret->lexpr, sequencePoint);
-// fileloc_incColumn ( ret->lexpr->term->loc);
-// fileloc_incColumn ( ret->lexpr->term->loc);
return ret;
}
}
-
-// constraint constraint_makeMaxReadSideEffectPostIncrement (exprNode e, fileloc sequencePoint)
-// {
-// constraint ret = constraint_makeNew();
-// //constraintTerm term;
-
-// e = exprNode_fakeCopy(e);
-// ret->lexpr = constraintExpr_makeMaxReadExpr(e);
-// ret->ar = EQ;
-// ret->post = TRUE;
-// ret->expr = constraintExpr_makeIncConstraintExpr (e);
-// ret->lexpr = constraintExpr_setFileLoc (ret->lexpr, sequencePoint);
-// return ret;
-// }
-
-
cstring arithType_print (arithType ar) /*@*/
{
cstring st = cstring_undefined;
switch (ar)
{
case LT:
- st = cstring_makeLiteral (" < ");
+ st = cstring_makeLiteral ("<");
break;
case LTE:
- st = cstring_makeLiteral (" <= ");
+ st = cstring_makeLiteral ("<=");
break;
case GT:
- st = cstring_makeLiteral (" > ");
+ st = cstring_makeLiteral (">");
break;
case GTE:
- st = cstring_makeLiteral (" >= ");
+ st = cstring_makeLiteral (">=");
break;
case EQ:
- st = cstring_makeLiteral (" == ");
+ st = cstring_makeLiteral ("==");
break;
case NONNEGATIVE:
- st = cstring_makeLiteral (" NONNEGATIVE ");
+ st = cstring_makeLiteral ("NONNEGATIVE");
break;
case POSITIVE:
- st = cstring_makeLiteral (" POSITIVE ");
+ st = cstring_makeLiteral ("POSITIVE");
break;
default:
llassert(FALSE);
}
}
+ /*drl added 8-11-001*/
+cstring constraint_printLocation (/*@observer@*/ /*@temp@*/ constraint c) /*@*/
+{
+ cstring string, ret;
+ fileloc errorLoc;
+
+ string = constraint_print(c);
+
+ errorLoc = constraint_getFileloc(c);
+
+ ret = message ("constraint: %q @ %q", string, fileloc_unparse(errorLoc) );
+
+ fileloc_free(errorLoc);
+ return ret;
+
+}
errorLoc = loc;
- loc = NULL;
-
temp = constraint_getFileloc(c);
if (fileloc_isDefined(temp) )
{
errorLoc = temp;
-
- if (c->post)
- {
- voptgenerror (FLG_FUNCTIONPOST, string, errorLoc);
- }
- else
- {
- voptgenerror (FLG_FUNCTIONCONSTRAINT, string, errorLoc);
- }
+ }
+ else
+ {
+ llassert(FALSE);
+ DPRINTF (("constraint %s had undefined fileloc %s", constraint_print(c), fileloc_unparse(temp)));
fileloc_free(temp);
- errorLoc = NULL;
+ errorLoc = fileloc_copy(errorLoc);
+ }
+
+ if (c->post)
+ {
+ voptgenerror (FLG_FUNCTIONPOST, string, errorLoc);
}
else
{
- if (c->post)
- {
- voptgenerror (FLG_FUNCTIONPOST, string, errorLoc);
- }
+ if (constraint_hasMaxSet (c) )
+ voptgenerror (FLG_ARRAYBOUNDS, string, errorLoc);
else
- {
- voptgenerror (FLG_FUNCTIONCONSTRAINT, string, errorLoc);
- }
- errorLoc = NULL;
+ voptgenerror (FLG_ARRAYBOUNDSREAD, string, errorLoc);
}
+
+ fileloc_free(errorLoc);
+
}
if (c->orig != constraint_undefined)
{
+ st = cstring_appendChar(st, '\n');
genExpr = exprNode_unparse(c->orig->generatingExpr);
if (!c->post)
{
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) )
) );
if (context_getFlag (FLG_CONSTRAINTLOCATION) )
{
cstring temp;
- // llassert (c->generatingExpr);
- temp = message ("\nOriginal Generating expression %q: %s\n", fileloc_unparse( exprNode_getfileloc (c->generatingExpr) ),
+
+ temp = message ("\nOriginal Generating expression %q: %s\n",
+ fileloc_unparse( exprNode_getfileloc (c->generatingExpr) ),
genExpr );
st = cstring_concatFree (st, temp);
cstring constraint_printDetailed (constraint c)
{
cstring st = cstring_undefined;
- cstring genExpr;
+ cstring temp = cstring_undefined;
+ cstring genExpr;
if (!c->post)
{
- st = message ("Unresolved constraint:\nLclint is unable to resolve %q", constraint_printDeep (c) );
+ 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:\n");
+ }
+ else
+ {
+ temp = cstring_makeLiteral("Possible out-of-bounds read:\n");
+ }
+
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) ),
- genExpr );
- st = cstring_concatFree (st, temp);
-
- if (constraint_hasMaxSet(c) )
- {
- temp = message ("Has MaxSet\n");
- st = cstring_concatFree (st, temp);
- }
+ cstring temp2;
+ temp2 = message ("%s\n", genExpr );
+ temp = cstring_concatFree (temp, temp2);
}
+
+ st = cstring_concatFree(temp,st);
+
return st;
}
llassert (c !=NULL);
if (c->post)
{
- type = cstring_makeLiteral ("Ensures: ");
+ if (context_getFlag (FLG_PARENCONSTRAINT) )
+ {
+ type = cstring_makeLiteral ("ensures: ");
+ }
+ else
+ {
+ type = cstring_makeLiteral ("ensures");
+ }
}
else
{
- type = cstring_makeLiteral ("Requires: ");
+ if (context_getFlag (FLG_PARENCONSTRAINT) )
+ {
+ type = cstring_makeLiteral ("requires: ");
+ }
+ else
+ {
+ type = cstring_makeLiteral ("requires");
+ }
+
}
- st = message ("%q: %q %q %q",
- type,
- constraintExpr_print (c->lexpr),
- arithType_print(c->ar),
- constraintExpr_print(c->expr)
+ if (context_getFlag (FLG_PARENCONSTRAINT) )
+ {
+ st = message ("%q: %q %q %q",
+ type,
+ constraintExpr_print (c->lexpr),
+ arithType_print(c->ar),
+ constraintExpr_print(c->expr)
+ );
+ }
+ else
+ {
+ st = message ("%q %q %q %q",
+ type,
+ constraintExpr_print (c->lexpr),
+ arithType_print(c->ar),
+ constraintExpr_print(c->expr)
);
+ }
return st;
}
return precondition;
}
-// bool constraint_hasTerm (constraint c, constraintTerm term)
-// {
-// DPRINTF((message ("Constraint %s", constraint_print (c) ) ) );
-
-// if (constraintExpr_includesTerm (c->lexpr, term) )
-// return TRUE;
-
-// if (constraintExpr_includesTerm (c->expr, term) )
-// return TRUE;
-
-// return FALSE;
-// }
-
constraint constraint_preserveOrig (/*@returned@*/ constraint c) /*@modifies c @*/
{
c->expr = expr;
free(os);
+ c = constraint_preserveOrig(c);
return c;
}
}
+int constraint_compare (/*@observer@*/ /*@temp@*/ const constraint * c1, /*@observer@*/ /*@temp@*/ const 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;
+}
+
+
+bool constraint_isPost (/*@observer@*/ /*@temp@*/ constraint c)
+{
+ llassert(constraint_isDefined(c) );
+
+ if (constraint_isUndefined(c) )
+ return FALSE;
+
+ return (c->post);
+}
+
+
+static int constraint_getDepth(/*@observer@*/ /*@temp@*/ constraint c)
+{
+ int l , r;
+
+ 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) ) ));
+ return l;
+ }
+ else
+ {
+ DPRINTF(( message("constraint depth returning %d for %s", r, constraint_print(c) ) ));
+ return r;
+ }
+}
+
+
+bool constraint_tooDeep (/*@observer@*/ /*@temp@*/ constraint c)
+{
+ int temp;
+
+ temp = constraint_getDepth(c);
+
+ if (temp >= 20 )
+ {
+ return TRUE;
+ }
+
+ return FALSE;
+
+}