X-Git-Url: http://andersk.mit.edu/gitweb/splint.git/blobdiff_plain/77d3741943947b83a5d6a10a5e31650a1005dbde..312c981596ce6202de7686f2d4c46aec1bae3939:/src/constraintGeneration.c diff --git a/src/constraintGeneration.c b/src/constraintGeneration.c index b027abe..dfb737d 100644 --- a/src/constraintGeneration.c +++ b/src/constraintGeneration.c @@ -17,8 +17,8 @@ ** the Free Software Foundation, Inc., 59 Temple Place - Suite 330, Boston, ** MA 02111-1307, USA. ** -** For information on lclint: lclint-request@cs.virginia.edu -** To report a bug: lclint-bug@cs.virginia.edu +** For information on splint: info@splint.org +** To report a bug: splint-bug@splint.org ** For more information: http://www.splint.org */ @@ -29,7 +29,7 @@ /* #define DEBUGPRINT 1 */ # include /* for isdigit */ -# include "lclintMacros.nf" +# include "splintMacros.nf" # include "basic.h" # include "cgrammar_tokens.h" @@ -37,24 +37,26 @@ # include "exprChecks.h" # include "exprNodeSList.h" -/*@access exprNode @*/ +/*@access exprNode@*/ /* NO! Don't do this recklessly! */ +/*@-nullderef@*/ /* DRL needs to fix this code! */ +/*@-nullpass@*/ /* DRL needs to fix this code! */ +/*@-temptrans@*/ /* DRL needs to fix this code! */ +static /*@truewhennull@*/ bool exprNode_handleError (/*@temp@*/ exprNode p_e); -static bool exprNode_handleError(/*@dependent@*/ exprNode p_e); +static void exprNode_stmt (/*@temp@*/ /*@temp@*/ exprNode p_e); +static void exprNode_multiStatement (/*@temp@*/ exprNode p_e); -static bool exprNode_isMultiStatement(/*@dependent@*/ exprNode p_e); -static void exprNode_multiStatement (/*@dependent@*/ exprNode p_e); - -static constraintList exprNode_traversTrueEnsuresConstraints (/*@dependent@*/ exprNode p_e); -static constraintList exprNode_traversFalseEnsuresConstraints (/*@dependent@*/ exprNode p_e); +static constraintList exprNode_traversTrueEnsuresConstraints (/*@temp@*/ exprNode p_e); +static constraintList exprNode_traversFalseEnsuresConstraints (/*@temp@*/ exprNode p_e); static void checkArgumentList (/*@out@*/ exprNode p_temp, exprNodeList p_arglist, fileloc p_sequencePoint) /*@modifies p_temp @*/; -static constraintList checkCall (/*@dependent@*/ exprNode p_fcn, exprNodeList p_arglist); +static constraintList checkCall (/*@temp@*/ exprNode p_fcn, exprNodeList p_arglist); -static bool exprNode_isUnhandled (/*@dependent@*/ /*@observer@*/ exprNode e) +static bool exprNode_isUnhandled (/*@temp@*/ /*@observer@*/ exprNode e) { - llassert( exprNode_isDefined(e) ); + llassert(exprNode_isDefined(e)); switch (e->kind) { case XPR_INITBLOCK: @@ -80,7 +82,7 @@ static bool exprNode_isUnhandled (/*@dependent@*/ /*@observer@*/ exprNode e) case XPR_FTCASE: case XPR_CASE: case XPR_NODE: - DPRINTF((message ("Warning current constraint generation does not handle expression %s", exprNode_unparse(e)) ) ); + DPRINTF((message ("Warning current constraint generation does not handle expression %s", exprNode_unparse(e)))); return TRUE; /*@notreached@*/ break; @@ -92,49 +94,47 @@ static bool exprNode_isUnhandled (/*@dependent@*/ /*@observer@*/ exprNode e) return FALSE; } -bool exprNode_handleError( exprNode e) +bool exprNode_handleError (exprNode e) { - if (exprNode_isError (e) || exprNode_isUnhandled(e) ) + if (exprNode_isError (e) || exprNode_isUnhandled (e)) { - static /*@only@*/ cstring error = cstring_undefined; - - if (!cstring_isDefined (error)) - { - error = cstring_makeLiteral (""); - } - - /*@-unqualifiedtrans*/ return TRUE; /*@=unqualifiedtrans*/ + return TRUE; } + return FALSE; } -bool /*@alt void@*/ exprNode_generateConstraints (/*@dependent@*/ exprNode e) +/* evans 2002-03-2 - parameter was dependent */ +bool /*@alt void@*/ exprNode_generateConstraints (/*@temp@*/ exprNode e) { - if (exprNode_isError (e) ) + if (exprNode_isError (e)) return FALSE; - if (exprNode_isUnhandled (e) ) + if (exprNode_isUnhandled (e)) { - DPRINTF( (message("Warning ignoring %s", exprNode_unparse (e) ) ) ); - return FALSE; + DPRINTF((message("Warning ignoring %s", exprNode_unparse (e)))); + return FALSE; } - DPRINTF((message ("exprNode_generateConstraints Analysising %s at %s", exprNode_unparse( e), - fileloc_unparse(exprNode_getfileloc(e) ) ) ) ); + DPRINTF((message ("exprNode_generateConstraints Analysising %s at %s", exprNode_unparse(e), + fileloc_unparse(exprNode_getfileloc(e))))); - if (exprNode_isMultiStatement ( e) ) + if (exprNode_isMultiStatement (e)) { exprNode_multiStatement(e); } else { - fileloc loc; +/* fileloc loc; */ - loc = exprNode_getNextSequencePoint(e); - exprNode_exprTraverse(e, FALSE, FALSE, loc); +/* loc = exprNode_getNextSequencePoint(e); */ +/* exprNode_exprTraverse(e, FALSE, FALSE, loc); */ - fileloc_free(loc); +/* fileloc_free(loc); */ + + exprNode_stmt(e); return FALSE; + } { @@ -145,45 +145,17 @@ bool /*@alt void@*/ exprNode_generateConstraints (/*@dependent@*/ exprNode e) constraintList_free(c); } - DPRINTF ( (message ("e->requiresConstraints %s", constraintList_printDetailed (e->requiresConstraints) ) ) ); + DPRINTF ((message ("e->requiresConstraints %s", constraintList_printDetailed (e->requiresConstraints)))); return FALSE; } - -/* handles multiple statements */ - -bool exprNode_isMultiStatement(exprNode e) -{ -if (exprNode_handleError (e) != NULL) - return FALSE; - - switch (e->kind) - { - case XPR_FOR: - case XPR_FORPRED: - case XPR_IF: - case XPR_IFELSE: - case XPR_WHILE: - case XPR_WHILEPRED: - case XPR_DOWHILE: - case XPR_BLOCK: - case XPR_STMT: - case XPR_STMTLIST: - case XPR_SWITCH: - return TRUE; - default: - return FALSE; - } - -} - -static void exprNode_stmt ( /*@dependent@*/ /*@temp@*/ exprNode e) +static void exprNode_stmt (/*@temp@*/ exprNode e) { exprNode snode; fileloc loc; cstring s; - if (exprNode_isError(e) ) + if (exprNode_isError(e)) { return; } @@ -191,15 +163,15 @@ static void exprNode_stmt ( /*@dependent@*/ /*@temp@*/ exprNode e) /*e->requiresConstraints = constraintList_makeNew(); e->ensuresConstraints = constraintList_makeNew(); */ - DPRINTF(( "expNode_stmt: STMT:") ); + DPRINTF(("expNode_stmt: STMT:")); s = exprNode_unparse(e); - DPRINTF ( ( message("exprNode_stmt: STMT: %s ", s) ) ); + DPRINTF ((message("exprNode_stmt: STMT: %s ", s))); if (e->kind == XPR_INIT) { constraintList tempList; - DPRINTF (("Init") ); - DPRINTF ( (message ("%s ", exprNode_unparse (e)) ) ); + DPRINTF (("Init")); + DPRINTF ((message ("%s ", exprNode_unparse (e)))); loc = exprNode_getNextSequencePoint(e); /* reduces to an expression */ exprNode_exprTraverse (e, FALSE, FALSE, loc); fileloc_free(loc); @@ -213,24 +185,46 @@ static void exprNode_stmt ( /*@dependent@*/ /*@temp@*/ exprNode e) constraintList_free(tempList); return; } + + /*drl 2/13/002 patched bug so return statement will be checked*/ + /*return is a stmt not not expression ...*/ + if (e->kind == XPR_RETURN) + { + constraintList tempList; + + loc = exprNode_getNextSequencePoint(e); /* reduces to an expression */ + + exprNode_exprTraverse (exprData_getSingle (e->edata), FALSE, TRUE, loc); + fileloc_free(loc); + + tempList = e->requiresConstraints; + e->requiresConstraints = exprNode_traversRequiresConstraints(e); + constraintList_free(tempList); + } if (e->kind != XPR_STMT) { - DPRINTF (("Not Stmt") ); - DPRINTF ( (message ("%s ", exprNode_unparse (e)) ) ); + DPRINTF (("Not Stmt")); + DPRINTF ((message ("%s ", exprNode_unparse (e)))); if (exprNode_isMultiStatement (e)) { exprNode_multiStatement (e); /* evans 2001-08-21: spurious return removed */ } - - DPRINTF( (message ("Ignoring non-statement %s", exprNode_unparse(e) ) ) ); - return; + else + { + loc = exprNode_getNextSequencePoint(e); /* reduces to an expression */ + + exprNode_exprTraverse (e, FALSE, TRUE, loc); + fileloc_free(loc); + + } + return; } - DPRINTF (("Stmt") ); - DPRINTF ( (message ("%s ", exprNode_unparse (e)) ) ); + DPRINTF (("Stmt")); + DPRINTF ((message ("%s ", exprNode_unparse (e)))); snode = exprData_getUopNode (e->edata); @@ -256,9 +250,9 @@ static void exprNode_stmt ( /*@dependent@*/ /*@temp@*/ exprNode e) constraintList_free (e->ensuresConstraints); e->ensuresConstraints = exprNode_traversEnsuresConstraints(snode); - DPRINTF ( (message ("smtlist constraints are: pre: %s \n and \t post %s\n", + DPRINTF ((message ("smtlist constraints are: pre: %s \n and \t post %s\n", constraintList_print(e->requiresConstraints), - constraintList_print(e->ensuresConstraints) ) ) ); + constraintList_print(e->ensuresConstraints)))); return; } @@ -266,7 +260,7 @@ static void exprNode_stmt ( /*@dependent@*/ /*@temp@*/ exprNode e) static void exprNode_stmtList (/*@dependent@*/ exprNode e) { exprNode stmt1, stmt2; - if (exprNode_isError (e) ) + if (exprNode_isError (e)) { return; } @@ -282,24 +276,24 @@ static void exprNode_stmtList (/*@dependent@*/ exprNode e) return; } llassert (e->kind == XPR_STMTLIST); - DPRINTF(( "exprNode_stmtList STMTLIST:") ); - DPRINTF ((cstring_toCharsSafe (exprNode_unparse(e)) ) ); + DPRINTF(("exprNode_stmtList STMTLIST:")); + DPRINTF ((cstring_toCharsSafe (exprNode_unparse(e)))); stmt1 = exprData_getPairA (e->edata); stmt2 = exprData_getPairB (e->edata); - DPRINTF(("exprNode_stmtlist ") ); - DPRINTF ((message("XW%s | %s", exprNode_unparse(stmt1), exprNode_unparse(stmt2) ) ) ); + DPRINTF(("exprNode_stmtlist ")); + DPRINTF ((message("XW%s | %s", exprNode_unparse(stmt1), exprNode_unparse(stmt2)))); exprNode_stmt (stmt1); - DPRINTF(("\nstmt after stmtList call " )); + DPRINTF(("\nstmt after stmtList call ")); exprNode_stmt (stmt2); - exprNode_mergeResolve (e, stmt1, stmt2 ); + exprNode_mergeResolve (e, stmt1, stmt2); - DPRINTF ( (message ("smtlist constraints are: pre: %s \n and \t post %s\n", + DPRINTF ((message ("smtlist constraints are: pre: %s \n and \t post %s\n", constraintList_print(e->requiresConstraints), - constraintList_print(e->ensuresConstraints) ) ) ); + constraintList_print(e->ensuresConstraints)))); return; } @@ -307,30 +301,30 @@ static exprNode doIf (/*@returned@*/ exprNode e, /*@dependent@*/ exprNode test, { constraintList temp; - DPRINTF ((message ("doIf: %s ", exprNode_unparse(e) ) ) ); + DPRINTF ((message ("doIf: %s ", exprNode_unparse(e)))); - llassert(exprNode_isDefined(test) ); - llassert (exprNode_isDefined (e) ); - llassert (exprNode_isDefined (body) ); + llassert(exprNode_isDefined(test)); + llassert (exprNode_isDefined (e)); + llassert (exprNode_isDefined (body)); - DPRINTF((message ("ensures constraints for %s are %s", exprNode_unparse(e), constraintList_printDetailed(e->ensuresConstraints) ) )); + DPRINTF((message ("ensures constraints for %s are %s", exprNode_unparse(e), constraintList_printDetailed(e->ensuresConstraints)))); - DPRINTF((message ("Requires constraints for %s are %s", exprNode_unparse(e), constraintList_printDetailed(e->ensuresConstraints) ) )); + DPRINTF((message ("Requires constraints for %s are %s", exprNode_unparse(e), constraintList_printDetailed(e->ensuresConstraints)))); - DPRINTF((message ("trueEnsures constraints for %s are %s", exprNode_unparse(e), constraintList_printDetailed(e->trueEnsuresConstraints) ) )); + DPRINTF((message ("trueEnsures constraints for %s are %s", exprNode_unparse(e), constraintList_printDetailed(e->trueEnsuresConstraints)))); - DPRINTF((message ("falseEnsures constraints for %s are %s", exprNode_unparse(e), constraintList_printDetailed(e->falseEnsuresConstraints) ) )); + DPRINTF((message ("falseEnsures constraints for %s are %s", exprNode_unparse(e), constraintList_printDetailed(e->falseEnsuresConstraints)))); - DPRINTF((message ("ensures constraints for %s are %s", exprNode_unparse(test), constraintList_printDetailed(test->ensuresConstraints) ) )); + DPRINTF((message ("ensures constraints for %s are %s", exprNode_unparse(test), constraintList_printDetailed(test->ensuresConstraints)))); - DPRINTF((message ("Requires constraints for %s are %s", exprNode_unparse(test), constraintList_printDetailed(test->ensuresConstraints) ) )); + DPRINTF((message ("Requires constraints for %s are %s", exprNode_unparse(test), constraintList_printDetailed(test->ensuresConstraints)))); - DPRINTF((message ("trueEnsures constraints for %s are %s", exprNode_unparse(test), constraintList_printDetailed(test->trueEnsuresConstraints) ) )); + DPRINTF((message ("trueEnsures constraints for %s are %s", exprNode_unparse(test), constraintList_printDetailed(test->trueEnsuresConstraints)))); - DPRINTF((message ("falseEnsures constraints for %s are %s", exprNode_unparse(test), constraintList_printDetailed(test->falseEnsuresConstraints) ) )); + DPRINTF((message ("falseEnsures constraints for %s are %s", exprNode_unparse(test), constraintList_printDetailed(test->falseEnsuresConstraints)))); @@ -349,9 +343,9 @@ static exprNode doIf (/*@returned@*/ exprNode e, /*@dependent@*/ exprNode test, test->trueEnsuresConstraints = constraintList_substituteFreeTarget(test->trueEnsuresConstraints, test->ensuresConstraints); - DPRINTF ((message ("doIf: test ensures %s ", constraintList_print(test->ensuresConstraints) ) ) ); + DPRINTF ((message ("doIf: test ensures %s ", constraintList_print(test->ensuresConstraints)))); - DPRINTF ((message ("doIf: test true ensures %s ", constraintList_print(test->trueEnsuresConstraints) ) ) ); + DPRINTF ((message ("doIf: test true ensures %s ", constraintList_print(test->trueEnsuresConstraints)))); constraintList_free(e->requiresConstraints); @@ -369,14 +363,14 @@ static exprNode doIf (/*@returned@*/ exprNode e, /*@dependent@*/ exprNode test, constraintList_free(e->ensuresConstraints); e->ensuresConstraints = constraintList_copy (test->ensuresConstraints); - if (exprNode_mayEscape (body) ) + if (exprNode_mayEscape (body)) { - DPRINTF (( message("doIf: the if statement body %s returns or exits", exprNode_unparse(body) ) )); + DPRINTF ((message("doIf: the if statement body %s returns or exits", exprNode_unparse(body)))); e->ensuresConstraints = constraintList_mergeEnsuresFreeFirst (e->ensuresConstraints, test->falseEnsuresConstraints); } - DPRINTF ((message ("doIf: if requiers %s ", constraintList_print(e->requiresConstraints) ) ) ); + DPRINTF ((message ("doIf: if requiers %s ", constraintList_print(e->requiresConstraints)))); return e; } @@ -391,12 +385,15 @@ static exprNode doIf (/*@returned@*/ exprNode e, /*@dependent@*/ exprNode test, exprNode_traversFalseEnsuresConstraints have all been run */ - static exprNode doIfElse (/*@returned@*/ exprNode e, /*@dependent@*/ exprNode p, /*@dependent@*/ exprNode trueBranch, /*@dependent@*/ exprNode falseBranch) { constraintList c1, cons, t, t2, f, f2; - DPRINTF ((message ("doIfElse: %s ", exprNode_unparse(e) ) ) ); + llassert (exprNode_isDefined (e)); + llassert (exprNode_isDefined (p)); + llassert (exprNode_isDefined (trueBranch)); + llassert (exprNode_isDefined (falseBranch)); + DPRINTF ((message ("doIfElse: %s ", exprNode_unparse(e)))); /* do requires clauses */ c1 = constraintList_copy (p->ensuresConstraints); @@ -407,7 +404,7 @@ static exprNode doIfElse (/*@returned@*/ exprNode e, /*@dependent@*/ exprNode p, cons = constraintList_reflectChanges(falseBranch->requiresConstraints, p->falseEnsuresConstraints); cons = constraintList_reflectChangesFreePre (cons, c1); - constraintList_free(e->requiresConstraints); + constraintList_free (e->requiresConstraints); e->requiresConstraints = constraintList_mergeRequiresFreeFirst (t, cons); e->requiresConstraints = constraintList_mergeRequiresFreeFirst (e->requiresConstraints, p->requiresConstraints); @@ -436,15 +433,15 @@ static exprNode doIfElse (/*@returned@*/ exprNode e, /*@dependent@*/ exprNode p, constraintList_free(cons); constraintList_free(c1); - DPRINTF ((message ("doIfElse: if requires %q ", constraintList_print(e->requiresConstraints) ) ) ); - DPRINTF ((message ("doIfElse: if ensures %q ", constraintList_print(e->ensuresConstraints) ) ) ); + DPRINTF ((message ("doIfElse: if requires %q ", constraintList_print(e->requiresConstraints)))); + DPRINTF ((message ("doIfElse: if ensures %q ", constraintList_print(e->ensuresConstraints)))); return e; } static exprNode doWhile (/*@returned@*/ exprNode e, /*@dependent@*/ exprNode test, /*@dependent@*/ exprNode body) { - DPRINTF ((message ("doWhile: %s ", exprNode_unparse(e) ) ) ); + DPRINTF ((message ("doWhile: %s ", exprNode_unparse(e)))); return doIf (e, test, body); } @@ -456,28 +453,28 @@ static exprNode doWhile (/*@returned@*/ exprNode e, /*@dependent@*/ exprNode tes sRefSet_elements (s, el) { - if (sRef_isFixedArray(el) ) + if (sRef_isFixedArray(el)) { - long int size; - DPRINTF( (message("%s is a fixed array", - sRef_unparse(el)) ) ); + size_t size; + DPRINTF((message("%s is a fixed array", + sRef_unparse(el)))); size = sRef_getArraySize(el); - DPRINTF( (message("%s is a fixed array with size %d", - sRef_unparse(el), (int)size) ) ); + DPRINTF((message("%s is a fixed array with size %d", + sRef_unparse(el), (int)size))); con = constraint_makeSRefSetBufferSize (el, (size - 1)); ret = constraintList_add(ret, con); } else { - DPRINTF( (message("%s is not a fixed array", - sRef_unparse(el)) ) ); + DPRINTF((message("%s is not a fixed array", + sRef_unparse(el)))); - if (sRef_isExternallyVisible (el) ) + if (sRef_isExternallyVisible (el)) { /* - DPRINTF( (message("%s is externally visible", - sRef_unparse(el) ) )); + DPRINTF((message("%s is externally visible", + sRef_unparse(el)))); con = constraint_makeSRefWriteSafeInt(el, 0); ret = constraintList_add(ret, con); @@ -490,8 +487,8 @@ static exprNode doWhile (/*@returned@*/ exprNode e, /*@dependent@*/ exprNode tes } end_sRefSet_elements ; - DPRINTF(( message("constraintList_makeFixedArrayConstraints returning %s", - constraintList_print(ret) ) )); + DPRINTF((message("constraintList_makeFixedArrayConstraints returning %s", + constraintList_print(ret)))); return ret; } @@ -514,17 +511,22 @@ static void doFor (/*@dependent@*/ exprNode e, /*@dependent@*/ exprNode forPred, exprNode init, test, inc; /* merge the constraints: modle as if statement */ - /* init - if (test) - for body - inc */ - init = exprData_getTripleInit (forPred->edata); - test = exprData_getTripleTest (forPred->edata); - inc = exprData_getTripleInc (forPred->edata); + /* init + if (test) + for body + inc */ - if ( ( (exprNode_isError (test) /*|| (exprNode_isError(init) )*/ ) || (exprNode_isError (inc) ) ) ) + llassert (exprNode_isDefined (e)); + llassert (exprNode_isDefined (forPred)); + llassert (exprNode_isDefined (forBody)); + + init = exprData_getTripleInit (forPred->edata); + test = exprData_getTripleTest (forPred->edata); + inc = exprData_getTripleInc (forPred->edata); + + if (((exprNode_isError (test) /*|| (exprNode_isError(init))*/) || (exprNode_isError (inc)))) { - DPRINTF ((message ("strange for statement:%s, ignoring it", exprNode_unparse(e) ) ) ); + DPRINTF ((message ("strange for statement:%s, ignoring it", exprNode_unparse(e)))); return; } @@ -537,50 +539,54 @@ static void doFor (/*@dependent@*/ exprNode e, /*@dependent@*/ exprNode forPred, if (!forBody->canBreak) { - e->ensuresConstraints = constraintList_addListFree(e->ensuresConstraints, constraintList_copy(forPred->ensuresConstraints) ); - e->ensuresConstraints = constraintList_addListFree(e->ensuresConstraints,constraintList_copy( test->falseEnsuresConstraints)); + e->ensuresConstraints = constraintList_addListFree(e->ensuresConstraints, constraintList_copy(forPred->ensuresConstraints)); + e->ensuresConstraints = constraintList_addListFree(e->ensuresConstraints,constraintList_copy(test->falseEnsuresConstraints)); } else { - DPRINTF(("Can break") ); + DPRINTF(("Can break")); } } static /*@dependent@*/ exprNode exprNode_makeDependent(/*@returned@*/ exprNode e) { - /*@-temptrans@*/ + /* !!! DRL - this is ridiculous! Read the manual on memory annotations please! */ return e; - /*@=temptrans@*/ } -static void exprNode_doGenerateConstraintSwitch (/*@dependent@*/ exprNode switchExpr, - /*@dependent@*/ exprNode body, /*@special@*/ constraintList * currentRequires, /*@special@*/ constraintList * - currentEnsures, /*@special@*/ constraintList * savedRequires, /*@special@*/ constraintList * - savedEnsures) - /*@post:only *currentRequires, *currentEnsures, *savedRequires, *savedEnsures @*/ /*@defines *currentRequires, *currentEnsures, *savedRequires, *savedEnsures @*/ +static void +exprNode_doGenerateConstraintSwitch + (/*@dependent@*/ exprNode switchExpr, + /*@dependent@*/ exprNode body, + /*@special@*/ constraintList *currentRequires, + /*@special@*/ constraintList *currentEnsures, + /*@special@*/ constraintList *savedRequires, + /*@special@*/ constraintList *savedEnsures) + /*@post:only *currentRequires, *currentEnsures, *savedRequires, *savedEnsures @*/ + /*@sets *currentRequires, *currentEnsures, *savedRequires, *savedEnsures @*/ { exprNode stmt, stmtList; - DPRINTF(( message("exprNode_doGenerateConstraintSwitch: (switch %s) %s", + DPRINTF((message("exprNode_doGenerateConstraintSwitch: (switch %s) %s", exprNode_unparse(switchExpr), exprNode_unparse(body) - ) )); + ))); - if (exprNode_isError(body) ) + if (exprNode_isError(body)) { - *currentRequires = constraintList_makeNew(); - *currentEnsures = constraintList_makeNew(); + *currentRequires = constraintList_makeNew (); + *currentEnsures = constraintList_makeNew (); - *savedRequires = constraintList_makeNew(); - *savedEnsures = constraintList_makeNew(); + *savedRequires = constraintList_makeNew (); + *savedEnsures = constraintList_makeNew (); /*@-onlytrans@*/ return; /*@=onlytrans@*/ } - if (body->kind != XPR_STMTLIST ) + if (body->kind != XPR_STMTLIST) { DPRINTF((message("exprNode_doGenerateConstraintSwitch: non stmtlist: %s", - exprNode_unparse(body) ))); + exprNode_unparse(body)))); stmt = body; stmtList = exprNode_undefined; stmt = exprNode_makeDependent(stmt); @@ -595,14 +601,14 @@ static void exprNode_doGenerateConstraintSwitch (/*@dependent@*/ exprNode switch } DPRINTF((message("exprNode_doGenerateConstraintSwitch: stmtlist: %s stmt: %s", - exprNode_unparse(stmtList), exprNode_unparse(stmt) ) - )); + exprNode_unparse(stmtList), exprNode_unparse(stmt)) + )); exprNode_doGenerateConstraintSwitch (switchExpr, stmtList, currentRequires, currentEnsures, - savedRequires, savedEnsures ); + savedRequires, savedEnsures); - if (exprNode_isError(stmt) ) + if (exprNode_isError(stmt)) /*@-onlytrans@*/ return; /*@=onlytrans@*/ @@ -611,13 +617,13 @@ static void exprNode_doGenerateConstraintSwitch (/*@dependent@*/ exprNode switch switchExpr = exprNode_makeDependent (switchExpr); - if (! exprNode_isCaseMarker(stmt) ) + if (! exprNode_isCaseMarker(stmt)) { constraintList temp; - DPRINTF (( message("Got normal statement %s (requires %s ensures %s)", exprNode_unparse(stmt), - constraintList_unparse(stmt->requiresConstraints), constraintList_unparse(stmt->ensuresConstraints) ) )); + DPRINTF ((message("Got normal statement %s (requires %s ensures %s)", exprNode_unparse(stmt), + constraintList_unparse(stmt->requiresConstraints), constraintList_unparse(stmt->ensuresConstraints)))); temp = constraintList_reflectChanges (stmt->requiresConstraints, *currentEnsures); @@ -631,18 +637,18 @@ static void exprNode_doGenerateConstraintSwitch (/*@dependent@*/ exprNode switch *currentEnsures = constraintList_mergeEnsuresFreeFirst (*currentEnsures, stmt->ensuresConstraints); - DPRINTF(( message("returning from exprNode_doGenerateConstraintSwitch: (switch %s) %s currentRequires:" + DPRINTF((message("returning from exprNode_doGenerateConstraintSwitch: (switch %s) %s currentRequires:" "%s currentEnsures:%s", exprNode_unparse(switchExpr), exprNode_unparse(body), constraintList_print(*currentRequires), constraintList_print(*currentEnsures) - ) )); + ))); /*@-onlytrans@*/ return; /*@=onlytrans@*/ } - if (exprNode_isCaseMarker(stmt) && exprNode_mustEscape(stmtList) ) + if (exprNode_isCaseMarker(stmt) && exprNode_mustEscape(stmtList)) { /* ** merge current and saved constraint with Logical Or... @@ -652,19 +658,19 @@ static void exprNode_doGenerateConstraintSwitch (/*@dependent@*/ exprNode switch constraintList temp; constraint con; - DPRINTF (( message("Got case marker") )); + DPRINTF ((message("Got case marker"))); if (constraintList_isUndefined(*savedEnsures) && - constraintList_isUndefined(*savedRequires) ) + constraintList_isUndefined(*savedRequires)) { - llassert(constraintList_isUndefined(*savedEnsures) ); - llassert(constraintList_isUndefined(*savedRequires) ); + llassert(constraintList_isUndefined(*savedEnsures)); + llassert(constraintList_isUndefined(*savedRequires)); *savedEnsures = constraintList_copy(*currentEnsures); *savedRequires = constraintList_copy(*currentRequires); } else { - DPRINTF (( message("Doing logical or") )); + DPRINTF ((message("Doing logical or"))); temp = constraintList_logicalOr (*savedEnsures, *currentEnsures); constraintList_free (*savedEnsures); *savedEnsures = temp; @@ -673,7 +679,7 @@ static void exprNode_doGenerateConstraintSwitch (/*@dependent@*/ exprNode switch } con = constraint_makeEnsureEqual (switchExpr, exprData_getSingle - (stmt->edata), exprNode_getfileloc(stmt) ); + (stmt->edata), exprNode_getfileloc(stmt)); constraintList_free(*currentEnsures); @@ -682,15 +688,15 @@ static void exprNode_doGenerateConstraintSwitch (/*@dependent@*/ exprNode switch constraintList_free(*currentRequires); *currentRequires = constraintList_makeNew(); - DPRINTF(( message("exprNode_doGenerateConstraintSwitch: (switch %s) %s savedRequires:" + DPRINTF((message("exprNode_doGenerateConstraintSwitch: (switch %s) %s savedRequires:" "%s savedEnsures:%s", exprNode_unparse(switchExpr), exprNode_unparse(body), constraintList_print(*savedRequires), constraintList_print(*savedEnsures) - ) )); + ))); } - else if (exprNode_isCaseMarker(stmt) ) + else if (exprNode_isCaseMarker(stmt)) /* prior case has no break. */ { /* @@ -704,16 +710,16 @@ static void exprNode_doGenerateConstraintSwitch (/*@dependent@*/ exprNode switch constraintList ensuresTemp; - DPRINTF (( message("Got case marker with no prior break") )); + DPRINTF ((message("Got case marker with no prior break"))); con = constraint_makeEnsureEqual (switchExpr, exprData_getSingle - (stmt->edata), exprNode_getfileloc(stmt) ); + (stmt->edata), exprNode_getfileloc(stmt)); ensuresTemp = constraintList_makeNew(); ensuresTemp = constraintList_add (ensuresTemp, con); - if (exprNode_isError(stmtList) ) + if (exprNode_isError(stmtList)) { constraintList_free(*currentEnsures); @@ -744,19 +750,18 @@ static void exprNode_doGenerateConstraintSwitch (/*@dependent@*/ exprNode switch BADEXIT; } - DPRINTF(( message("returning from exprNode_doGenerateConstraintSwitch: (switch %s) %s currentRequires:" + DPRINTF((message("returning from exprNode_doGenerateConstraintSwitch: (switch %s) %s currentRequires:" "%s currentEnsures:%s", exprNode_unparse(switchExpr), exprNode_unparse(body), constraintList_print(*currentRequires), constraintList_print(*currentEnsures) - ) )); + ))); /*@-onlytrans@*/ return; /*@=onlytrans@*/ - } -static void exprNode_generateConstraintSwitch ( exprNode switchStmt) +static void exprNode_generateConstraintSwitch (/*@notnull@*/ exprNode switchStmt) { constraintList constraintsRequires; constraintList constraintsEnsures; @@ -766,13 +771,18 @@ static void exprNode_generateConstraintSwitch ( exprNode switchStmt) exprNode body; exprNode switchExpr; - switchExpr = exprData_getPairA(switchStmt->edata); - body = exprData_getPairB(switchStmt->edata); + switchExpr = exprData_getPairA (switchStmt->edata); + body = exprData_getPairB (switchStmt->edata); + + if (!exprNode_isDefined (body)) + { + return; + } /*@i22*/ - DPRINTF((message("") )); + DPRINTF((message(""))); - if ( body->kind == XPR_BLOCK) + if (body->kind == XPR_BLOCK) body = exprData_getSingle(body->edata); /* @@ -783,7 +793,11 @@ static void exprNode_generateConstraintSwitch ( exprNode switchStmt) lastEnsures = constraintList_makeNew(); */ - exprNode_doGenerateConstraintSwitch (switchExpr, body, &lastRequires, &lastEnsures, &constraintsRequires, &constraintsEnsures); + /*@-mustfree@*/ + /*@i6534 - evans 2002-01-01: spurious warnings for these becuase of stack allocated storage */ + exprNode_doGenerateConstraintSwitch (switchExpr, body, &lastRequires, + &lastEnsures, &constraintsRequires, &constraintsEnsures); + /*@=mustfree@*/ /* merge current and saved constraint with Logical Or... @@ -793,7 +807,7 @@ static void exprNode_generateConstraintSwitch ( exprNode switchStmt) constraintList_free(switchStmt->requiresConstraints); constraintList_free(switchStmt->ensuresConstraints); - if (constraintList_isDefined(constraintsEnsures) && constraintList_isDefined(constraintsRequires) ) + if (constraintList_isDefined(constraintsEnsures) && constraintList_isDefined(constraintsRequires)) { switchStmt->ensuresConstraints = constraintList_logicalOr(constraintsEnsures, lastEnsures); switchStmt->requiresConstraints = constraintList_mergeRequires(constraintsRequires, lastRequires); @@ -809,22 +823,22 @@ static void exprNode_generateConstraintSwitch ( exprNode switchStmt) constraintList_free (lastRequires); constraintList_free (lastEnsures); - DPRINTF(( (message(" exprNode_generateConstraintSwitch returning requires: %s and ensures %s", - constraintList_print( switchStmt->requiresConstraints), - constraintList_print( switchStmt->ensuresConstraints) - ) - ) )); + DPRINTF(((message(" exprNode_generateConstraintSwitch returning requires: %s and ensures %s", + constraintList_print(switchStmt->requiresConstraints), + constraintList_print(switchStmt->ensuresConstraints) + ) + ))); } -static exprNode doSwitch (/*@returned@*/ exprNode e) +static exprNode doSwitch (/*@returned@*/ /*@notnull@*/ exprNode e) { exprNode body; exprData data; data = e->edata; - DPRINTF (( message ("doSwitch for: switch (%s) %s", + DPRINTF ((message ("doSwitch for: switch (%s) %s", exprNode_unparse (exprData_getPairA (data)), - exprNode_unparse (exprData_getPairB (data))) )); + exprNode_unparse (exprData_getPairB (data))))); body = exprData_getPairB (data); exprNode_generateConstraintSwitch (e); @@ -843,8 +857,8 @@ void exprNode_multiStatement (/*@dependent@*/ exprNode e) constraintList temp; - DPRINTF((message ("exprNode_multistatement Analysising %s %s at", exprNode_unparse( e), - fileloc_unparse(exprNode_getfileloc(e) ) ) ) ); + DPRINTF((message ("exprNode_multistatement Analysising %s %s at", exprNode_unparse(e), + fileloc_unparse(exprNode_getfileloc(e))))); if (exprNode_handleError (e)) { @@ -872,12 +886,12 @@ void exprNode_multiStatement (/*@dependent@*/ exprNode e) break; case XPR_FORPRED: - exprNode_generateConstraints (exprData_getTripleInit (data) ); + exprNode_generateConstraints (exprData_getTripleInit (data)); test = exprData_getTripleTest (data); exprNode_exprTraverse (test,FALSE, FALSE, exprNode_loc(e)); - exprNode_generateConstraints (exprData_getTripleInc (data) ); + exprNode_generateConstraints (exprData_getTripleInc (data)); - if (!exprNode_isError(test) ) + if (!exprNode_isError(test)) { constraintList temp2; temp2 = test->trueEnsuresConstraints; @@ -902,8 +916,8 @@ void exprNode_multiStatement (/*@dependent@*/ exprNode e) break; case XPR_IF: - DPRINTF(( "IF:") ); - DPRINTF ((exprNode_unparse(e) ) ); + DPRINTF(("IF:")); + DPRINTF ((exprNode_unparse(e))); e1 = exprData_getPairA (data); e2 = exprData_getPairB (data); @@ -916,6 +930,7 @@ void exprNode_multiStatement (/*@dependent@*/ exprNode e) case XPR_IFELSE: DPRINTF(("Starting IFELSE")); p = exprData_getTriplePred (data); + trueBranch = exprData_getTripleTrue (data); falseBranch = exprData_getTripleFalse (data); @@ -924,6 +939,7 @@ void exprNode_multiStatement (/*@dependent@*/ exprNode e) exprNode_generateConstraints (trueBranch); exprNode_generateConstraints (falseBranch); + llassert (exprNode_isDefined (p)); temp = p->ensuresConstraints; p->ensuresConstraints = exprNode_traversEnsuresConstraints (p); constraintList_free(temp); @@ -936,24 +952,41 @@ void exprNode_multiStatement (/*@dependent@*/ exprNode e) p->trueEnsuresConstraints = exprNode_traversTrueEnsuresConstraints(p); constraintList_free(temp); + + + DPRINTF((message("p->trueEnsuresConstraints before substitue %s", constraintList_print(p->trueEnsuresConstraints) ) + )); + + /*drl 10/10/2002 this is a bit of a hack but the reason why we do this is so that any function post conditions or similar things get applied correctly to each branch. e.g. in strlen(s) < 5 we want the trueEnsures to be maxRead(s) < 5*/ + + p->trueEnsuresConstraints = constraintList_substituteFreeTarget (p->trueEnsuresConstraints, + p->ensuresConstraints); + + DPRINTF(( message ("p->trueEnsuresConstraints after substitue %s", constraintList_print(p->trueEnsuresConstraints) ) + )); + temp = p->falseEnsuresConstraints; p->falseEnsuresConstraints = exprNode_traversFalseEnsuresConstraints(p); constraintList_free(temp); - e = doIfElse (e, p, trueBranch, falseBranch); - DPRINTF( ("Done IFELSE") ); + /*See comment on trueEnsures*/ + p->falseEnsuresConstraints = constraintList_substituteFreeTarget (p->falseEnsuresConstraints, + p->ensuresConstraints); + + e = doIfElse (e, p, trueBranch, falseBranch); + DPRINTF(("Done IFELSE")); break; - + case XPR_DOWHILE: e2 = (exprData_getPairB (data)); e1 = (exprData_getPairA (data)); - DPRINTF((message ("do { %s } while (%s)", exprNode_unparse(e2), exprNode_unparse(e1) ) )); + DPRINTF((message ("do { %s } while (%s)", exprNode_unparse(e2), exprNode_unparse(e1)))); exprNode_generateConstraints (e2); exprNode_generateConstraints (e1); e = exprNode_copyConstraints (e, e2); - DPRINTF ((message ("e = %s ", constraintList_print(e->requiresConstraints) ) )); + DPRINTF ((message ("e = %s ", constraintList_print(e->requiresConstraints)))); break; @@ -961,10 +994,10 @@ void exprNode_multiStatement (/*@dependent@*/ exprNode e) exprNode_generateConstraints (exprData_getSingle (data)); constraintList_free(e->requiresConstraints); - e->requiresConstraints = constraintList_copy ( (exprData_getSingle (data))->requiresConstraints ); + e->requiresConstraints = constraintList_copy ((exprData_getSingle (data))->requiresConstraints); constraintList_free(e->ensuresConstraints); - e->ensuresConstraints = constraintList_copy ( (exprData_getSingle (data))->ensuresConstraints ); + e->ensuresConstraints = constraintList_copy ((exprData_getSingle (data))->ensuresConstraints); break; case XPR_SWITCH: @@ -988,36 +1021,36 @@ static bool lltok_isBoolean_Op (lltok tok) I don't want to violate the abstraction maybe this should go in lltok.c */ - if (lltok_isEq_Op (tok) ) + if (lltok_isEq_Op (tok)) { return TRUE; } - if (lltok_isAnd_Op (tok) ) + if (lltok_isAnd_Op (tok)) { return TRUE; } - if (lltok_isOr_Op (tok) ) + if (lltok_isOr_Op (tok)) { return TRUE; } - if (lltok_isGt_Op (tok) ) + if (lltok_isGt_Op (tok)) { return TRUE; } - if (lltok_isLt_Op (tok) ) + if (lltok_isLt_Op (tok)) { return TRUE; } - if (lltok_isLe_Op (tok) ) + if (lltok_isLe_Op (tok)) { return TRUE; } - if (lltok_isGe_Op (tok) ) + if (lltok_isGe_Op (tok)) { return TRUE; } @@ -1044,14 +1077,14 @@ static void exprNode_booleanTraverse (/*@dependent@*/ exprNode e, /*@unused@*/ b /* arithmetic tests */ - if (lltok_isEq_Op (tok) ) + if (lltok_isEq_Op (tok)) { cons = constraint_makeEnsureEqual (t1, t2, sequencePoint); e->trueEnsuresConstraints = constraintList_add(e->trueEnsuresConstraints, cons); } - if (lltok_isLt_Op (tok) ) + if (lltok_isLt_Op (tok)) { cons = constraint_makeEnsureLessThan (t1, t2, sequencePoint); e->trueEnsuresConstraints = constraintList_add(e->trueEnsuresConstraints, cons); @@ -1059,7 +1092,7 @@ static void exprNode_booleanTraverse (/*@dependent@*/ exprNode e, /*@unused@*/ b e->falseEnsuresConstraints = constraintList_add(e->falseEnsuresConstraints, cons); } - if (lltok_isGe_Op (tok) ) + if (lltok_isGe_Op (tok)) { cons = constraint_makeEnsureGreaterThanEqual (t1, t2, sequencePoint); e->trueEnsuresConstraints = constraintList_add(e->trueEnsuresConstraints, cons); @@ -1068,7 +1101,7 @@ static void exprNode_booleanTraverse (/*@dependent@*/ exprNode e, /*@unused@*/ b e->falseEnsuresConstraints = constraintList_add(e->falseEnsuresConstraints, cons); } - if (lltok_isGt_Op (tok) ) + if (lltok_isGt_Op (tok)) { cons = constraint_makeEnsureGreaterThan (t1, t2, sequencePoint); e->trueEnsuresConstraints = constraintList_add(e->trueEnsuresConstraints, cons); @@ -1076,7 +1109,7 @@ static void exprNode_booleanTraverse (/*@dependent@*/ exprNode e, /*@unused@*/ b e->falseEnsuresConstraints = constraintList_add(e->falseEnsuresConstraints, cons); } - if (lltok_isLe_Op (tok) ) + if (lltok_isLe_Op (tok)) { cons = constraint_makeEnsureLessThanEqual (t1, t2, sequencePoint); e->trueEnsuresConstraints = constraintList_add(e->trueEnsuresConstraints, cons); @@ -1087,7 +1120,7 @@ static void exprNode_booleanTraverse (/*@dependent@*/ exprNode e, /*@unused@*/ b /* Logical operations */ - if (lltok_isAnd_Op (tok) ) + if (lltok_isAnd_Op (tok)) { /* true ensures */ tempList = constraintList_copy (t1->trueEnsuresConstraints); @@ -1101,10 +1134,10 @@ static void exprNode_booleanTraverse (/*@dependent@*/ exprNode e, /*@unused@*/ b tempList = constraintList_logicalOr (tempList, t1->falseEnsuresConstraints); constraintList_free (temp); - /* evans - was constraintList_addList - memory leak detected by lclint */ + /* evans - was constraintList_addList - memory leak detected by splint */ e->falseEnsuresConstraints = constraintList_addListFree (e->falseEnsuresConstraints, tempList); } - else if (lltok_isOr_Op (tok) ) + else if (lltok_isOr_Op (tok)) { /* false ensures */ tempList = constraintList_copy (t1->falseEnsuresConstraints); @@ -1124,7 +1157,7 @@ static void exprNode_booleanTraverse (/*@dependent@*/ exprNode e, /*@unused@*/ b } else { - DPRINTF((message("%s is not a boolean operation", lltok_unparse(tok) ) )); + DPRINTF((message("%s is not a boolean operation", lltok_unparse(tok)))); } } @@ -1138,13 +1171,13 @@ void exprNode_exprTraverse (exprNode e, bool definatelv, bool definaterv, /*@ob constraintList temp; - if (exprNode_isError(e) ) + if (exprNode_isError(e)) { return; } - DPRINTF((message ("exprNode_exprTraverset Analysising %s %s at", exprNode_unparse( e), - fileloc_unparse(exprNode_getfileloc(e) ) ) ) ); + DPRINTF((message ("exprNode_exprTraverset Analysising %s %s at", exprNode_unparse(e), + fileloc_unparse(exprNode_getfileloc(e))))); /*e->requiresConstraints = constraintList_makeNew(); e->ensuresConstraints = constraintList_makeNew(); @@ -1152,7 +1185,7 @@ void exprNode_exprTraverse (exprNode e, bool definatelv, bool definaterv, /*@ob e->falseEnsuresConstraints = constraintList_makeNew();; */ - if (exprNode_isUnhandled (e) ) + if (exprNode_isUnhandled (e)) { return; } @@ -1171,17 +1204,17 @@ void exprNode_exprTraverse (exprNode e, bool definatelv, bool definaterv, /*@ob case XPR_FETCH: - if (definatelv ) + if (definatelv) { - t1 = (exprData_getPairA (data) ); - t2 = (exprData_getPairB (data) ); + t1 = (exprData_getPairA (data)); + t2 = (exprData_getPairB (data)); cons = constraint_makeWriteSafeExprNode (t1, t2); } else { - t1 = (exprData_getPairA (data) ); - t2 = (exprData_getPairB (data) ); - cons = constraint_makeReadSafeExprNode (t1, t2 ); + t1 = (exprData_getPairA (data)); + t2 = (exprData_getPairB (data)); + cons = constraint_makeReadSafeExprNode (t1, t2); } e->requiresConstraints = constraintList_add(e->requiresConstraints, cons); @@ -1214,16 +1247,16 @@ void exprNode_exprTraverse (exprNode e, bool definatelv, bool definaterv, /*@ob */ t2 = exprData_getInitNode (data); - /* DPRINTF(( (message("initialization: %s = %s", + /* DPRINTF(((message("initialization: %s = %s", exprNode_unparse(lhs), exprNode_unparse(t2) - ) - ) )); */ + ) + ))); */ - exprNode_exprTraverse (t2, definatelv, TRUE, sequencePoint ); + exprNode_exprTraverse (t2, definatelv, TRUE, sequencePoint); /* this test is nessecary because some expressions generate a null expression node. function pointer do that -- drl */ - if ( (!exprNode_isError (e)) && (!exprNode_isError(t2)) ) + if ((!exprNode_isError (e)) && (!exprNode_isError(t2))) { cons = constraint_makeEnsureEqual (e, t2, sequencePoint); e->ensuresConstraints = constraintList_add(e->ensuresConstraints, cons); @@ -1234,11 +1267,11 @@ void exprNode_exprTraverse (exprNode e, bool definatelv, bool definaterv, /*@ob case XPR_ASSIGN: t1 = exprData_getOpA (data); t2 = exprData_getOpB (data); - exprNode_exprTraverse (t1, TRUE, definaterv, sequencePoint ); - exprNode_exprTraverse (t2, definatelv, TRUE, sequencePoint ); + exprNode_exprTraverse (t1, TRUE, definaterv, sequencePoint); + exprNode_exprTraverse (t2, definatelv, TRUE, sequencePoint); /* this test is nessecary because some expressions generate a null expression node. function pointer do that -- drl */ - if ( (!exprNode_isError (t1)) && (!exprNode_isError(t2)) ) + if ((!exprNode_isError (t1)) && (!exprNode_isError(t2))) { cons = constraint_makeEnsureEqual (t1, t2, sequencePoint); e->ensuresConstraints = constraintList_add(e->ensuresConstraints, cons); @@ -1247,32 +1280,31 @@ void exprNode_exprTraverse (exprNode e, bool definatelv, bool definaterv, /*@ob case XPR_OP: t1 = exprData_getOpA (data); t2 = exprData_getOpB (data); - tok = exprData_getOpTok (data); - + tok = exprData_getOpTok (data); - if (tok.tok == ADD_ASSIGN) + if (lltok_getTok (tok) == ADD_ASSIGN) { - exprNode_exprTraverse (t1, TRUE, definaterv, sequencePoint ); - exprNode_exprTraverse (t2, definatelv, TRUE, sequencePoint ); + exprNode_exprTraverse (t1, TRUE, definaterv, sequencePoint); + exprNode_exprTraverse (t2, definatelv, TRUE, sequencePoint); - cons = constraint_makeAddAssign (t1, t2, sequencePoint ); + cons = constraint_makeAddAssign (t1, t2, sequencePoint); e->ensuresConstraints = constraintList_add(e->ensuresConstraints, cons); } - else if (tok.tok == SUB_ASSIGN) + else if (lltok_getTok (tok) == SUB_ASSIGN) { - exprNode_exprTraverse (t1, TRUE, definaterv, sequencePoint ); - exprNode_exprTraverse (t2, definatelv, TRUE, sequencePoint ); + exprNode_exprTraverse (t1, TRUE, definaterv, sequencePoint); + exprNode_exprTraverse (t2, definatelv, TRUE, sequencePoint); - cons = constraint_makeSubtractAssign (t1, t2, sequencePoint ); + cons = constraint_makeSubtractAssign (t1, t2, sequencePoint); e->ensuresConstraints = constraintList_add(e->ensuresConstraints, cons); } else { - exprNode_exprTraverse (t1, definatelv, definaterv, sequencePoint ); - exprNode_exprTraverse (t2, definatelv, definaterv, sequencePoint ); + exprNode_exprTraverse (t1, definatelv, definaterv, sequencePoint); + exprNode_exprTraverse (t2, definatelv, definaterv, sequencePoint); } - if (lltok_isBoolean_Op (tok) ) + if (lltok_isBoolean_Op (tok)) exprNode_booleanTraverse (e, definatelv, definaterv, sequencePoint); break; @@ -1292,23 +1324,23 @@ void exprNode_exprTraverse (exprNode e, bool definatelv, bool definaterv, /*@ob case XPR_CALL: fcn = exprData_getFcn(data); - exprNode_exprTraverse (fcn, definatelv, definaterv, sequencePoint ); - DPRINTF ( (message ("Got call that %s ( %s) ", exprNode_unparse(fcn), exprNodeList_unparse (exprData_getArgs (data) ) ) ) ); + exprNode_exprTraverse (fcn, definatelv, definaterv, sequencePoint); + DPRINTF ((message ("Got call that %s (%s) ", exprNode_unparse(fcn), exprNodeList_unparse (exprData_getArgs (data))))); fcn->requiresConstraints = constraintList_addListFree (fcn->requiresConstraints, - checkCall (fcn, exprData_getArgs (data) ) ); + checkCall (fcn, exprData_getArgs (data) )); fcn->ensuresConstraints = constraintList_addListFree (fcn->ensuresConstraints, - exprNode_getPostConditions(fcn, exprData_getArgs (data),e ) ); + exprNode_getPostConditions(fcn, exprData_getArgs (data),e )); - t1 = exprNode_createNew (exprNode_getType (e) ); + t1 = exprNode_createNew (exprNode_getType (e)); checkArgumentList (t1, exprData_getArgs(data), sequencePoint); exprNode_mergeResolve (e, t1, fcn); exprNode_free(t1); break; case XPR_RETURN: - exprNode_exprTraverse (exprData_getSingle (data), definatelv, definaterv, sequencePoint ); + exprNode_exprTraverse (exprData_getSingle (data), definatelv, definaterv, sequencePoint); break; case XPR_NULLRETURN: @@ -1317,11 +1349,11 @@ void exprNode_exprTraverse (exprNode e, bool definatelv, bool definaterv, /*@ob case XPR_FACCESS: - exprNode_exprTraverse (exprData_getFieldNode (data), definatelv, definaterv, sequencePoint ); + exprNode_exprTraverse (exprData_getFieldNode (data), definatelv, definaterv, sequencePoint); break; case XPR_ARROW: - exprNode_exprTraverse (exprData_getFieldNode (data), definatelv, definaterv, sequencePoint ); + exprNode_exprTraverse (exprData_getFieldNode (data), definatelv, definaterv, sequencePoint); break; case XPR_STRINGLITERAL: @@ -1335,23 +1367,23 @@ void exprNode_exprTraverse (exprNode e, bool definatelv, bool definaterv, /*@ob case XPR_PREOP: t1 = exprData_getUopNode(data); tok = (exprData_getUopTok (data)); - exprNode_exprTraverse (t1, definatelv, definaterv, sequencePoint ); + exprNode_exprTraverse (t1, definatelv, definaterv, sequencePoint); /*handle * pointer access */ - if (lltok_isInc_Op (tok) ) + if (lltok_isInc_Op (tok)) { DPRINTF(("doing ++(var)")); t1 = exprData_getUopNode (data); - cons = constraint_makeMaxSetSideEffectPostIncrement (t1, sequencePoint ); + cons = constraint_makeMaxSetSideEffectPostIncrement (t1, sequencePoint); e->ensuresConstraints = constraintList_add (e->ensuresConstraints, cons); } - else if (lltok_isDec_Op (tok) ) + else if (lltok_isDec_Op (tok)) { DPRINTF(("doing --(var)")); t1 = exprData_getUopNode (data); - cons = constraint_makeMaxSetSideEffectPostDecrement (t1, sequencePoint ); + cons = constraint_makeMaxSetSideEffectPostDecrement (t1, sequencePoint); e->ensuresConstraints = constraintList_add (e->ensuresConstraints, cons); } - else if (lltok_isMult( tok ) ) + else if (lltok_isMult(tok )) { if (definatelv) { @@ -1363,7 +1395,7 @@ void exprNode_exprTraverse (exprNode e, bool definatelv, bool definaterv, /*@ob } e->requiresConstraints = constraintList_add(e->requiresConstraints, cons); } - else if (lltok_isNot_Op (tok) ) + else if (lltok_isNot_Op (tok)) /* ! expr */ { constraintList_free(e->trueEnsuresConstraints); @@ -1373,136 +1405,136 @@ void exprNode_exprTraverse (exprNode e, bool definatelv, bool definaterv, /*@ob e->falseEnsuresConstraints = constraintList_copy (t1->trueEnsuresConstraints); } - else if (lltok_isAmpersand_Op (tok) ) + else if (lltok_isAmpersand_Op (tok)) { break; } - else if (lltok_isMinus_Op (tok) ) + else if (lltok_isMinus_Op (tok)) { break; } - else if ( lltok_isExcl_Op (tok) ) + else if (lltok_isExcl_Op (tok)) { break; } - else if (lltok_isTilde_Op (tok) ) + else if (lltok_isTilde_Op (tok)) { break; } else { - llcontbug((message("Unsupported preop in %s", exprNode_unparse(e) ) )); + llcontbug (message("Unsupported preop in %s", exprNode_unparse(e))); BADEXIT; } break; case XPR_POSTOP: + exprNode_exprTraverse (exprData_getUopNode (data), TRUE, + definaterv, sequencePoint); - exprNode_exprTraverse (exprData_getUopNode (data), TRUE, definaterv, sequencePoint ); - - if (lltok_isInc_Op (exprData_getUopTok (data) ) ) + if (lltok_isInc_Op (exprData_getUopTok (data))) { DPRINTF(("doing ++")); t1 = exprData_getUopNode (data); - cons = constraint_makeMaxSetSideEffectPostIncrement (t1, sequencePoint ); + cons = constraint_makeMaxSetSideEffectPostIncrement (t1, sequencePoint); e->ensuresConstraints = constraintList_add (e->ensuresConstraints, cons); } - if (lltok_isDec_Op (exprData_getUopTok (data) ) ) + if (lltok_isDec_Op (exprData_getUopTok (data))) { DPRINTF(("doing --")); t1 = exprData_getUopNode (data); - cons = constraint_makeMaxSetSideEffectPostDecrement (t1, sequencePoint ); + cons = constraint_makeMaxSetSideEffectPostDecrement (t1, sequencePoint); e->ensuresConstraints = constraintList_add (e->ensuresConstraints, cons); } break; case XPR_CAST: { t2 = exprData_getCastNode (data); - DPRINTF (( message ("Examining cast (%q)%s", + DPRINTF ((message ("Examining cast (%q)%s", qtype_unparse (exprData_getCastType (data)), - exprNode_unparse (t2) ) - )); - exprNode_exprTraverse (t2, definatelv, definaterv, sequencePoint ); + exprNode_unparse (t2)) + )); + exprNode_exprTraverse (t2, definatelv, definaterv, sequencePoint); } break; case XPR_COND: { exprNode pred, trueBranch, falseBranch; - llassert(FALSE); - pred = exprData_getTriplePred (data); - trueBranch = exprData_getTripleTrue (data); - falseBranch = exprData_getTripleFalse (data); - - exprNode_exprTraverse (pred, FALSE, TRUE, sequencePoint ); - - temp = pred->ensuresConstraints; - pred->ensuresConstraints = exprNode_traversEnsuresConstraints(pred); - constraintList_free(temp); - - temp = pred->requiresConstraints; - pred->requiresConstraints = exprNode_traversRequiresConstraints(pred); - constraintList_free(temp); - - temp = pred->trueEnsuresConstraints; - pred->trueEnsuresConstraints = exprNode_traversTrueEnsuresConstraints(pred); - constraintList_free(temp); - - temp = pred->falseEnsuresConstraints; - pred->falseEnsuresConstraints = exprNode_traversFalseEnsuresConstraints(pred); - constraintList_free(temp); - - - exprNode_exprTraverse (trueBranch, FALSE, TRUE, sequencePoint ); - - temp = trueBranch->ensuresConstraints; - trueBranch->ensuresConstraints = exprNode_traversEnsuresConstraints(trueBranch); - constraintList_free(temp); - - - temp = trueBranch->requiresConstraints; - trueBranch->requiresConstraints = exprNode_traversRequiresConstraints(trueBranch); - constraintList_free(temp); - - - temp = trueBranch->trueEnsuresConstraints; - trueBranch->trueEnsuresConstraints = exprNode_traversTrueEnsuresConstraints(trueBranch); - constraintList_free(temp); - - temp = trueBranch->falseEnsuresConstraints; - trueBranch->falseEnsuresConstraints = exprNode_traversFalseEnsuresConstraints(trueBranch); - constraintList_free(temp); - - exprNode_exprTraverse (falseBranch, FALSE, TRUE, sequencePoint ); - - temp = falseBranch->ensuresConstraints; - falseBranch->ensuresConstraints = exprNode_traversEnsuresConstraints(falseBranch); - constraintList_free(temp); - - - temp = falseBranch->requiresConstraints; - falseBranch->requiresConstraints = exprNode_traversRequiresConstraints(falseBranch); - constraintList_free(temp); - - - temp = falseBranch->trueEnsuresConstraints; - falseBranch->trueEnsuresConstraints = exprNode_traversTrueEnsuresConstraints(falseBranch); - constraintList_free(temp); - - temp = falseBranch->falseEnsuresConstraints; - falseBranch->falseEnsuresConstraints = exprNode_traversFalseEnsuresConstraints(falseBranch); - constraintList_free(temp); - - /* if pred is true e equals true otherwise pred equals false */ - - cons = constraint_makeEnsureEqual (e, trueBranch, sequencePoint); - trueBranch->ensuresConstraints = constraintList_add(trueBranch->ensuresConstraints, cons); - - cons = constraint_makeEnsureEqual (e, trueBranch, sequencePoint); - falseBranch->ensuresConstraints = constraintList_add(falseBranch->ensuresConstraints, cons); + llassert(FALSE); + pred = exprData_getTriplePred (data); + trueBranch = exprData_getTripleTrue (data); + falseBranch = exprData_getTripleFalse (data); + + llassert (exprNode_isDefined (pred)); + llassert (exprNode_isDefined (trueBranch)); + llassert (exprNode_isDefined (falseBranch)); - e = doIfElse (e, pred, trueBranch, falseBranch); - + exprNode_exprTraverse (pred, FALSE, TRUE, sequencePoint); + + temp = pred->ensuresConstraints; + pred->ensuresConstraints = exprNode_traversEnsuresConstraints(pred); + constraintList_free(temp); + + temp = pred->requiresConstraints; + pred->requiresConstraints = exprNode_traversRequiresConstraints(pred); + constraintList_free(temp); + + temp = pred->trueEnsuresConstraints; + pred->trueEnsuresConstraints = exprNode_traversTrueEnsuresConstraints(pred); + constraintList_free(temp); + + temp = pred->falseEnsuresConstraints; + pred->falseEnsuresConstraints = exprNode_traversFalseEnsuresConstraints(pred); + constraintList_free(temp); + + exprNode_exprTraverse (trueBranch, FALSE, TRUE, sequencePoint); + + temp = trueBranch->ensuresConstraints; + trueBranch->ensuresConstraints = exprNode_traversEnsuresConstraints(trueBranch); + constraintList_free(temp); + + temp = trueBranch->requiresConstraints; + trueBranch->requiresConstraints = exprNode_traversRequiresConstraints(trueBranch); + constraintList_free(temp); + + + temp = trueBranch->trueEnsuresConstraints; + trueBranch->trueEnsuresConstraints = exprNode_traversTrueEnsuresConstraints(trueBranch); + constraintList_free(temp); + + temp = trueBranch->falseEnsuresConstraints; + trueBranch->falseEnsuresConstraints = exprNode_traversFalseEnsuresConstraints(trueBranch); + constraintList_free(temp); + + exprNode_exprTraverse (falseBranch, FALSE, TRUE, sequencePoint); + + temp = falseBranch->ensuresConstraints; + falseBranch->ensuresConstraints = exprNode_traversEnsuresConstraints(falseBranch); + constraintList_free(temp); + + + temp = falseBranch->requiresConstraints; + falseBranch->requiresConstraints = exprNode_traversRequiresConstraints(falseBranch); + constraintList_free(temp); + + temp = falseBranch->trueEnsuresConstraints; + falseBranch->trueEnsuresConstraints = exprNode_traversTrueEnsuresConstraints(falseBranch); + constraintList_free(temp); + + temp = falseBranch->falseEnsuresConstraints; + falseBranch->falseEnsuresConstraints = exprNode_traversFalseEnsuresConstraints(falseBranch); + constraintList_free(temp); + + /* if pred is true e equals true otherwise pred equals false */ + + cons = constraint_makeEnsureEqual (e, trueBranch, sequencePoint); + trueBranch->ensuresConstraints = constraintList_add(trueBranch->ensuresConstraints, cons); + + cons = constraint_makeEnsureEqual (e, trueBranch, sequencePoint); + falseBranch->ensuresConstraints = constraintList_add(falseBranch->ensuresConstraints, cons); + + e = doIfElse (e, pred, trueBranch, falseBranch); } break; case XPR_COMMA: @@ -1512,8 +1544,8 @@ void exprNode_exprTraverse (exprNode e, bool definatelv, bool definaterv, /*@ob /* we essiantially treat this like expr1; expr2 of course sequencePoint isn't adjusted so this isn't completely accurate problems../ */ - exprNode_exprTraverse (t1, FALSE, FALSE, sequencePoint ); - exprNode_exprTraverse (t2, definatelv, definaterv, sequencePoint ); + exprNode_exprTraverse (t1, FALSE, FALSE, sequencePoint); + exprNode_exprTraverse (t2, definatelv, definaterv, sequencePoint); exprNode_mergeResolve (e, t1, t2); break; @@ -1521,22 +1553,22 @@ void exprNode_exprTraverse (exprNode e, bool definatelv, bool definaterv, /*@ob handledExprNode = FALSE; } - e->requiresConstraints = constraintList_preserveOrig ( e->requiresConstraints); - e->ensuresConstraints = constraintList_preserveOrig ( e->ensuresConstraints); - e->requiresConstraints = constraintList_addGeneratingExpr ( e->requiresConstraints, e); + e->requiresConstraints = constraintList_preserveOrig (e->requiresConstraints); + e->ensuresConstraints = constraintList_preserveOrig (e->ensuresConstraints); + e->requiresConstraints = constraintList_addGeneratingExpr (e->requiresConstraints, e); - e->ensuresConstraints = constraintList_addGeneratingExpr ( e->ensuresConstraints, e); + e->ensuresConstraints = constraintList_addGeneratingExpr (e->ensuresConstraints, e); - e->requiresConstraints = constraintList_removeSurpressed( e->requiresConstraints); + e->requiresConstraints = constraintList_removeSurpressed(e->requiresConstraints); - DPRINTF((message ("ensures constraints for %s are %s", exprNode_unparse(e), constraintList_printDetailed(e->ensuresConstraints) ) )); + DPRINTF((message ("ensures constraints for %s are %s", exprNode_unparse(e), constraintList_printDetailed(e->ensuresConstraints)))); - DPRINTF((message ("Requires constraints for %s are %s", exprNode_unparse(e), constraintList_printDetailed(e->ensuresConstraints) ) )); + DPRINTF((message ("Requires constraints for %s are %s", exprNode_unparse(e), constraintList_printDetailed(e->ensuresConstraints)))); - DPRINTF((message ("trueEnsures constraints for %s are %s", exprNode_unparse(e), constraintList_printDetailed(e->trueEnsuresConstraints) ) )); + DPRINTF((message ("trueEnsures constraints for %s are %s", exprNode_unparse(e), constraintList_printDetailed(e->trueEnsuresConstraints)))); - DPRINTF((message ("falseEnsures constraints for %s are %s", exprNode_unparse(e), constraintList_printDetailed(e->falseEnsuresConstraints) ) )); + DPRINTF((message ("falseEnsures constraints for %s are %s", exprNode_unparse(e), constraintList_printDetailed(e->falseEnsuresConstraints)))); return; } @@ -1555,7 +1587,8 @@ constraintList exprNode_traversTrueEnsuresConstraints (exprNode e) ret = constraintList_makeNew(); return ret; } - ret = constraintList_copy (e->trueEnsuresConstraints ); + + ret = constraintList_copy (e->trueEnsuresConstraints); handledExprNode = TRUE; @@ -1565,55 +1598,55 @@ constraintList exprNode_traversTrueEnsuresConstraints (exprNode e) { case XPR_WHILEPRED: t1 = exprData_getSingle (data); - ret = constraintList_addListFree ( ret, exprNode_traversTrueEnsuresConstraints (t1) ); + ret = constraintList_addListFree (ret, exprNode_traversTrueEnsuresConstraints (t1)); break; case XPR_FETCH: ret = constraintList_addListFree (ret, exprNode_traversTrueEnsuresConstraints - (exprData_getPairA (data) ) ); + (exprData_getPairA (data))); ret = constraintList_addListFree (ret, exprNode_traversTrueEnsuresConstraints - (exprData_getPairB (data) ) ); + (exprData_getPairB (data))); break; case XPR_PREOP: ret = constraintList_addListFree (ret, exprNode_traversTrueEnsuresConstraints - (exprData_getUopNode (data) ) ); + (exprData_getUopNode (data))); break; case XPR_PARENS: ret = constraintList_addListFree (ret, exprNode_traversTrueEnsuresConstraints - (exprData_getUopNode (data) ) ); + (exprData_getUopNode (data))); break; case XPR_INIT: ret = constraintList_addListFree (ret, exprNode_traversTrueEnsuresConstraints - (exprData_getInitNode (data) ) ); + (exprData_getInitNode (data))); break; case XPR_ASSIGN: ret = constraintList_addListFree (ret, exprNode_traversTrueEnsuresConstraints - (exprData_getOpA (data) ) ); + (exprData_getOpA (data))); ret = constraintList_addListFree (ret, exprNode_traversTrueEnsuresConstraints - (exprData_getOpB (data) ) ); + (exprData_getOpB (data))); break; case XPR_OP: ret = constraintList_addListFree (ret, exprNode_traversTrueEnsuresConstraints - (exprData_getOpA (data) ) ); + (exprData_getOpA (data))); ret = constraintList_addListFree (ret, exprNode_traversTrueEnsuresConstraints - (exprData_getOpB (data) ) ); + (exprData_getOpB (data))); break; case XPR_SIZEOFT: break; @@ -1622,20 +1655,20 @@ constraintList exprNode_traversTrueEnsuresConstraints (exprNode e) ret = constraintList_addListFree (ret, exprNode_traversTrueEnsuresConstraints - (exprData_getSingle (data) ) ); + (exprData_getSingle (data))); break; case XPR_CALL: ret = constraintList_addListFree (ret, exprNode_traversTrueEnsuresConstraints - (exprData_getFcn (data) ) ); - /*@i11*/ /* exprNodeList_unparse (exprData_getArgs (data) ); */ + (exprData_getFcn (data))); + /*@i11*/ /* exprNodeList_unparse (exprData_getArgs (data)); */ break; case XPR_RETURN: ret = constraintList_addListFree (ret, exprNode_traversTrueEnsuresConstraints - (exprData_getSingle (data) ) ); + (exprData_getSingle (data))); break; case XPR_NULLRETURN: @@ -1644,13 +1677,13 @@ constraintList exprNode_traversTrueEnsuresConstraints (exprNode e) case XPR_FACCESS: ret = constraintList_addListFree (ret, exprNode_traversTrueEnsuresConstraints - (exprData_getFieldNode (data) ) ); + (exprData_getFieldNode (data))); break; case XPR_ARROW: ret = constraintList_addListFree (ret, exprNode_traversTrueEnsuresConstraints - (exprData_getFieldNode (data) ) ); + (exprData_getFieldNode (data))); break; case XPR_STRINGLITERAL: @@ -1662,14 +1695,14 @@ constraintList exprNode_traversTrueEnsuresConstraints (exprNode e) ret = constraintList_addListFree (ret, exprNode_traversTrueEnsuresConstraints - (exprData_getUopNode (data) ) ); + (exprData_getUopNode (data))); break; case XPR_CAST: ret = constraintList_addListFree (ret, exprNode_traversTrueEnsuresConstraints - (exprData_getCastNode (data) ) ); + (exprData_getCastNode (data))); break; default: @@ -1685,70 +1718,68 @@ constraintList exprNode_traversFalseEnsuresConstraints (exprNode e) bool handledExprNode; exprData data; constraintList ret; - - if (exprNode_handleError (e)) - { - ret = constraintList_makeNew(); - return ret; - } - - ret = constraintList_copy (e->falseEnsuresConstraints ); - - handledExprNode = TRUE; - + + if (exprNode_handleError (e)) + { + ret = constraintList_makeNew(); + return ret; + } + + ret = constraintList_copy (e->falseEnsuresConstraints); + handledExprNode = TRUE; data = e->edata; switch (e->kind) { case XPR_WHILEPRED: t1 = exprData_getSingle (data); - ret = constraintList_addListFree ( ret,exprNode_traversFalseEnsuresConstraints (t1) ); + ret = constraintList_addListFree (ret,exprNode_traversFalseEnsuresConstraints (t1)); break; case XPR_FETCH: ret = constraintList_addListFree (ret, exprNode_traversFalseEnsuresConstraints - (exprData_getPairA (data) ) ); + (exprData_getPairA (data))); ret = constraintList_addListFree (ret, exprNode_traversFalseEnsuresConstraints - (exprData_getPairB (data) ) ); + (exprData_getPairB (data))); break; case XPR_PREOP: ret = constraintList_addListFree (ret, exprNode_traversFalseEnsuresConstraints - (exprData_getUopNode (data) ) ); + (exprData_getUopNode (data))); break; case XPR_PARENS: ret = constraintList_addListFree (ret, exprNode_traversFalseEnsuresConstraints - (exprData_getUopNode (data) ) ); + (exprData_getUopNode (data))); break; case XPR_INIT: ret = constraintList_addListFree (ret, exprNode_traversFalseEnsuresConstraints - ( exprData_getInitNode (data) ) ); + ( exprData_getInitNode (data))); break; case XPR_ASSIGN: ret = constraintList_addListFree (ret, exprNode_traversFalseEnsuresConstraints - (exprData_getOpA (data) ) ); + (exprData_getOpA (data))); ret = constraintList_addListFree (ret, exprNode_traversFalseEnsuresConstraints - (exprData_getOpB (data) ) ); + (exprData_getOpB (data))); break; case XPR_OP: ret = constraintList_addListFree (ret, exprNode_traversFalseEnsuresConstraints - (exprData_getOpA (data) ) ); + (exprData_getOpA (data))); ret = constraintList_addListFree (ret, exprNode_traversFalseEnsuresConstraints - (exprData_getOpB (data) ) ); + (exprData_getOpB (data))); break; case XPR_SIZEOFT: break; @@ -1757,20 +1788,20 @@ constraintList exprNode_traversFalseEnsuresConstraints (exprNode e) ret = constraintList_addListFree (ret, exprNode_traversFalseEnsuresConstraints - (exprData_getSingle (data) ) ); + (exprData_getSingle (data))); break; case XPR_CALL: ret = constraintList_addListFree (ret, exprNode_traversFalseEnsuresConstraints - (exprData_getFcn (data) ) ); - /*@i11*/ /* exprNodeList_unparse (exprData_getArgs (data) ); */ + (exprData_getFcn (data))); + /*@i11*/ /* exprNodeList_unparse (exprData_getArgs (data)); */ break; case XPR_RETURN: ret = constraintList_addListFree (ret, exprNode_traversFalseEnsuresConstraints - (exprData_getSingle (data) ) ); + (exprData_getSingle (data))); break; case XPR_NULLRETURN: @@ -1779,13 +1810,13 @@ constraintList exprNode_traversFalseEnsuresConstraints (exprNode e) case XPR_FACCESS: ret = constraintList_addListFree (ret, exprNode_traversFalseEnsuresConstraints - (exprData_getFieldNode (data) ) ); + (exprData_getFieldNode (data))); break; case XPR_ARROW: ret = constraintList_addListFree (ret, exprNode_traversFalseEnsuresConstraints - (exprData_getFieldNode (data) ) ); + (exprData_getFieldNode (data))); break; case XPR_STRINGLITERAL: @@ -1797,14 +1828,14 @@ constraintList exprNode_traversFalseEnsuresConstraints (exprNode e) ret = constraintList_addListFree (ret, exprNode_traversFalseEnsuresConstraints - (exprData_getUopNode (data) ) ); + (exprData_getUopNode (data))); break; case XPR_CAST: ret = constraintList_addListFree (ret, exprNode_traversFalseEnsuresConstraints - (exprData_getCastNode (data) ) ); + (exprData_getCastNode (data))); break; default: @@ -1829,63 +1860,62 @@ constraintList exprNode_traversFalseEnsuresConstraints (exprNode e) ret = constraintList_makeNew(); return ret; } - ret = constraintList_copy (e->requiresConstraints ); - - handledExprNode = TRUE; - + + ret = constraintList_copy (e->requiresConstraints); + handledExprNode = TRUE; data = e->edata; switch (e->kind) { case XPR_WHILEPRED: t1 = exprData_getSingle (data); - ret = constraintList_addListFree ( ret, exprNode_traversRequiresConstraints (t1) ); + ret = constraintList_addListFree (ret, exprNode_traversRequiresConstraints (t1)); break; case XPR_FETCH: ret = constraintList_addListFree (ret, exprNode_traversRequiresConstraints - (exprData_getPairA (data) ) ); + (exprData_getPairA (data))); ret = constraintList_addListFree (ret, exprNode_traversRequiresConstraints - (exprData_getPairB (data) ) ); + (exprData_getPairB (data))); break; case XPR_PREOP: ret = constraintList_addListFree (ret, exprNode_traversRequiresConstraints - (exprData_getUopNode (data) ) ); + (exprData_getUopNode (data))); break; case XPR_PARENS: ret = constraintList_addListFree (ret, exprNode_traversRequiresConstraints - (exprData_getUopNode (data) ) ); + (exprData_getUopNode (data))); break; case XPR_INIT: ret = constraintList_addListFree (ret, exprNode_traversRequiresConstraints - (exprData_getInitNode (data) ) ); + (exprData_getInitNode (data))); break; case XPR_ASSIGN: ret = constraintList_addListFree (ret, exprNode_traversRequiresConstraints - (exprData_getOpA (data) ) ); + (exprData_getOpA (data))); ret = constraintList_addListFree (ret, exprNode_traversRequiresConstraints - (exprData_getOpB (data) ) ); + (exprData_getOpB (data))); break; case XPR_OP: ret = constraintList_addListFree (ret, exprNode_traversRequiresConstraints - (exprData_getOpA (data) ) ); + (exprData_getOpA (data))); ret = constraintList_addListFree (ret, exprNode_traversRequiresConstraints - (exprData_getOpB (data) ) ); + (exprData_getOpB (data))); break; case XPR_SIZEOFT: break; @@ -1894,20 +1924,20 @@ constraintList exprNode_traversFalseEnsuresConstraints (exprNode e) ret = constraintList_addListFree (ret, exprNode_traversRequiresConstraints - (exprData_getSingle (data) ) ); + (exprData_getSingle (data))); break; case XPR_CALL: ret = constraintList_addListFree (ret, exprNode_traversRequiresConstraints - (exprData_getFcn (data) ) ); - /*@i11*/ /* exprNodeList_unparse (exprData_getArgs (data) ); */ + (exprData_getFcn (data))); + /*@i11*/ /* exprNodeList_unparse (exprData_getArgs (data)); */ break; case XPR_RETURN: ret = constraintList_addListFree (ret, exprNode_traversRequiresConstraints - (exprData_getSingle (data) ) ); + (exprData_getSingle (data))); break; case XPR_NULLRETURN: @@ -1916,13 +1946,13 @@ constraintList exprNode_traversFalseEnsuresConstraints (exprNode e) case XPR_FACCESS: ret = constraintList_addListFree (ret, exprNode_traversRequiresConstraints - (exprData_getFieldNode (data) ) ); + (exprData_getFieldNode (data))); break; case XPR_ARROW: ret = constraintList_addListFree (ret, exprNode_traversRequiresConstraints - (exprData_getFieldNode (data) ) ); + (exprData_getFieldNode (data))); break; case XPR_STRINGLITERAL: @@ -1934,14 +1964,14 @@ constraintList exprNode_traversFalseEnsuresConstraints (exprNode e) ret = constraintList_addListFree (ret, exprNode_traversRequiresConstraints - (exprData_getUopNode (data) ) ); + (exprData_getUopNode (data))); break; case XPR_CAST: ret = constraintList_addListFree (ret, exprNode_traversRequiresConstraints - (exprData_getCastNode (data) ) ); + (exprData_getCastNode (data))); break; default: @@ -1961,20 +1991,19 @@ constraintList exprNode_traversFalseEnsuresConstraints (exprNode e) exprData data; constraintList ret; - - if (exprNode_handleError (e)) - { - ret = constraintList_makeNew(); - return ret; - } - - ret = constraintList_copy (e->ensuresConstraints ); - handledExprNode = TRUE; - + if (exprNode_handleError (e)) + { + ret = constraintList_makeNew(); + return ret; + } + + ret = constraintList_copy (e->ensuresConstraints); + handledExprNode = TRUE; + data = e->edata; - - DPRINTF( (message ( - "exprnode_traversEnsuresConstraints call for %s with constraintList of %s", + + DPRINTF ((message ("exprnode_traversEnsuresConstraints call for %s with " + "constraintList of %s", exprNode_unparse (e), constraintList_print(e->ensuresConstraints) ) @@ -1983,128 +2012,116 @@ constraintList exprNode_traversFalseEnsuresConstraints (exprNode e) switch (e->kind) { - case XPR_WHILEPRED: + case XPR_WHILEPRED: t1 = exprData_getSingle (data); - ret = constraintList_addListFree ( ret,exprNode_traversEnsuresConstraints (t1) ); + ret = constraintList_addListFree (ret,exprNode_traversEnsuresConstraints (t1)); break; case XPR_FETCH: - ret = constraintList_addListFree (ret, - exprNode_traversEnsuresConstraints - (exprData_getPairA (data) ) ); - + exprNode_traversEnsuresConstraints + (exprData_getPairA (data))); + ret = constraintList_addListFree (ret, - exprNode_traversEnsuresConstraints - (exprData_getPairB (data) ) ); + exprNode_traversEnsuresConstraints + (exprData_getPairB (data))); break; case XPR_PREOP: - ret = constraintList_addListFree (ret, - exprNode_traversEnsuresConstraints - (exprData_getUopNode (data) ) ); + exprNode_traversEnsuresConstraints + (exprData_getUopNode (data))); break; case XPR_PARENS: ret = constraintList_addListFree (ret, exprNode_traversEnsuresConstraints - (exprData_getUopNode (data) ) ); + (exprData_getUopNode (data))); break; case XPR_INIT: ret = constraintList_addListFree (ret, exprNode_traversEnsuresConstraints - (exprData_getInitNode (data) ) ); - break; - - + (exprData_getInitNode (data))); + break; + + case XPR_ASSIGN: - ret = constraintList_addListFree (ret, - exprNode_traversEnsuresConstraints - (exprData_getOpA (data) ) ); - - ret = constraintList_addListFree (ret, - exprNode_traversEnsuresConstraints - (exprData_getOpB (data) ) ); - break; + ret = constraintList_addListFree (ret, + exprNode_traversEnsuresConstraints + (exprData_getOpA (data))); + + ret = constraintList_addListFree (ret, + exprNode_traversEnsuresConstraints + (exprData_getOpB (data))); + break; case XPR_OP: - ret = constraintList_addListFree (ret, - exprNode_traversEnsuresConstraints - (exprData_getOpA (data) ) ); - - ret = constraintList_addListFree (ret, - exprNode_traversEnsuresConstraints - (exprData_getOpB (data) ) ); - break; + ret = constraintList_addListFree (ret, + exprNode_traversEnsuresConstraints + (exprData_getOpA (data))); + + ret = constraintList_addListFree (ret, + exprNode_traversEnsuresConstraints + (exprData_getOpB (data))); + break; case XPR_SIZEOFT: break; case XPR_SIZEOF: - - ret = constraintList_addListFree (ret, - exprNode_traversEnsuresConstraints - (exprData_getSingle (data) ) ); - break; - + ret = constraintList_addListFree (ret, + exprNode_traversEnsuresConstraints + (exprData_getSingle (data))); + break; case XPR_CALL: ret = constraintList_addListFree (ret, - exprNode_traversEnsuresConstraints - (exprData_getFcn (data) ) ); - /*@i11*/ /* exprNodeList_unparse (exprData_getArgs (data) ); */ + exprNode_traversEnsuresConstraints + (exprData_getFcn (data))); + /*@i11*/ /* exprNodeList_unparse (exprData_getArgs (data)); */ break; - case XPR_RETURN: ret = constraintList_addListFree (ret, - exprNode_traversEnsuresConstraints - (exprData_getSingle (data) ) ); + exprNode_traversEnsuresConstraints + (exprData_getSingle (data))); break; - case XPR_NULLRETURN: break; - case XPR_FACCESS: ret = constraintList_addListFree (ret, exprNode_traversEnsuresConstraints - (exprData_getFieldNode (data) ) ); + (exprData_getFieldNode (data))); break; - case XPR_ARROW: ret = constraintList_addListFree (ret, exprNode_traversEnsuresConstraints - (exprData_getFieldNode (data) ) ); + (exprData_getFieldNode (data))); break; - case XPR_STRINGLITERAL: break; - case XPR_NUMLIT: break; case XPR_POSTOP: - - ret = constraintList_addListFree (ret, - exprNode_traversEnsuresConstraints - (exprData_getUopNode (data) ) ); - break; + ret = constraintList_addListFree (ret, + exprNode_traversEnsuresConstraints + (exprData_getUopNode (data))); + break; case XPR_CAST: - ret = constraintList_addListFree (ret, - exprNode_traversEnsuresConstraints - (exprData_getCastNode (data) ) ); + exprNode_traversEnsuresConstraints + (exprData_getCastNode (data))); break; - default: break; } - - DPRINTF( (message ( - "exprnode_traversEnsuresConstraints call for %s with constraintList of is returning %s", - exprNode_unparse (e), - constraintList_print(ret)))); + + DPRINTF((message ("exprnode_traversEnsuresConstraints call for %s with " + "constraintList of is returning %s", + exprNode_unparse (e), + constraintList_print(ret)))); return ret; } /*drl moved out of constraintResolve.c 07-02-001 */ -void checkArgumentList (/*@out@*/ exprNode temp, exprNodeList arglist, fileloc sequencePoint) +void checkArgumentList (/*@out@*/ exprNode temp, exprNodeList arglist, + fileloc sequencePoint) { temp->requiresConstraints = constraintList_makeNew(); temp->ensuresConstraints = constraintList_makeNew(); @@ -2138,7 +2155,7 @@ constraintList exprNode_getPostConditions (exprNode fcn, exprNodeList arglist, e { constraintList postconditions; uentry temp; - DPRINTF( (message ("Got call that %s ( %s) ", exprNode_unparse(fcn), exprNodeList_unparse (arglist ) ) ) ); + DPRINTF((message ("Got call that %s (%s) ", exprNode_unparse(fcn), exprNodeList_unparse (arglist)))); temp = exprNode_getUentry (fcn); @@ -2157,19 +2174,63 @@ constraintList exprNode_getPostConditions (exprNode fcn, exprNodeList arglist, e return postconditions; } +/* +comment this out for now +we'll include it in a production release when its stable... + + void findStructs (exprNodeList arglist) +{ + + ctype ct, rt; + + DPRINTF(( + message("doing findStructs: %s", exprNodeList_unparse(arglist)) + )); + + + exprNodeList_elements(arglist, expr) + { + ct = exprNode_getType(expr); + + rt = ctype_realType (ct); + + if (ctype_isStruct (rt)) + TPRINTF((message("Found structure %s", exprNode_unparse(expr)) + )); + if (hasInvariants(ct)) + { + constraintList invars; + + invars = getInvariants(ct); + + + TPRINTF((message ("findStructs has invariants %s ", constraintList_print (invars)) + )); + + invars = constraintList_doSRefFixStructConstraint(invars, exprNode_getSref(expr), ct); + + + TPRINTF((message ("findStructs finded invariants to be %s ", constraintList_print (invars)) + )); + } + } + end_exprNodeList_elements; +} + +*/ /*drl moved out of constraintResolve.c 07-02-001 */ constraintList checkCall (/*@dependent@*/ exprNode fcn, exprNodeList arglist) { constraintList preconditions; uentry temp; - DPRINTF( (message ("Got call that %s ( %s) ", exprNode_unparse(fcn), exprNodeList_unparse (arglist ) ) ) ); + DPRINTF((message ("Got call that %s (%s) ", exprNode_unparse(fcn), exprNodeList_unparse (arglist)))); temp = exprNode_getUentry (fcn); preconditions = uentry_getFcnPreconditions (temp); - if (constraintList_isDefined(preconditions) ) + if (constraintList_isDefined(preconditions)) { preconditions = constraintList_togglePost (preconditions); preconditions = constraintList_preserveCallInfo(preconditions, fcn); @@ -2177,11 +2238,57 @@ constraintList checkCall (/*@dependent@*/ exprNode fcn, exprNodeList arglist) } else { - if (constraintList_isUndefined(preconditions) ) + if (constraintList_isUndefined(preconditions)) preconditions = constraintList_makeNew(); } - DPRINTF (( message("Done checkCall\n") )); - DPRINTF (( message("Returning list %q ", constraintList_printDetailed(preconditions) ) )); + + // drl remember to remove this code before you make a pslint release. + /* + if (context_getFlag (FLG_IMPLICTCONSTRAINT) ) + { + + uentryList_elements (params, el) + { + DPRINTF((message("setImplictfcnConstraints doing: %s", uentry_unparse(el) ) )); + + s = uentry_getSref(el); + if (sRef_isReference (s) ) + { + DPRINTF((message ("%s is a pointer", sRef_unparse(s) ) )); + } + else + { + DPRINTF((message ("%s is NOT a pointer", sRef_unparse(s) ) )); + } + //drl 4/26/01 + //chagned this from MaxSet(s) == 0 to MaxSet(s) >= 0 + c = constraint_makeSRefWriteSafeInt (s, 0); + + implicitFcnConstraints = constraintList_add(implicitFcnConstraints , c); + + //drl 10/23/2002 added support for out + if (!uentry_isOut(el) ) + { + c = constraint_makeSRefReadSafeInt (s, 0); + + implicitFcnConstraints = constraintList_add(implicitFcnConstraints , c); + } + + + } + + } + */ + DPRINTF ((message("Done checkCall\n"))); + DPRINTF ((message("Returning list %q ", constraintList_printDetailed(preconditions)))); + + /* + drl we're going to comment this out for now + we'll include it if we're sure it's working + + findStructs(arglist); + */ + return preconditions; } @@ -2194,7 +2301,7 @@ constraintList checkCall (/*@dependent@*/ exprNode fcn, exprNodeList arglist) but this is the easy way to do this If I have time I'd like to cause the exprNode to get created correctly in the first place */ /*@i223*/ -void exprNode_findValue( exprNode e) +void exprNode_findValue(exprNode e) { exprData data; @@ -2203,7 +2310,7 @@ void exprNode_findValue( exprNode e) data = e->edata; - if (exprNode_hasValue(e) ) + if (exprNode_hasValue(e)) return; if (e->kind == XPR_OP) @@ -2215,31 +2322,33 @@ void exprNode_findValue( exprNode e) exprNode_findValue(t1); exprNode_findValue(t2); - if (!(exprNode_knownIntValue(t1) && (exprNode_knownIntValue(t2) ) ) ) + if (!(exprNode_knownIntValue(t1) && (exprNode_knownIntValue(t2)))) return; - if (lltok_isPlus_Op (tok) ) + if (lltok_isPlus_Op (tok)) { long v1, v2; v1 = exprNode_getLongValue(t1); v2 = exprNode_getLongValue(t2); - if (multiVal_isDefined(e->val) ) + if (multiVal_isDefined(e->val)) multiVal_free (e->val); e->val = multiVal_makeInt (v1 + v2); } - if ( lltok_isMinus_Op (tok) ) + if (lltok_isMinus_Op (tok)) { long v1, v2; v1 = exprNode_getLongValue(t1); v2 = exprNode_getLongValue(t2); - if (multiVal_isDefined(e->val) ) - multiVal_free (e->val); + if (multiVal_isDefined(e->val)) + { + multiVal_free (e->val); + } e->val = multiVal_makeInt (v1 - v2); }