X-Git-Url: http://andersk.mit.edu/gitweb/splint.git/blobdiff_plain/361091ccc3ff7e62a4817ef6400e752fef38f3c2..920a3797c23377bfb7332b0c11bda1d708cabb72:/src/constraint.c diff --git a/src/constraint.c b/src/constraint.c index f609083..3891247 100644 --- a/src/constraint.c +++ b/src/constraint.c @@ -1,7 +1,9 @@ /* -** constraintList.c +** constraint.c */ +//#define DEBUGPRINT 1 + # include /* for isdigit */ # include "lclintMacros.nf" # include "basic.h" @@ -11,37 +13,218 @@ # include "exprChecks.h" # include "aliasChecks.h" # include "exprNodeSList.h" -# include "exprData.i" /*@i33*/ /*@-fcnuse*/ /*@-assignexpose*/ -/*@notnull@*/ -/*@special@*/ constraint constraint_makeNew (void) - /*@post:isnull result->term, result->expr, result->constrType@*/ - /*@defines result->ar, result->post@*/; +/*@access exprNode @*/ + + +static /*@only@*/ cstring constraint_printDetailedPostCondition (/*@observer@*/ /*@temp@*/ constraint 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) */ + +/* { */ +/* 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) +{ + checkChar (s, '@'); +} + + + +constraint makeConstraintParse2 (constraintExpr l, lltok relOp, exprNode cconstant) +{ + char *t; + int c; + constraint ret; + ret = constraint_makeNew(); + llassert (l!=NULL); + + 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; + // ret->orig = ret; + DPRINTF(("GENERATED CONSTRAINT:")); + DPRINTF( (message ("%s", constraint_print(ret) ) ) ); + return ret; +} + +bool constraint_same (constraint c1, constraint c2) +{ + + if (c1->ar != c2->ar) + return FALSE; + + if (!constraintExpr_similar (c1->lexpr, c2->lexpr) ) + return FALSE; + + if (!constraintExpr_similar (c1->expr, c2->expr) ) + return FALSE; + + return TRUE; +} + +constraint makeConstraintParse3 (constraintExpr l, lltok relOp, constraintExpr r) +{ + constraint ret; + ret = constraint_makeNew(); + llassert (l !=NULL); + + 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") ); + + ret->expr = constraintExpr_copy (r); + + ret->post = TRUE; + + ret->orig = constraint_copy(ret); + + ret = constraint_simplify (ret); + + // ret->orig = ret; + DPRINTF(("GENERATED CONSTRAINT:")); + DPRINTF( (message ("%s", constraint_print(ret) ) ) ); + return ret; +} constraint constraint_copy (constraint c) { constraint ret; + + llassert (constraint_isDefined(c) ); + // TPRINTF((message("Copying constraint %q", constraint_print) )); + ret = constraint_makeNew(); - ret->lexpr = c->lexpr; + ret->lexpr = constraintExpr_copy (c->lexpr); ret->ar = c->ar; - ret->expr = c->expr; + ret->expr = constraintExpr_copy (c->expr); ret->post = c->post; + ret->generatingExpr = exprNode_fakeCopy(c->generatingExpr); + + /*@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); + else + ret->or = NULL; + + ret->fcnPre = c->fcnPre; + return ret; } -bool constraint_resolve (/*@unused@*/ constraint c) +/*like copy expect it doesn't allocate memory for the constraint*/ + +void constraint_overWrite (constraint c1, constraint c2) { - return FALSE; + llassert (constraint_isDefined(c1) ); + + llassert (c1 != c2); + + DPRINTF((message("OverWriteing constraint %q with %q", constraint_print(c1), + constraint_print(c2) ) )); + + constraintExpr_free(c1->lexpr); + constraintExpr_free(c1->expr); + + c1->lexpr = constraintExpr_copy (c2->lexpr); + c1->ar = c2->ar; + c1->expr = constraintExpr_copy (c2->expr); + c1->post = c2->post; + + if (c1->orig != NULL) + constraint_free (c1->orig); + + if (c2->orig != NULL) + c1->orig = constraint_copy (c2->orig); + else + c1->orig = NULL; + + /*@i33 make sure that the or is freed correctly*/ + if (c1->or != NULL) + constraint_free (c1->or); + + if (c2->or != NULL) + c1->or = constraint_copy (c2->or); + else + c1->or = NULL; + + c1->fcnPre = c2->fcnPre; + + c1->generatingExpr = c2->generatingExpr; } -/*@notnull@*/ -/*@special@*/ constraint constraint_makeNew (void) - /*@post:isnull result->term, result->expr, result->constrType@*/ - /*@defines result->ar, result->post@*/ + + +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 ret; ret = dmalloc(sizeof (*ret) ); @@ -49,127 +232,162 @@ bool constraint_resolve (/*@unused@*/ constraint c) ret->expr = NULL; ret->ar = LT; ret->post = FALSE; - /*@i23*/return ret; + ret->orig = NULL; + ret->or = NULL; + ret->generatingExpr = NULL; + ret->fcnPre = NULL; + return ret; } -/*@-czechfcns@*/ -constraintExpr constraintExpr_alloc () + +constraint constraint_addGeneratingExpr (/*@returned@*/ constraint c, exprNode e) { - constraintExpr ret; - ret = dmalloc (sizeof (*ret) ); - ret->term = NULL; - ret->expr = NULL; - ret->op = PLUS; - return ret; + + if (c->generatingExpr == NULL) + { + c->generatingExpr = exprNode_fakeCopy(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; } -constraintExpr constraintExpr_copy (constraintExpr expr) +constraint constraint_origAddGeneratingExpr (/*@returned@*/ constraint c, exprNode e) { - constraintExpr ret; - ret = constraintExpr_alloc(); - ret->term = constraintTerm_copy(expr->term); - ret->op = expr->op; - if (expr->expr != NULL) + + if (c->orig != constraint_undefined) { - ret->expr = constraintExpr_copy (expr->expr); + c->orig = constraint_addGeneratingExpr(c->orig, e); } else { - ret->expr = NULL; + DPRINTF ((message ("constraint_origAddGeneratingExpr: Not setting generatingExpr for %s to %s", constraint_print(c), exprNode_unparse(e) ) )); } - + return c; } -constraintExpr constraintExpr_makeMaxSetExpr (exprNode expr) +constraint constraint_setFcnPre (/*@returned@*/ constraint c ) { - constraintExpr ret; - ret = constraintExpr_alloc(); - ret->term = constraintTerm_makeMaxSetexpr(expr); - return ret; + + if (c->orig != constraint_undefined) + { + c->orig->fcnPre = TRUE; + } + else + { + c->fcnPre = TRUE; + // TPRINTF(( message("Warning Setting fcnPre directly") )); + } + return c; } -constraintExpr constraintExpr_makeMaxReadExpr (exprNode expr) + + + +fileloc constraint_getFileloc (constraint c) { - constraintExpr ret; - ret = constraintExpr_alloc(); - ret->term = constraintTerm_makeMaxReadexpr(expr); - return ret; + if (exprNode_isDefined(c->generatingExpr) ) + return (fileloc_copy (exprNode_getfileloc (c->generatingExpr) ) ); + + return (constraintExpr_getFileloc (c->lexpr) ); + + } -constraintExpr constraintExpr_makeMinSetExpr (exprNode expr) +static bool checkForMaxSet (constraint c) { - constraintExpr ret; - ret = constraintExpr_alloc(); - ret->term = constraintTerm_makeMinSetexpr(expr); - return ret; + if (constraintExpr_hasMaxSet(c->lexpr) || constraintExpr_hasMaxSet(c->expr) ) + return TRUE; + + return FALSE; } -constraintExpr constraintExpr_makeMinReadExpr (exprNode expr) +bool constraint_hasMaxSet(constraint c) { - constraintExpr ret; - ret = constraintExpr_alloc(); - ret->term = constraintTerm_makeMinReadexpr(expr); - return ret; + if (c->orig != NULL) + { + if (checkForMaxSet(c->orig) ) + return TRUE; + } + + return (checkForMaxSet(c) ); } -constraintExpr constraintExpr_makeValueExpr (exprNode expr) +constraint constraint_makeReadSafeExprNode ( exprNode po, exprNode ind) { - constraintExpr ret; - ret = constraintExpr_alloc(); - ret->term = constraintTerm_makeValueexpr(expr); + constraint ret = constraint_makeNew(); + // constraintTerm term; + po = exprNode_fakeCopy(po); + ind = exprNode_fakeCopy(ind); + ret->lexpr = constraintExpr_makeMaxReadExpr(po); + ret->ar = GTE; + ret->expr = constraintExpr_makeValueExpr (ind); + ret->post = FALSE; return ret; } - -constraintExpr makeConstraintExprIntlit (int i) +constraint constraint_makeWriteSafeInt (exprNode po, int ind) { - constraintExpr ret; - ret = dmalloc (sizeof (*ret) ); - ret->term = constraintTerm_makeIntLitValue(i); - ret->expr = NULL; - ret->op = PLUS; - /*@i1*/ return ret; -} + constraint ret = constraint_makeNew(); + + ret->lexpr =constraintExpr_makeMaxSetExpr(po); + ret->ar = GTE; + ret->expr = constraintExpr_makeIntLiteral (ind); + /*@i1*/return ret; +} -constraintExpr constraintExpr_makeValueInt (int i) +constraint constraint_makeSRefSetBufferSize (sRef s, long int size) { - return makeConstraintExprIntlit(i); + 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 constraint_makeWriteSafeExprNode (exprNode po, exprNode ind) +constraint constraint_makeSRefWriteSafeInt (sRef s, int ind) { constraint ret = constraint_makeNew(); - constraintTerm term; + - ret->lexpr =constraintExpr_makeMaxSetExpr(po); + ret->lexpr = constraintExpr_makeSRefMaxset ( s ); ret->ar = GTE; - ret->expr = constraintExpr_makeValueExpr (ind); + ret->expr = constraintExpr_makeIntLiteral (ind); + ret->post = TRUE; /*@i1*/return ret; } - -constraint constraint_makeReadSafeExprNode ( exprNode po, exprNode ind) + +/* drl added 01/12/2000 + + makes the constraint: Ensures index <= MaxRead(buffer) */ + +constraint constraint_makeEnsureLteMaxRead(exprNode index, exprNode buffer) { constraint ret = constraint_makeNew(); - // constraintTerm term; - po = exprNode_fakeCopy(po); - ind = exprNode_fakeCopy(ind); - ret->lexpr = constraintExpr_makeMaxReadExpr(po); - ret->ar = GTE; - ret->expr = constraintExpr_makeValueExpr (ind); + + ret->lexpr = constraintExpr_makeValueExpr (index); + ret->ar = LTE; + ret->expr = constraintExpr_makeMaxReadExpr(buffer); + ret->post = TRUE; return ret; } -constraint constraint_makeWriteSafeInt (exprNode po, int ind) +constraint constraint_makeWriteSafeExprNode (exprNode po, exprNode ind) { constraint ret = constraint_makeNew(); - constraintTerm term; + ret->lexpr =constraintExpr_makeMaxSetExpr(po); ret->ar = GTE; - ret->expr = constraintExpr_makeValueInt (ind); + ret->expr = constraintExpr_makeValueExpr (ind); /*@i1*/return ret; } - + + constraint constraint_makeReadSafeInt ( exprNode po, int ind) { constraint ret = constraint_makeNew(); @@ -178,105 +396,268 @@ constraint constraint_makeReadSafeInt ( exprNode po, int ind) ret->lexpr = constraintExpr_makeMaxReadExpr(po); ret->ar = GTE; - ret->expr = constraintExpr_makeValueInt (ind); + ret->expr = constraintExpr_makeIntLiteral (ind); + ret->post = FALSE; return ret; } -constraint constraint_makeEnsureMaxReadAtLeast (exprNode e1, exprNode t2, fileloc sequencePoint) +constraint constraint_makeSRefReadSafeInt (sRef s, int ind) { constraint ret = constraint_makeNew(); - constraintTerm term; + + + ret->lexpr = constraintExpr_makeSRefMaxRead (s ); + ret->ar = GTE; + ret->expr = constraintExpr_makeIntLiteral (ind); + ret->post = TRUE; + /*@i1*/return ret; +} + +constraint constraint_makeEnsureMaxReadAtLeast (exprNode e1, exprNode t2, fileloc sequencePoint) +{ + constraint ret; e1 = exprNode_fakeCopy (e1); t2 = exprNode_fakeCopy (t2); ret = constraint_makeReadSafeExprNode(e1, t2); - if (ret->lexpr->term->loc != NULL) - fileloc_free(ret->lexpr->term->loc); + + ret->lexpr = constraintExpr_setFileloc (ret->lexpr, sequencePoint); - ret->lexpr->term->loc = fileloc_copy (sequencePoint); ret->post = TRUE; - fileloc_incColumn (ret->lexpr->term->loc); + // fileloc_incColumn (ret->lexpr->term->loc); return ret; } - -constraint constraint_makeEnsureMinReadAtMost (exprNode po, exprNode ind, fileloc sequencePoint) +static constraint constraint_makeEnsuresOpConstraintExpr (/*@only@*/ constraintExpr c1, /*@only@*/ constraintExpr c2, fileloc sequencePoint, arithType ar) { - constraint ret = constraint_makeNew(); - constraintTerm term; - po = exprNode_fakeCopy(po); - ind = exprNode_fakeCopy(ind); - ret->lexpr = constraintExpr_makeMinReadExpr(po); - ret->ar = LTE; - ret->expr = constraintExpr_makeValueExpr (ind); - ret->post = TRUE; + constraint ret; + + llassert(c1 && c2); + // llassert(sequencePoint); - if (ret->lexpr->term->loc != NULL) - fileloc_free(ret->lexpr->term->loc); + ret = constraint_makeNew(); - ret->lexpr->term->loc = fileloc_copy (sequencePoint); - /*make this refer to element after preconditions */ - fileloc_incColumn (ret->lexpr->term->loc); - /*@i1*/ return ret; + ret->lexpr = c1; + ret->ar = ar; + ret->post = TRUE; + ret->expr = c2; + ret->lexpr = constraintExpr_setFileloc (ret->lexpr, sequencePoint); + return ret; } -constraintExpr makeMaxSetPostOpInc (exprNode e) +static constraint constraint_makeEnsuresOp (exprNode e1, exprNode e2, fileloc sequencePoint, arithType ar) { - constraintExpr ret; - ret = constraintExpr_makeValueExpr (e); - ret->term = constraintTerm_makeMaxSetexpr (e); - ret->op = MINUS; - ret->expr = makeConstraintExprIntlit (1); + constraintExpr c1, c2; + constraint ret; + exprNode e; + + if (! (e1 && e2) ) + { + llcontbug((message("null exprNode, Exprnodes are %s and %s", + exprNode_unparse(e1), exprNode_unparse(e2) ) + )); + } + + // llassert (sequencePoint); + + e = exprNode_fakeCopy(e1); + c1 = constraintExpr_makeValueExpr (e); + + e = exprNode_fakeCopy(e2); + c2 = constraintExpr_makeValueExpr (e); + + ret = constraint_makeEnsuresOpConstraintExpr (c1, c2, sequencePoint, ar); + return ret; } -constraint constraint_makeMaxSetSideEffectPostIncrement (exprNode e, fileloc sequencePoint) + +/* make constraint ensures e1 == e2 */ + +constraint constraint_makeEnsureEqual (exprNode e1, exprNode e2, fileloc sequencePoint) { - constraint ret = constraint_makeNew(); - //constraintTerm term; - exprNode t2; - e = exprNode_fakeCopy(e); - ret->lexpr = constraintExpr_makeMaxSetExpr(e); + return ( constraint_makeEnsuresOp (e1, e2, sequencePoint, EQ) ); +} + +/*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) */ + + t2 = constraintExpr_makeDecConstraintExpr (t2); + + return ( constraint_makeEnsuresOpConstraintExpr (t1, t2, sequencePoint, LTE) ); +} + +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) +{ + constraintExpr t1, t2; + + t1 = constraintExpr_makeValueExpr (e1); + t2 = constraintExpr_makeValueExpr (e2); + + + /* change this to e1 >= (e2 + 1) */ + t2 = constraintExpr_makeIncConstraintExpr (t2); + + + return ( constraint_makeEnsuresOpConstraintExpr (t1, t2, sequencePoint, GTE) ); +} + +constraint constraint_makeEnsureGreaterThanEqual (exprNode e1, exprNode e2, fileloc sequencePoint) +{ + return ( constraint_makeEnsuresOp (e1, e2, sequencePoint, GTE) ); +} + + +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) +{ + 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 = makeMaxSetPostOpInc(e); + ret->expr = constraintExpr_makeAddExpr (x2, y); + + ret->lexpr = constraintExpr_setFileloc (ret->lexpr, sequencePoint); - fileloc_incColumn ( ret->lexpr->term->loc); - fileloc_incColumn ( ret->lexpr->term->loc); return ret; } -constraintExpr makeMaxReadPostOpInc (exprNode e) + +/* Makes the constraint e = e - f */ +constraint constraint_makeSubtractAssign (exprNode e, exprNode f, fileloc sequencePoint) { - constraintExpr ret; - ret = constraintExpr_makeValueExpr (e); - ret->term = constraintTerm_makeMaxReadexpr (e); - ret->op = MINUS; - ret->expr = makeConstraintExprIntlit (1); + 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_makeMaxReadSideEffectPostIncrement (exprNode e, fileloc sequencePoint) +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; - exprNode t2; + e = exprNode_fakeCopy(e); - ret->lexpr = constraintExpr_makeMaxReadExpr(e); + ret->lexpr = constraintExpr_makeValueExpr (e); ret->ar = EQ; ret->post = TRUE; - ret->expr = makeMaxReadPostOpInc(e); + ret->expr = constraintExpr_makeValueExpr (e); + ret->expr = constraintExpr_makeIncConstraintExpr (ret->expr); - fileloc_incColumn ( ret->lexpr->term->loc); - fileloc_incColumn ( ret->lexpr->term->loc); + ret->lexpr = constraintExpr_setFileloc (ret->lexpr, sequencePoint); +// fileloc_incColumn ( ret->lexpr->term->loc); +// fileloc_incColumn ( ret->lexpr->term->loc); return ret; } -cstring arithType_print (arithType ar) +void constraint_free (/*@only@*/ constraint c) +{ + llassert(constraint_isDefined (c) ); + + + if (constraint_isDefined(c->orig) ) + constraint_free (c->orig); + if ( constraint_isDefined(c->or) ) + constraint_free (c->or); + + + constraintExpr_free(c->lexpr); + constraintExpr_free(c->expr); + + c->orig = NULL; + c->or = NULL; + c->lexpr = NULL; + c->expr = NULL; + + free (c); + +} + + +// 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) @@ -309,36 +690,165 @@ cstring arithType_print (arithType ar) return st; } -cstring constraintExpr_print (constraintExpr ex) +void constraint_printErrorPostCondition (constraint c, fileloc loc) { - cstring st; - cstring opStr; - llassert (ex != NULL); + cstring string; + fileloc errorLoc, temp; + + string = constraint_printDetailedPostCondition (c); + + errorLoc = loc; + + loc = NULL; - st = message ("%s", - constraintTerm_print (ex->term)); + 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; + fileloc errorLoc, temp; - if (ex->expr != NULL) + string = constraint_printDetailed (c); + + 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); + } + fileloc_free(temp); + } + else + { + if (c->post) + { + voptgenerror (FLG_FUNCTIONPOST, string, errorLoc); + } + else + { + voptgenerror (FLG_FUNCTIONCONSTRAINT, string, errorLoc); + } + } +} + + +cstring constraint_printDeep (constraint c) +{ + cstring st = cstring_undefined; + + st = constraint_print(c); + + if (c->orig != constraint_undefined) { - if (ex->op == PLUS) + if (!c->post) { - opStr = cstring_makeLiteral (" + "); + if (c->orig->fcnPre) + st = cstring_concatFree(st, (message(" derived from %s precondition: %q", exprNode_unparse(c->orig->generatingExpr), constraint_printDeep(c->orig) ) + ) ); + else + st = cstring_concatFree(st,(message(" needed to satisfy %q", + constraint_printDeep(c->orig) ) + ) ); + } else { - opStr = cstring_makeLiteral (" - "); + st = cstring_concatFree(st,(message("derived from: %q", + constraint_printDeep(c->orig) ) + ) ); + } + } + + return st; + +} + + +static /*@only@*/ cstring constraint_printDetailedPostCondition (/*@observer@*/ /*@temp@*/ constraint c) +{ + cstring st = cstring_undefined; + + st = message ("Unsatisfied ensures constraint condition:\nLCLint is unable to verify the constraint %q", constraint_printDeep (c) ); + + 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) ); + st = cstring_concatFree (st, temp); + + if (constraint_hasMaxSet(c) ) + { + temp = message ("Has MaxSet\n"); + st = cstring_concatFree (st, temp); } - st = message ("%s %s %s", st, opStr, constraintExpr_print (ex->expr) ); } return st; } +cstring constraint_printDetailed (constraint c) +{ + cstring st = cstring_undefined; + + 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) ); + } + + 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) ); + st = cstring_concatFree (st, temp); + + if (constraint_hasMaxSet(c) ) + { + temp = message ("Has MaxSet\n"); + st = cstring_concatFree (st, temp); + } + } + return st; +} -cstring constraint_print (constraint c) +/*@only@*/ cstring constraint_print (constraint c) /*@*/ { cstring st = cstring_undefined; cstring type = cstring_undefined; - llassert (c); + llassert (c !=NULL); if (c->post) { type = cstring_makeLiteral ("Ensures: "); @@ -347,7 +857,7 @@ cstring constraint_print (constraint c) { type = cstring_makeLiteral ("Requires: "); } - st = message ("%s: %s %s %s", + st = message ("%q: %q %q %q", type, constraintExpr_print (c->lexpr), arithType_print(c->ar), @@ -356,6 +866,216 @@ cstring constraint_print (constraint c) return st; } +cstring constraint_printOr (constraint c) /*@*/ +{ + cstring ret; + constraint temp; + + ret = cstring_undefined; + temp = c; + + ret = cstring_concatFree (ret, constraint_print(temp) ); + + temp = temp->or; + + while ( constraint_isDefined(temp) ) + { + ret = cstring_concatFree (ret, cstring_makeLiteral (" OR ") ); + ret = cstring_concatFree (ret, constraint_print(temp) ); + temp = temp->or; + } + + return ret; + +} + +/*@only@*/ constraint constraint_doSRefFixBaseParam (/*@returned@*/ /*@only@*/ constraint precondition, + exprNodeList arglist) +{ + precondition->lexpr = constraintExpr_doSRefFixBaseParam (precondition->lexpr, + arglist); + precondition->expr = constraintExpr_doSRefFixBaseParam (precondition->expr, + arglist); + + return 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; +} + +/*@only@*/ 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); + + precondition->fcnPre = FALSE; + 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 @*/ +{ + + DPRINTF( (message("Doing constraint_preserverOrig for %q ", constraint_printDetailed(c) ) )); + + if (c->orig == constraint_undefined) + c->orig = constraint_copy (c); + + else if (c->orig->fcnPre) + { + constraint temp; + + temp = c->orig; + + /* avoid infinite loop */ + c->orig = NULL; + c->orig = constraint_copy (c); + 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 + { + DPRINTF( (message("Not changing constraint") )); + } + + DPRINTF( (message("After Doing constraint_preserverOrig for %q ", constraint_printDetailed(c) ) )); + + return c; +} /*@=fcnuse*/ /*@=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; + // /*@kept@*/ exprNode generatingExpr; + + 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) getInt (&s); + advanceField(&s); + post = (bool) getInt (&s); + advanceField(&s); + ar = (arithType) getInt (&s); + + s = fgets(os, MAX_DUMP_LINE_LENGTH, f); + + checkChar (&s, 'l'); + + lexpr = constraintExpr_undump (f); + + s = fgets(os, MAX_DUMP_LINE_LENGTH, f); + + 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); + return c; +} + + +void constraint_dump (/*@observer@*/ constraint c, FILE *f) +{ + bool fcnPre; + bool post; + arithType ar; + + constraintExpr lexpr; + constraintExpr expr; + // /*@kept@*/ exprNode generatingExpr; + + 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); +} + +