X-Git-Url: http://andersk.mit.edu/gitweb/splint.git/blobdiff_plain/93307a76942c3d0e463af62442eef5a542ebdfb2..22b8afc959f05820d93be5f55d2251e42ebc3bd8:/src/constraint.c diff --git a/src/constraint.c b/src/constraint.c index bcf358a..2187b0d 100644 --- a/src/constraint.c +++ b/src/constraint.c @@ -2,6 +2,8 @@ ** constraintList.c */ +//#define DEBUGPRINT 1 + # include /* for isdigit */ # include "lclintMacros.nf" # include "basic.h" @@ -27,8 +29,8 @@ constraint makeConstraintParse (sRef x, lltok relOp, exprNode cconstant) int c; constraint ret; ret = constraint_makeNew(); - llassert (x); - if (!x) + llassert (sRef_isValid(x) ); + if (!sRef_isValid(x)) return ret; @@ -131,6 +133,8 @@ constraint constraint_copy (constraint c) ret->ar = c->ar; ret->expr = constraintExpr_copy (c->expr); ret->post = c->post; + ret->generatingExpr = c->generatingExpr; + /*@i33 fix this*/ if (c->orig != NULL) ret->orig = constraint_copy (c->orig); @@ -152,7 +156,7 @@ void constraint_overWrite (constraint c1, constraint c2) c1->orig = constraint_copy (c2->orig); else c1->orig = NULL; - + c1->generatingExpr = c2->generatingExpr; } bool constraint_resolve (/*@unused@*/ constraint c) @@ -171,16 +175,54 @@ constraint constraint_makeNew (void) ret->ar = LT; ret->post = FALSE; ret->orig = NULL; + ret->generatingExpr = NULL; /*@i23*/return ret; } +constraint constraint_addGeneratingExpr (/*@returned@*/ constraint c, exprNode e) +{ + + if (c->generatingExpr == NULL) + { + c->generatingExpr = e; + DPRINTF ((message ("setting generatingExpr for %s to %s", constraint_print(c), exprNode_unparse(e) ) )); + } + else + { + DPRINTF ((message ("Not setting generatingExpr for %s to %s", constraint_print(c), exprNode_unparse(e) ) )); + } + return c; +} + fileloc constraint_getFileloc (constraint c) { + if (c->generatingExpr) + return (exprNode_getfileloc (c->generatingExpr) ); + return (constraintExpr_getFileloc (c->lexpr) ); } +static bool checkForMaxSet (constraint c) +{ + if (constraintExpr_hasMaxSet(c->lexpr) || constraintExpr_hasMaxSet(c->expr) ) + return TRUE; + + return FALSE; +} + +bool constraint_hasMaxSet(constraint c) +{ + if (c->orig) + { + if (checkForMaxSet(c->orig) ) + return TRUE; + } + + return (checkForMaxSet(c) ); +} + constraint constraint_makeReadSafeExprNode ( exprNode po, exprNode ind) { constraint ret = constraint_makeNew(); @@ -203,7 +245,44 @@ constraint constraint_makeWriteSafeInt (exprNode po, int ind) ret->expr = constraintExpr_makeValueInt (ind); /*@i1*/return ret; } - + +constraint constraint_makeSRefSetBufferSize (sRef s, int size) +{ + constraint ret = constraint_makeNew(); + ret->lexpr = constraintExpr_makeSRefMaxset (s); + ret->ar = EQ; + ret->expr = constraintExpr_makeValueInt (size); + ret->post = TRUE; + /*@i1*/return ret; +} + +constraint constraint_makeSRefWriteSafeInt (sRef s, int ind) +{ + constraint ret = constraint_makeNew(); + + + ret->lexpr = constraintExpr_makeSRefMaxset (s); + ret->ar = GTE; + ret->expr = constraintExpr_makeValueInt (ind); + ret->post = TRUE; + /*@i1*/return ret; +} + +/* drl added 01/12/2000 + + makes the constraint: Ensures index <= MaxRead(buffer) */ + +constraint constraint_makeEnsureLteMaxRead(exprNode index, exprNode buffer) +{ + constraint ret = constraint_makeNew(); + + ret->lexpr = constraintExpr_makeValueExpr (index); + ret->ar = LTE; + ret->expr = constraintExpr_makeMaxReadExpr(buffer); + ret->post = TRUE; + return ret; +} + constraint constraint_makeWriteSafeExprNode (exprNode po, exprNode ind) { constraint ret = constraint_makeNew(); @@ -214,7 +293,8 @@ constraint constraint_makeWriteSafeExprNode (exprNode po, exprNode ind) ret->expr = constraintExpr_makeValueExpr (ind); /*@i1*/return ret; } - + + constraint constraint_makeReadSafeInt ( exprNode po, int ind) { constraint ret = constraint_makeNew(); @@ -246,28 +326,60 @@ constraint constraint_makeEnsureMaxReadAtLeast (exprNode e1, exprNode t2, filelo } -/* make constraint ensures e1 == e2 */ - -constraint constraint_makeEnsureEqual (exprNode e1, exprNode e2, fileloc sequencePoint) +static constraint constraint_makeEnsuresOp (exprNode e1, exprNode e2, fileloc sequencePoint, arithType ar) { constraint ret = constraint_makeNew(); exprNode e; e = exprNode_fakeCopy(e1); + if (! (e1 && e2) ) + { + llcontbug((message("null exprNode, Exprnodes are %s and %s", + exprNode_unparse(e1), exprNode_unparse(e2) ) + )); + } + ret->lexpr = constraintExpr_makeValueExpr (e); - ret->ar = EQ; + ret->ar = ar; ret->post = TRUE; e = exprNode_fakeCopy(e2); ret->expr = constraintExpr_makeValueExpr (e); ret->lexpr = constraintExpr_setFileloc (ret->lexpr, sequencePoint); -// fileloc_incColumn ( ret->lexpr->term->loc); -// fileloc_incColumn ( ret->lexpr->term->loc); return ret; } -exprNode exprNode_copyConstraints (exprNode dst, exprNode src) +/* make constraint ensures e1 == e2 */ + +constraint constraint_makeEnsureEqual (exprNode e1, exprNode e2, fileloc sequencePoint) +{ + return ( constraint_makeEnsuresOp (e1, e2, sequencePoint, EQ) ); +} + +/*make constraint ensures e1 < e2 */ +constraint constraint_makeEnsureLessThan (exprNode e1, exprNode e2, fileloc sequencePoint) +{ + return ( constraint_makeEnsuresOp (e1, e2, sequencePoint, LT) ); +} + +constraint constraint_makeEnsureLessThanEqual (exprNode e1, exprNode e2, fileloc sequencePoint) +{ + return ( constraint_makeEnsuresOp (e1, e2, sequencePoint, LTE) ); +} + +constraint constraint_makeEnsureGreaterThan (exprNode e1, exprNode e2, fileloc sequencePoint) +{ + return ( constraint_makeEnsuresOp (e1, e2, sequencePoint, GT) ); +} + +constraint constraint_makeEnsureGreaterThanEqual (exprNode e1, exprNode e2, fileloc sequencePoint) +{ + return ( constraint_makeEnsuresOp (e1, e2, sequencePoint, GTE) ); +} + + +exprNode exprNode_copyConstraints (/*@returned@*/ exprNode dst, exprNode src) { dst->ensuresConstraints = constraintList_copy (src->ensuresConstraints ); dst->requiresConstraints = constraintList_copy (src->requiresConstraints ); @@ -276,6 +388,23 @@ exprNode exprNode_copyConstraints (exprNode dst, exprNode src) return dst; } +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(); @@ -344,15 +473,39 @@ cstring arithType_print (arithType ar) return st; } +void constraint_printError (constraint c, fileloc loc) +{ + cstring string; + fileloc errorLoc; + + string = constraint_printDetailed (c); + + errorLoc = loc; + + if (constraint_getFileloc(c) ) + errorLoc = constraint_getFileloc(c); + + + if (c->post) + { + voptgenerror (FLG_FUNCTIONPOST, string, errorLoc); + } + else + { + voptgenerror (FLG_FUNCTIONCONSTRAINT, string, errorLoc); + } + +} cstring constraint_printDetailed (constraint c) { cstring st = cstring_undefined; + if (!c->post) { if (c->orig) - st = message ("Unresolved constraint:\nLclint is unable to resolve %s needed to satisy %s", constraint_print (c), constraint_print(c->orig) ); + st = message ("Unresolved constraint:\nLclint is unable to resolve %s needed to satisfy %s", constraint_print (c), constraint_print(c->orig) ); else st = message ("Unresolved constraint:\nLclint is unable to resolve %s", constraint_print (c)); @@ -364,10 +517,26 @@ cstring constraint_printDetailed (constraint c) else st = message ("Block Post condition:\nThis function block has the post condition %s", constraint_print (c)); } + + if (context_getFlag (FLG_CONSTRAINTLOCATION) ) + { + cstring temp; + // llassert (c->generatingExpr); + temp = message ("\nOriginal Generating expression %s: %s\n", fileloc_unparse( exprNode_getfileloc (c->generatingExpr) ), + exprNode_unparse(c->generatingExpr) ); + st = cstring_concat (st, temp); + + if (constraint_hasMaxSet(c) ) + { + cstring temp2; + temp2 = message ("\nHas MaxSet\n"); + st = cstring_concat (st, temp2); + } + } return st; } -cstring constraint_print (constraint c) +cstring constraint_print (constraint c) /*@*/ { cstring st = cstring_undefined; cstring type = cstring_undefined; @@ -401,6 +570,26 @@ constraint constraint_doSRefFixBaseParam (constraint precondition, } +constraint constraint_doFixResult (constraint postcondition, exprNode fcnCall) +{ + postcondition = constraint_copy (postcondition); + postcondition->lexpr = constraintExpr_doFixResult (postcondition->lexpr, fcnCall); + postcondition->expr = constraintExpr_doFixResult (postcondition->expr, fcnCall); + + return postcondition; +} + +constraint constraint_doSRefFixConstraintParam (constraint precondition, + exprNodeList arglist) +{ + + precondition = constraint_copy (precondition); + precondition->lexpr = constraintExpr_doSRefFixConstraintParam (precondition->lexpr, arglist); + precondition->expr = constraintExpr_doSRefFixConstraintParam (precondition->expr, arglist); + + return precondition; +} + // bool constraint_hasTerm (constraint c, constraintTerm term) // { // DPRINTF((message ("Constraint %s", constraint_print (c) ) ) );