X-Git-Url: http://andersk.mit.edu/gitweb/splint.git/blobdiff_plain/470b7798e9c04260b853bd5600fefc03abb04dfe..2934b455c4074408a0f819009c071456f021ba21:/src/constraintGeneration.c diff --git a/src/constraintGeneration.c b/src/constraintGeneration.c index 2e460e4..b5dffe2 100644 --- a/src/constraintGeneration.c +++ b/src/constraintGeneration.c @@ -15,9 +15,10 @@ # include "aliasChecks.h" # include "exprNodeSList.h" -# include "exprData.i" # include "exprDataQuite.i" +/*@access exprNode @*/ + extern void forLoopHeuristics( exprNode e, exprNode forPred, exprNode forBody); bool /*@alt void@*/ exprNode_generateConstraints (/*@temp@*/ exprNode e); @@ -25,23 +26,16 @@ static bool exprNode_handleError( exprNode p_e); //static cstring exprNode_findConstraints ( exprNode p_e); static bool exprNode_isMultiStatement(exprNode p_e); -static bool exprNode_multiStatement (exprNode p_e); -bool exprNode_exprTraverse (exprNode e, bool definatelv, bool definaterv, fileloc sequencePoint); +static void exprNode_multiStatement (exprNode p_e); + //static void exprNode_constraintPropagateUp (exprNode p_e); -constraintList exprNode_traversRequiresConstraints (exprNode e); -constraintList exprNode_traversEnsuresConstraints (exprNode e); -constraintList exprNode_traversTrueEnsuresConstraints (exprNode e); -constraintList exprNode_traversFalseEnsuresConstraints (exprNode e); +static constraintList exprNode_traversTrueEnsuresConstraints (exprNode e); +static constraintList exprNode_traversFalseEnsuresConstraints (exprNode e); -extern constraintList reflectChanges (constraintList pre2, constraintList post1); +exprNode makeDataTypeConstraints (/*@returned@*/ exprNode e); -void mergeResolve (exprNode parent, exprNode child1, exprNode child2); -exprNode makeDataTypeConstraints (exprNode e); constraintList constraintList_makeFixedArrayConstraints (sRefSet s); -constraintList checkCall (exprNode fcn, exprNodeList arglist); - -void checkArgumentList (exprNode temp, exprNodeList arglist, fileloc sequencePoint); //bool exprNode_testd() //{ @@ -54,7 +48,7 @@ void checkArgumentList (exprNode temp, exprNodeList arglist, fileloc sequencePoi */ //} -bool exprNode_isUnhandled (exprNode e) +static bool exprNode_isUnhandled (exprNode e) { llassert( exprNode_isDefined(e) ); switch (e->kind) @@ -117,11 +111,12 @@ bool /*@alt void@*/ exprNode_generateConstraints (/*@temp@*/ exprNode e) { if (exprNode_isError (e) ) return FALSE; - - e->requiresConstraints = constraintList_new(); - e->ensuresConstraints = constraintList_new(); - e->trueEnsuresConstraints = constraintList_new(); - e->falseEnsuresConstraints = constraintList_new(); + /* + e->requiresConstraints = constraintList_makeNew(); + e->ensuresConstraints = constraintList_makeNew(); + e->trueEnsuresConstraints = constraintList_makeNew(); + e->falseEnsuresConstraints = constraintList_makeNew(); + */ if (exprNode_isUnhandled (e) ) { @@ -146,7 +141,7 @@ bool /*@alt void@*/ exprNode_generateConstraints (/*@temp@*/ exprNode e) loc = exprNode_getNextSequencePoint(e); exprNode_exprTraverse(e, FALSE, FALSE, loc); - // llassert(FALSE); + fileloc_free(loc); return FALSE; } @@ -154,14 +149,14 @@ bool /*@alt void@*/ exprNode_generateConstraints (/*@temp@*/ exprNode e) constraintList c; c = constraintList_makeFixedArrayConstraints (e->uses); - e->requiresConstraints = reflectChanges (e->requiresConstraints, c); + e->requiresConstraints = reflectChangesFreePre (e->requiresConstraints, c); // e->ensuresConstraints = constraintList_mergeEnsures(c, e->ensuresConstraints); + constraintList_free(c); } - /* printf ("%s", (message ("%s", constraintList_printDetailed (e->requiresConstraints) ) ) ); - printf ("%s", (message ("%s", constraintList_printDetailed (e->ensuresConstraints) ) ) ); */ + DPRINTF ( (message ("e->requiresConstraints %s", constraintList_printDetailed (e->requiresConstraints) ) ) ); return FALSE; } @@ -192,19 +187,18 @@ if (exprNode_handleError (e) != NULL) } -bool exprNode_stmt (exprNode e) +static void exprNode_stmt (exprNode e) { exprNode snode; fileloc loc; - bool notError; - char * s; + cstring s; if (exprNode_isError(e) ) { - return FALSE; + return; // FALSE; } - e->requiresConstraints = constraintList_new(); - e->ensuresConstraints = constraintList_new(); + /*e->requiresConstraints = constraintList_makeNew(); + e->ensuresConstraints = constraintList_makeNew(); */ // e = makeDataTypeConstraints(e); @@ -214,13 +208,21 @@ bool exprNode_stmt (exprNode e) if (e->kind == XPR_INIT) { + constraintList tempList; DPRINTF (("Init") ); DPRINTF ( (message ("%s ", exprNode_unparse (e)) ) ); loc = exprNode_getNextSequencePoint(e); /* reduces to an expression */ - notError = exprNode_exprTraverse (e, FALSE, FALSE, loc); + exprNode_exprTraverse (e, FALSE, FALSE, loc); + fileloc_free(loc); + + tempList = e->requiresConstraints; e->requiresConstraints = exprNode_traversRequiresConstraints(e); + constraintList_free(tempList); + + tempList = e->ensuresConstraints; e->ensuresConstraints = exprNode_traversEnsuresConstraints(e); - return notError; + constraintList_free(tempList); + return; // notError; } if (e->kind != XPR_STMT) @@ -232,8 +234,8 @@ bool exprNode_stmt (exprNode e) { return exprNode_multiStatement (e ); } - BPRINTF( (message ("Ignoring non-statement %s", exprNode_unparse(e) ) ) ); - return TRUE; + DPRINTF( (message ("Ignoring non-statement %s", exprNode_unparse(e) ) ) ); + return; //TRUE; // llassert(FALSE); } @@ -248,43 +250,56 @@ bool exprNode_stmt (exprNode e) if (exprNode_isMultiStatement (snode)) { - bool temp; - - temp = exprNode_multiStatement (snode); - exprNode_copyConstraints (e, snode); - return temp; + exprNode_multiStatement (snode); + (void) exprNode_copyConstraints (e, snode); + return; } loc = exprNode_getNextSequencePoint(e); /* reduces to an expression */ - notError = exprNode_exprTraverse (snode, FALSE, FALSE, loc); + //notError = + exprNode_exprTraverse (snode, FALSE, FALSE, loc); + + fileloc_free(loc); + + constraintList_free (e->requiresConstraints); e->requiresConstraints = exprNode_traversRequiresConstraints(snode); // printf ("For: %s \n", exprNode_unparse (e) ); // printf ("%s\n", constraintList_print(e->requiresConstraints) ); + + constraintList_free (e->ensuresConstraints); e->ensuresConstraints = exprNode_traversEnsuresConstraints(snode); // printf ("Ensures that:\n %s\n", constraintList_print(e->ensuresConstraints) ); // llassert(notError); - return notError; + + DPRINTF ( (message ("smtlist constraints are: pre: %s \n and \t post %s\n", + constraintList_print(e->requiresConstraints), + constraintList_print(e->ensuresConstraints) ) ) ); + + return; // notError; } -bool exprNode_stmtList (exprNode e) +static void exprNode_stmtList (exprNode e) { exprNode stmt1, stmt2; if (exprNode_isError (e) ) { - return FALSE; + return; // FALSE; } - e->requiresConstraints = constraintList_new(); - e->ensuresConstraints = constraintList_new(); + /* + e->requiresConstraints = constraintList_makeNew(); + e->ensuresConstraints = constraintList_makeNew(); + */ // e = makeDataTypeConstraints(e); /*Handle case of stmtList with only one statement: The parse tree stores this as stmt instead of stmtList*/ if (e->kind != XPR_STMTLIST) { - return exprNode_stmt(e); + exprNode_stmt(e); + return; } llassert (e->kind == XPR_STMTLIST); DPRINTF(( "STMTLIST:") ); @@ -305,34 +320,80 @@ bool exprNode_stmtList (exprNode e) DPRINTF ( (message ("smtlist constraints are: pre: %s \n and \t post %s\n", constraintList_print(e->requiresConstraints), constraintList_print(e->ensuresConstraints) ) ) ); - return TRUE; + return; // TRUE; } -exprNode doIf (exprNode e, exprNode test, exprNode body) +static exprNode doIf (/*@returned@*/ exprNode e, exprNode test, exprNode body) { + constraintList temp; + DPRINTF ((message ("doIf: %s ", exprNode_unparse(e) ) ) ); - llassert(test); - llassert(e); - llassert(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 ("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 ("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 ("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 ("falseEnsures constraints for %s are %s", exprNode_unparse(test), constraintList_printDetailed(test->falseEnsuresConstraints) ) )); + + + + temp = test->trueEnsuresConstraints; + test->trueEnsuresConstraints = exprNode_traversTrueEnsuresConstraints(test); + constraintList_free(temp); + + temp = test->ensuresConstraints; test->ensuresConstraints = exprNode_traversEnsuresConstraints (test); + constraintList_free(temp); + + temp = test->requiresConstraints; test->requiresConstraints = exprNode_traversRequiresConstraints (test); - - test->trueEnsuresConstraints = exprNode_traversTrueEnsuresConstraints(test); + constraintList_free(temp); + + test->trueEnsuresConstraints = constraintList_substituteFreeTarget(test->trueEnsuresConstraints, test->ensuresConstraints); + + DPRINTF ((message ("doIf: test ensures %s ", constraintList_print(test->ensuresConstraints) ) ) ); + + DPRINTF ((message ("doIf: test true ensures %s ", constraintList_print(test->trueEnsuresConstraints) ) ) ); + + constraintList_free(e->requiresConstraints); e->requiresConstraints = reflectChanges (body->requiresConstraints, test->trueEnsuresConstraints); - e->requiresConstraints = reflectChanges (e->requiresConstraints, + + e->requiresConstraints = reflectChangesFreePre (e->requiresConstraints, test->ensuresConstraints); + temp = e->requiresConstraints; e->requiresConstraints = constraintList_mergeRequires (e->requiresConstraints, test->requiresConstraints); - + constraintList_free(temp); + + #warning bad + constraintList_free(e->ensuresConstraints); e->ensuresConstraints = constraintList_copy (test->ensuresConstraints); - /* - if (!exprNode_mayEscape (body) ) - e->ensuresConstraints = constraintList_mergeEnsures (e->ensuresConstraints, + + if (exprNode_mayEscape (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) ) ) ); return e; @@ -349,41 +410,56 @@ exprNode doIf (exprNode e, exprNode test, exprNode body) */ -exprNode doIfElse (/*@returned@*/ exprNode e, exprNode p, exprNode trueBranch, exprNode falseBranch) +static exprNode doIfElse (/*@returned@*/ exprNode e, exprNode p, exprNode trueBranch, exprNode falseBranch) { - constraintList c1, cons, t, f; + constraintList c1, cons, t, t2, f, f2; + + DPRINTF ((message ("doIfElse: %s ", exprNode_unparse(e) ) ) ); // do requires clauses c1 = constraintList_copy (p->ensuresConstraints); t = reflectChanges (trueBranch->requiresConstraints, p->trueEnsuresConstraints); - t = reflectChanges (t, p->ensuresConstraints); + t = reflectChangesFreePre (t, p->ensuresConstraints); - // e->requiresConstraints = constraintList_copy (cons); - cons = reflectChanges (falseBranch->requiresConstraints, p->falseEnsuresConstraints); - cons = reflectChanges (cons, c1); + cons = reflectChangesFreePre (cons, c1); - e->requiresConstraints = constraintList_mergeRequires (t, cons); - e->requiresConstraints = constraintList_mergeRequires (e->requiresConstraints, p->requiresConstraints); + constraintList_free(e->requiresConstraints); + e->requiresConstraints = constraintList_mergeRequiresFreeFirst (t, cons); + e->requiresConstraints = constraintList_mergeRequiresFreeFirst (e->requiresConstraints, p->requiresConstraints); // do ensures clauses // find the the ensures lists for each subbranch t = constraintList_mergeEnsures (p->trueEnsuresConstraints, trueBranch->ensuresConstraints); + t2 = t; t = constraintList_mergeEnsures (p->ensuresConstraints, t); - + constraintList_free(t2); + f = constraintList_mergeEnsures (p->falseEnsuresConstraints, falseBranch->ensuresConstraints); + f2 = f; f = constraintList_mergeEnsures (p->ensuresConstraints, f); + constraintList_free(f2); // find ensures for whole if/else statement + constraintList_free(e->ensuresConstraints); + e->ensuresConstraints = constraintList_logicalOr (t, f); + constraintList_free(t); + constraintList_free(f); + 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) ) ) ); + return e; } -exprNode doWhile (exprNode e, exprNode test, exprNode body) +static exprNode doWhile (/*@returned@*/ exprNode e, exprNode test, exprNode body) { DPRINTF ((message ("doWhile: %s ", exprNode_unparse(e) ) ) ); return doIf (e, test, body); @@ -393,23 +469,23 @@ constraintList constraintList_makeFixedArrayConstraints (sRefSet s) { constraintList ret; constraint con; - ret = constraintList_new(); + ret = constraintList_makeNew(); sRefSet_elements (s, el) { // llassert (el); if (sRef_isFixedArray(el) ) { - int s; + long int size; DPRINTF( (message("%s is a fixed array", sRef_unparse(el)) ) ); //if (el->kind == SK_DERIVED) // break; //hack until I find the real problem - s = sRef_getArraySize(el); + size = sRef_getArraySize(el); DPRINTF( (message("%s is a fixed array with size %d", - sRef_unparse(el), s) ) ); - con = constraint_makeSRefSetBufferSize (el, (s - 1)); - //con = constraint_makeSRefWriteSafeInt (el, (s - 1)); + sRef_unparse(el), (int)size) ) ); + con = constraint_makeSRefSetBufferSize (el, (size - 1)); + //con = constraint_makeSRefWriteSafeInt (el, (size - 1)); ret = constraintList_add(ret, con); } else @@ -438,19 +514,19 @@ constraintList constraintList_makeFixedArrayConstraints (sRefSet s) return ret; } -exprNode makeDataTypeConstraints (exprNode e) +exprNode makeDataTypeConstraints (/*@returned@*/ exprNode e) { constraintList c; DPRINTF(("makeDataTypeConstraints")); c = constraintList_makeFixedArrayConstraints (e->uses); - e->ensuresConstraints = constraintList_addList (e->ensuresConstraints, c); + e->ensuresConstraints = constraintList_addListFree (e->ensuresConstraints, c); return e; } -void doFor (exprNode e, exprNode forPred, exprNode forBody) +static void doFor (exprNode e, exprNode forPred, exprNode forBody) { exprNode init, test, inc; //merge the constraints: modle as if statement @@ -470,14 +546,17 @@ void doFor (exprNode e, exprNode forPred, exprNode forBody) forLoopHeuristics(e, forPred, forBody); + constraintList_free(e->requiresConstraints); e->requiresConstraints = reflectChanges (forBody->requiresConstraints, test->ensuresConstraints); - e->requiresConstraints = reflectChanges (e->requiresConstraints, test->trueEnsuresConstraints); - e->requiresConstraints = reflectChanges (e->requiresConstraints, forPred->ensuresConstraints); + e->requiresConstraints = reflectChangesFreePre (e->requiresConstraints, test->trueEnsuresConstraints); + e->requiresConstraints = reflectChangesFreePre (e->requiresConstraints, forPred->ensuresConstraints); if (!forBody->canBreak) { - e->ensuresConstraints = constraintList_addList(e->ensuresConstraints, forPred->ensuresConstraints); - e->ensuresConstraints = constraintList_addList(e->ensuresConstraints, test->falseEnsuresConstraints); + e->ensuresConstraints = constraintList_addListFree(e->ensuresConstraints, constraintList_copy(forPred->ensuresConstraints) ); + e->ensuresConstraints = constraintList_addListFree(e->ensuresConstraints,constraintList_copy( test->falseEnsuresConstraints)); + // forPred->ensuresConstraints = constraintList_undefined; + // test->falseEnsuresConstraints = constraintList_undefined; } else { @@ -486,14 +565,14 @@ void doFor (exprNode e, exprNode forPred, exprNode forBody) } -exprNode doSwitch (/*@returned@*/ exprNode e) +static exprNode doSwitch (/*@returned@*/ exprNode e) { exprNode body; exprData data; data = e->edata; llassert(FALSE); - //TPRINTF (( message ("doSwitch for: switch (%s) %s", + //DPRINTF (( message ("doSwitch for: switch (%s) %s", // exprNode_unparse (exprData_getPairA (data)), // exprNode_unparse (exprData_getPairB (data))) )); @@ -508,7 +587,7 @@ exprNode doSwitch (/*@returned@*/ exprNode e) } -bool exprNode_multiStatement (exprNode e) +void exprNode_multiStatement (exprNode e) { bool ret; @@ -517,12 +596,15 @@ bool exprNode_multiStatement (exprNode e) exprNode p, trueBranch, falseBranch; exprNode forPred, forBody; exprNode test; - // constraintList t, f; - e->requiresConstraints = constraintList_new(); - e->ensuresConstraints = constraintList_new(); - e->trueEnsuresConstraints = constraintList_new(); - e->falseEnsuresConstraints = constraintList_new(); + constraintList temp; + + // constraintList t, f; + /*e->requiresConstraints = constraintList_makeNew(); + e->ensuresConstraints = constraintList_makeNew(); + e->trueEnsuresConstraints = constraintList_makeNew(); + e->falseEnsuresConstraints = constraintList_makeNew(); + */ // e = makeDataTypeConstraints(e); DPRINTF((message ("exprNode_multistatement Analysising %s %s at", exprNode_unparse( e), @@ -530,7 +612,7 @@ bool exprNode_multiStatement (exprNode e) if (exprNode_handleError (e)) { - return FALSE; + return; // FALSE; } data = e->edata; @@ -562,8 +644,13 @@ bool exprNode_multiStatement (exprNode e) exprNode_generateConstraints (exprData_getTripleInc (data) ); if (!exprNode_isError(test) ) - test->trueEnsuresConstraints = exprNode_traversTrueEnsuresConstraints(test); - + { + constraintList temp2; + temp2 = test->trueEnsuresConstraints; + test->trueEnsuresConstraints = exprNode_traversTrueEnsuresConstraints(test); + constraintList_free(temp2); + } + exprNode_generateConstraints (exprData_getTripleInc (data)); break; @@ -591,7 +678,6 @@ bool exprNode_multiStatement (exprNode e) FALSE, FALSE, exprNode_loc(e1)); exprNode_generateConstraints (e2); - e = doIf (e, e1, e2); @@ -611,11 +697,21 @@ bool exprNode_multiStatement (exprNode e) exprNode_generateConstraints (trueBranch); exprNode_generateConstraints (falseBranch); + temp = p->ensuresConstraints; p->ensuresConstraints = exprNode_traversEnsuresConstraints (p); + constraintList_free(temp); + + temp = p->requiresConstraints; p->requiresConstraints = exprNode_traversRequiresConstraints (p); - + constraintList_free(temp); + + temp = p->trueEnsuresConstraints; p->trueEnsuresConstraints = exprNode_traversTrueEnsuresConstraints(p); + constraintList_free(temp); + + temp = p->falseEnsuresConstraints; p->falseEnsuresConstraints = exprNode_traversFalseEnsuresConstraints(p); + constraintList_free(temp); e = doIfElse (e, p, trueBranch, falseBranch); DPRINTF( ("Done IFELSE") ); @@ -637,7 +733,11 @@ bool exprNode_multiStatement (exprNode e) case XPR_BLOCK: // ret = message ("{ %s }", exprNode_generateConstraints (exprData_getSingle (data)); + + constraintList_free(e->requiresConstraints); e->requiresConstraints = constraintList_copy ( (exprData_getSingle (data))->requiresConstraints ); + + constraintList_free(e->ensuresConstraints); e->ensuresConstraints = constraintList_copy ( (exprData_getSingle (data))->ensuresConstraints ); // e->constraints = (exprData_getSingle (data))->constraints; break; @@ -647,16 +747,17 @@ bool exprNode_multiStatement (exprNode e) break; case XPR_STMT: case XPR_STMTLIST: - return exprNode_stmtList (e); + exprNode_stmtList (e); + return ; /*@notreached@*/ break; default: ret=FALSE; } - return ret; + return; // ret; } -bool lltok_isBoolean_Op (lltok tok) +static bool lltok_isBoolean_Op (lltok tok) { /*this should really be a switch statement but I don't want to violate the abstraction @@ -701,13 +802,13 @@ bool lltok_isBoolean_Op (lltok tok) } -void exprNode_booleanTraverse (exprNode e, bool definatelv, bool definaterv, fileloc sequencePoint) +static void exprNode_booleanTraverse (exprNode e, /*@unused@*/ bool definatelv, /*@unused@*/ bool definaterv, fileloc sequencePoint) { constraint cons; exprNode t1, t2; exprData data; lltok tok; -constraintList tempList; +constraintList tempList, temp; data = e->edata; tok = exprData_getOpTok (data); @@ -774,34 +875,45 @@ if (lltok_isLe_Op (tok) ) //true ensures tempList = constraintList_copy (t1->trueEnsuresConstraints); tempList = constraintList_addList (tempList, t2->trueEnsuresConstraints); - e->trueEnsuresConstraints = constraintList_addList(e->trueEnsuresConstraints, tempList); + e->trueEnsuresConstraints = constraintList_addListFree(e->trueEnsuresConstraints, tempList); //false ensures: fens t1 or tens t1 and fens t2 tempList = constraintList_copy (t1->trueEnsuresConstraints); tempList = constraintList_addList (tempList, t2->falseEnsuresConstraints); + temp = tempList; tempList = constraintList_logicalOr (tempList, t1->falseEnsuresConstraints); + constraintList_free(temp); + e->falseEnsuresConstraints =constraintList_addList(e->falseEnsuresConstraints, tempList); } - - if (lltok_isOr_Op (tok) ) - { + else if (lltok_isOr_Op (tok) ) + { //false ensures tempList = constraintList_copy (t1->falseEnsuresConstraints); tempList = constraintList_addList (tempList, t2->falseEnsuresConstraints); - e->falseEnsuresConstraints = constraintList_addList(e->falseEnsuresConstraints, tempList); + e->falseEnsuresConstraints = constraintList_addListFree(e->falseEnsuresConstraints, tempList); //true ensures: tens t1 or fens t1 and tens t2 tempList = constraintList_copy (t1->falseEnsuresConstraints); tempList = constraintList_addList (tempList, t2->trueEnsuresConstraints); + + temp = tempList; tempList = constraintList_logicalOr (tempList, t1->trueEnsuresConstraints); - e->trueEnsuresConstraints =constraintList_addList(e->trueEnsuresConstraints, tempList); + constraintList_free(temp); + + + e->trueEnsuresConstraints =constraintList_addListFree(e->trueEnsuresConstraints, tempList); } + else + { + DPRINTF((message("%s is not a boolean operation", lltok_unparse(tok) ) )); + } } -bool exprNode_exprTraverse (exprNode e, bool definatelv, bool definaterv, fileloc sequencePoint) +void exprNode_exprTraverse (exprNode e, bool definatelv, bool definaterv, /*@observer@*/ fileloc sequencePoint) { exprNode t1, t2, fcn; lltok tok; @@ -809,22 +921,24 @@ bool exprNode_exprTraverse (exprNode e, bool definatelv, bool definaterv, filel exprData data; constraint cons; + constraintList temp; + if (exprNode_isError(e) ) { - return FALSE; + return; // FALSE; } DPRINTF((message ("exprNode_exprTraverset Analysising %s %s at", exprNode_unparse( e), fileloc_unparse(exprNode_getfileloc(e) ) ) ) ); - e->requiresConstraints = constraintList_new(); - e->ensuresConstraints = constraintList_new(); - e->trueEnsuresConstraints = constraintList_new();; - e->falseEnsuresConstraints = constraintList_new();; - + /*e->requiresConstraints = constraintList_makeNew(); + e->ensuresConstraints = constraintList_makeNew(); + e->trueEnsuresConstraints = constraintList_makeNew();; + e->falseEnsuresConstraints = constraintList_makeNew();; + */ if (exprNode_isUnhandled (e) ) { - return FALSE; + return; // FALSE; } // e = makeDataTypeConstraints (e); @@ -866,7 +980,7 @@ bool exprNode_exprTraverse (exprNode e, bool definatelv, bool definaterv, filel // cons = constraint_makeEnsureMinReadAtMost (t1, t2, sequencePoint); // e->ensuresConstraints = constraintList_add(e->ensuresConstraints, cons); - + exprNode_exprTraverse (exprData_getPairA (data), FALSE, TRUE, sequencePoint); exprNode_exprTraverse (exprData_getPairB (data), FALSE, TRUE, sequencePoint); @@ -896,7 +1010,8 @@ bool exprNode_exprTraverse (exprNode e, bool definatelv, bool definaterv, filel t1 = exprData_getOpA (data); t2 = exprData_getOpB (data); exprNode_exprTraverse (t1, TRUE, definaterv, sequencePoint ); - lltok_unparse (exprData_getOpTok (data)); + //lltok_unparse (exprData_getOpTok (data)); + #warning check this for += -= etc exprNode_exprTraverse (t2, definatelv, TRUE, sequencePoint ); /* this test is nessecary because some expressions generate a null expression node. function pointer do that -- drl */ @@ -914,13 +1029,29 @@ bool exprNode_exprTraverse (exprNode e, bool definatelv, bool definaterv, filel tok = exprData_getOpTok (data); exprNode_exprTraverse (t2, definatelv, definaterv, sequencePoint ); + #warning fix definatelv and definaterv + + if (tok.tok == ADD_ASSIGN) + { + cons = constraint_makeAddAssign (t1, t2, sequencePoint ); + e->ensuresConstraints = constraintList_add(e->ensuresConstraints, cons); + } + + if (tok.tok == SUB_ASSIGN) + { + cons = constraint_makeSubtractAssign (t1, t2, sequencePoint ); + e->ensuresConstraints = constraintList_add(e->ensuresConstraints, cons); + } + + + if (lltok_isBoolean_Op (tok) ) exprNode_booleanTraverse (e, definatelv, definaterv, sequencePoint); // e->constraints = constraintList_exprNodemerge (exprData_getOpA (data), exprData_getOpB (data)); break; case XPR_SIZEOFT: - ctype_unparse (qtype_getType (exprData_getType (data) ) ); + #warning make sure the case can be ignored.. break; @@ -933,13 +1064,12 @@ bool exprNode_exprTraverse (exprNode e, bool definatelv, bool definaterv, filel fcn = exprData_getFcn(data); exprNode_exprTraverse (fcn, definatelv, definaterv, sequencePoint ); - exprNodeList_unparse (exprData_getArgs (data) ); DPRINTF ( (message ("Got call that %s ( %s) ", exprNode_unparse(fcn), exprNodeList_unparse (exprData_getArgs (data) ) ) ) ); - fcn->requiresConstraints = constraintList_addList (fcn->requiresConstraints, + fcn->requiresConstraints = constraintList_addListFree (fcn->requiresConstraints, checkCall (fcn, exprData_getArgs (data) ) ); - fcn->ensuresConstraints = constraintList_addList (fcn->ensuresConstraints, + fcn->ensuresConstraints = constraintList_addListFree (fcn->ensuresConstraints, getPostConditions(fcn, exprData_getArgs (data),e ) ); t1 = exprNode_createNew (exprNode_getType (e) ); @@ -957,26 +1087,24 @@ bool exprNode_exprTraverse (exprNode e, bool definatelv, bool definaterv, filel break; case XPR_NULLRETURN: - cstring_makeLiteral ("return");; + break; case XPR_FACCESS: exprNode_exprTraverse (exprData_getFieldNode (data), definatelv, definaterv, sequencePoint ); - exprData_getFieldName (data) ; break; case XPR_ARROW: exprNode_exprTraverse (exprData_getFieldNode (data), definatelv, definaterv, sequencePoint ); - exprData_getFieldName (data); break; case XPR_STRINGLITERAL: - cstring_copy (exprData_getLiteral (data)); + break; case XPR_NUMLIT: - cstring_copy (exprData_getLiteral (data)); + break; case XPR_PREOP: @@ -999,8 +1127,7 @@ bool exprNode_exprTraverse (exprNode e, bool definatelv, bool definaterv, filel cons = constraint_makeMaxSetSideEffectPostDecrement (t1, sequencePoint ); e->ensuresConstraints = constraintList_add (e->ensuresConstraints, cons); } - - if (lltok_isMult( exprData_getUopTok (data) ) ) + else if (lltok_isMult( tok ) ) { if (definatelv) { @@ -1012,19 +1139,43 @@ bool exprNode_exprTraverse (exprNode e, bool definatelv, bool definaterv, filel } e->requiresConstraints = constraintList_add(e->requiresConstraints, cons); } - - /* ! expr */ - if (lltok_isNot_Op (exprData_getUopTok (data) ) ) + else if (lltok_isNot_Op (tok) ) + /* ! expr */ { + constraintList_free(e->trueEnsuresConstraints); + e->trueEnsuresConstraints = constraintList_copy (t1->falseEnsuresConstraints); + constraintList_free(e->falseEnsuresConstraints); e->falseEnsuresConstraints = constraintList_copy (t1->trueEnsuresConstraints); } + + else if (lltok_isAmpersand_Op (tok) ) + { + break; + } + else if (lltok_isMinus_Op (tok) ) + { + break; + } + else if ( lltok_isExcl_Op (tok) ) + { + break; + } + else if (lltok_isTilde_Op (tok) ) + { + break; + } + else + { + llcontbug((message("Unsupported preop in %s", exprNode_unparse(e) ) )); + BADEXIT; + } break; case XPR_POSTOP: exprNode_exprTraverse (exprData_getUopNode (data), TRUE, definaterv, sequencePoint ); - lltok_unparse (exprData_getUopTok (data)); + if (lltok_isInc_Op (exprData_getUopTok (data) ) ) { DPRINTF(("doing ++")); @@ -1053,26 +1204,64 @@ bool exprNode_exprTraverse (exprNode e, bool definatelv, bool definaterv, filel false = 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 (true, FALSE, TRUE, sequencePoint ); + + temp = true->ensuresConstraints; true->ensuresConstraints = exprNode_traversEnsuresConstraints(true); + constraintList_free(temp); + + + temp = true->requiresConstraints; true->requiresConstraints = exprNode_traversRequiresConstraints(true); + constraintList_free(temp); + + temp = true->trueEnsuresConstraints; true->trueEnsuresConstraints = exprNode_traversTrueEnsuresConstraints(true); + constraintList_free(temp); + + temp = true->falseEnsuresConstraints; true->falseEnsuresConstraints = exprNode_traversFalseEnsuresConstraints(true); + constraintList_free(temp); + //dfdf exprNode_exprTraverse (false, FALSE, TRUE, sequencePoint ); + + temp = false->ensuresConstraints; false->ensuresConstraints = exprNode_traversEnsuresConstraints(false); + constraintList_free(temp); + + + temp = false->requiresConstraints; false->requiresConstraints = exprNode_traversRequiresConstraints(false); + constraintList_free(temp); + + temp = false->trueEnsuresConstraints; false->trueEnsuresConstraints = exprNode_traversTrueEnsuresConstraints(false); - false->falseEnsuresConstraints = exprNode_traversFalseEnsuresConstraints(false); + constraintList_free(temp); + temp = false->falseEnsuresConstraints; + false->falseEnsuresConstraints = exprNode_traversFalseEnsuresConstraints(false); + constraintList_free(temp); /* if pred is true e equals true otherwise pred equals false */ @@ -1108,9 +1297,15 @@ bool exprNode_exprTraverse (exprNode e, bool definatelv, bool definaterv, filel e->ensuresConstraints = constraintList_addGeneratingExpr ( e->ensuresConstraints, e); - DPRINTF((message ("ensures constraint 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) ) )); - return handledExprNode; + 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) ) )); + + return; // handledExprNode; } @@ -1125,7 +1320,7 @@ constraintList exprNode_traversTrueEnsuresConstraints (exprNode e) if (exprNode_handleError (e)) { - ret = constraintList_new(); + ret = constraintList_makeNew(); return ret; } ret = constraintList_copy (e->trueEnsuresConstraints ); @@ -1138,45 +1333,45 @@ constraintList exprNode_traversTrueEnsuresConstraints (exprNode e) { case XPR_WHILEPRED: t1 = exprData_getSingle (data); - ret = constraintList_addList ( ret,exprNode_traversTrueEnsuresConstraints (t1) ); + ret = constraintList_addListFree ( ret, exprNode_traversTrueEnsuresConstraints (t1) ); break; case XPR_FETCH: - ret = constraintList_addList (ret, + ret = constraintList_addListFree (ret, exprNode_traversTrueEnsuresConstraints (exprData_getPairA (data) ) ); - ret = constraintList_addList (ret, + ret = constraintList_addListFree (ret, exprNode_traversTrueEnsuresConstraints (exprData_getPairB (data) ) ); break; case XPR_PREOP: - ret = constraintList_addList (ret, + ret = constraintList_addListFree (ret, exprNode_traversTrueEnsuresConstraints (exprData_getUopNode (data) ) ); break; case XPR_PARENS: - ret = constraintList_addList (ret, exprNode_traversTrueEnsuresConstraints + ret = constraintList_addListFree (ret, exprNode_traversTrueEnsuresConstraints (exprData_getUopNode (data) ) ); break; case XPR_ASSIGN: - ret = constraintList_addList (ret, + ret = constraintList_addListFree (ret, exprNode_traversTrueEnsuresConstraints (exprData_getOpA (data) ) ); - ret = constraintList_addList (ret, + ret = constraintList_addListFree (ret, exprNode_traversTrueEnsuresConstraints (exprData_getOpB (data) ) ); break; case XPR_OP: - ret = constraintList_addList (ret, + ret = constraintList_addListFree (ret, exprNode_traversTrueEnsuresConstraints (exprData_getOpA (data) ) ); - ret = constraintList_addList (ret, + ret = constraintList_addListFree (ret, exprNode_traversTrueEnsuresConstraints (exprData_getOpB (data) ) ); break; @@ -1188,20 +1383,20 @@ constraintList exprNode_traversTrueEnsuresConstraints (exprNode e) case XPR_SIZEOF: - ret = constraintList_addList (ret, - exprNode_traversTrueEnsuresConstraints - (exprData_getSingle (data) ) ); + ret = constraintList_addListFree (ret, + exprNode_traversTrueEnsuresConstraints + (exprData_getSingle (data) ) ); break; case XPR_CALL: - ret = constraintList_addList (ret, + ret = constraintList_addListFree (ret, exprNode_traversTrueEnsuresConstraints (exprData_getFcn (data) ) ); /*@i11*/ // exprNodeList_unparse (exprData_getArgs (data) ); break; case XPR_RETURN: - ret = constraintList_addList (ret, + ret = constraintList_addListFree (ret, exprNode_traversTrueEnsuresConstraints (exprData_getSingle (data) ) ); break; @@ -1211,14 +1406,14 @@ constraintList exprNode_traversTrueEnsuresConstraints (exprNode e) break; case XPR_FACCESS: - ret = constraintList_addList (ret, + ret = constraintList_addListFree (ret, exprNode_traversTrueEnsuresConstraints (exprData_getFieldNode (data) ) ); //exprData_getFieldName (data) ; break; case XPR_ARROW: - ret = constraintList_addList (ret, + ret = constraintList_addListFree (ret, exprNode_traversTrueEnsuresConstraints (exprData_getFieldNode (data) ) ); // exprData_getFieldName (data); @@ -1233,19 +1428,18 @@ constraintList exprNode_traversTrueEnsuresConstraints (exprNode e) break; case XPR_POSTOP: - ret = constraintList_addList (ret, + ret = constraintList_addListFree (ret, exprNode_traversTrueEnsuresConstraints (exprData_getUopNode (data) ) ); break; case XPR_CAST: - ret = constraintList_addList (ret, + ret = constraintList_addListFree (ret, exprNode_traversTrueEnsuresConstraints (exprData_getCastNode (data) ) ); - break; - break; + default: break; } @@ -1264,7 +1458,7 @@ constraintList exprNode_traversFalseEnsuresConstraints (exprNode e) if (exprNode_handleError (e)) { - ret = constraintList_new(); + ret = constraintList_makeNew(); return ret; } ret = constraintList_copy (e->falseEnsuresConstraints ); @@ -1277,45 +1471,45 @@ constraintList exprNode_traversFalseEnsuresConstraints (exprNode e) { case XPR_WHILEPRED: t1 = exprData_getSingle (data); - ret = constraintList_addList ( ret,exprNode_traversFalseEnsuresConstraints (t1) ); + ret = constraintList_addListFree ( ret,exprNode_traversFalseEnsuresConstraints (t1) ); break; case XPR_FETCH: - ret = constraintList_addList (ret, + ret = constraintList_addListFree (ret, exprNode_traversFalseEnsuresConstraints (exprData_getPairA (data) ) ); - ret = constraintList_addList (ret, + ret = constraintList_addListFree (ret, exprNode_traversFalseEnsuresConstraints (exprData_getPairB (data) ) ); break; case XPR_PREOP: - ret = constraintList_addList (ret, + ret = constraintList_addListFree (ret, exprNode_traversFalseEnsuresConstraints (exprData_getUopNode (data) ) ); break; case XPR_PARENS: - ret = constraintList_addList (ret, exprNode_traversFalseEnsuresConstraints + ret = constraintList_addListFree (ret, exprNode_traversFalseEnsuresConstraints (exprData_getUopNode (data) ) ); break; case XPR_ASSIGN: - ret = constraintList_addList (ret, + ret = constraintList_addListFree (ret, exprNode_traversFalseEnsuresConstraints (exprData_getOpA (data) ) ); - ret = constraintList_addList (ret, + ret = constraintList_addListFree (ret, exprNode_traversFalseEnsuresConstraints (exprData_getOpB (data) ) ); break; case XPR_OP: - ret = constraintList_addList (ret, + ret = constraintList_addListFree (ret, exprNode_traversFalseEnsuresConstraints (exprData_getOpA (data) ) ); - ret = constraintList_addList (ret, + ret = constraintList_addListFree (ret, exprNode_traversFalseEnsuresConstraints (exprData_getOpB (data) ) ); break; @@ -1327,20 +1521,20 @@ constraintList exprNode_traversFalseEnsuresConstraints (exprNode e) case XPR_SIZEOF: - ret = constraintList_addList (ret, + ret = constraintList_addListFree (ret, exprNode_traversFalseEnsuresConstraints (exprData_getSingle (data) ) ); break; case XPR_CALL: - ret = constraintList_addList (ret, + ret = constraintList_addListFree (ret, exprNode_traversFalseEnsuresConstraints (exprData_getFcn (data) ) ); /*@i11*/ // exprNodeList_unparse (exprData_getArgs (data) ); break; case XPR_RETURN: - ret = constraintList_addList (ret, + ret = constraintList_addListFree (ret, exprNode_traversFalseEnsuresConstraints (exprData_getSingle (data) ) ); break; @@ -1350,14 +1544,14 @@ constraintList exprNode_traversFalseEnsuresConstraints (exprNode e) break; case XPR_FACCESS: - ret = constraintList_addList (ret, + ret = constraintList_addListFree (ret, exprNode_traversFalseEnsuresConstraints (exprData_getFieldNode (data) ) ); //exprData_getFieldName (data) ; break; case XPR_ARROW: - ret = constraintList_addList (ret, + ret = constraintList_addListFree (ret, exprNode_traversFalseEnsuresConstraints (exprData_getFieldNode (data) ) ); // exprData_getFieldName (data); @@ -1372,14 +1566,14 @@ constraintList exprNode_traversFalseEnsuresConstraints (exprNode e) break; case XPR_POSTOP: - ret = constraintList_addList (ret, + ret = constraintList_addListFree (ret, exprNode_traversFalseEnsuresConstraints (exprData_getUopNode (data) ) ); break; case XPR_CAST: - ret = constraintList_addList (ret, + ret = constraintList_addListFree (ret, exprNode_traversFalseEnsuresConstraints (exprData_getCastNode (data) ) ); break; @@ -1393,7 +1587,7 @@ constraintList exprNode_traversFalseEnsuresConstraints (exprNode e) /* walk down the tree and get all requires Constraints in each subexpression*/ -constraintList exprNode_traversRequiresConstraints (exprNode e) +/*@only@*/ constraintList exprNode_traversRequiresConstraints (exprNode e) { exprNode t1; @@ -1404,7 +1598,7 @@ constraintList exprNode_traversRequiresConstraints (exprNode e) if (exprNode_handleError (e)) { - ret = constraintList_new(); + ret = constraintList_makeNew(); return ret; } ret = constraintList_copy (e->requiresConstraints ); @@ -1417,45 +1611,45 @@ constraintList exprNode_traversRequiresConstraints (exprNode e) { case XPR_WHILEPRED: t1 = exprData_getSingle (data); - ret = constraintList_addList ( ret,exprNode_traversRequiresConstraints (t1) ); + ret = constraintList_addListFree ( ret, exprNode_traversRequiresConstraints (t1) ); break; case XPR_FETCH: - ret = constraintList_addList (ret, + ret = constraintList_addListFree (ret, exprNode_traversRequiresConstraints (exprData_getPairA (data) ) ); - ret = constraintList_addList (ret, + ret = constraintList_addListFree (ret, exprNode_traversRequiresConstraints (exprData_getPairB (data) ) ); break; case XPR_PREOP: - ret = constraintList_addList (ret, + ret = constraintList_addListFree (ret, exprNode_traversRequiresConstraints (exprData_getUopNode (data) ) ); break; case XPR_PARENS: - ret = constraintList_addList (ret, exprNode_traversRequiresConstraints + ret = constraintList_addListFree (ret, exprNode_traversRequiresConstraints (exprData_getUopNode (data) ) ); break; case XPR_ASSIGN: - ret = constraintList_addList (ret, + ret = constraintList_addListFree (ret, exprNode_traversRequiresConstraints (exprData_getOpA (data) ) ); - ret = constraintList_addList (ret, + ret = constraintList_addListFree (ret, exprNode_traversRequiresConstraints (exprData_getOpB (data) ) ); break; case XPR_OP: - ret = constraintList_addList (ret, + ret = constraintList_addListFree (ret, exprNode_traversRequiresConstraints (exprData_getOpA (data) ) ); - ret = constraintList_addList (ret, + ret = constraintList_addListFree (ret, exprNode_traversRequiresConstraints (exprData_getOpB (data) ) ); break; @@ -1467,20 +1661,20 @@ constraintList exprNode_traversRequiresConstraints (exprNode e) case XPR_SIZEOF: - ret = constraintList_addList (ret, + ret = constraintList_addListFree (ret, exprNode_traversRequiresConstraints (exprData_getSingle (data) ) ); break; case XPR_CALL: - ret = constraintList_addList (ret, + ret = constraintList_addListFree (ret, exprNode_traversRequiresConstraints (exprData_getFcn (data) ) ); /*@i11*/ // exprNodeList_unparse (exprData_getArgs (data) ); break; case XPR_RETURN: - ret = constraintList_addList (ret, + ret = constraintList_addListFree (ret, exprNode_traversRequiresConstraints (exprData_getSingle (data) ) ); break; @@ -1490,14 +1684,14 @@ constraintList exprNode_traversRequiresConstraints (exprNode e) break; case XPR_FACCESS: - ret = constraintList_addList (ret, + ret = constraintList_addListFree (ret, exprNode_traversRequiresConstraints (exprData_getFieldNode (data) ) ); //exprData_getFieldName (data) ; break; case XPR_ARROW: - ret = constraintList_addList (ret, + ret = constraintList_addListFree (ret, exprNode_traversRequiresConstraints (exprData_getFieldNode (data) ) ); // exprData_getFieldName (data); @@ -1512,14 +1706,14 @@ constraintList exprNode_traversRequiresConstraints (exprNode e) break; case XPR_POSTOP: - ret = constraintList_addList (ret, + ret = constraintList_addListFree (ret, exprNode_traversRequiresConstraints (exprData_getUopNode (data) ) ); break; case XPR_CAST: - ret = constraintList_addList (ret, + ret = constraintList_addListFree (ret, exprNode_traversRequiresConstraints (exprData_getCastNode (data) ) ); break; @@ -1533,7 +1727,7 @@ constraintList exprNode_traversRequiresConstraints (exprNode e) /* walk down the tree and get all Ensures Constraints in each subexpression*/ -constraintList exprNode_traversEnsuresConstraints (exprNode e) +/*@only@*/ constraintList exprNode_traversEnsuresConstraints (exprNode e) { exprNode t1; @@ -1547,7 +1741,7 @@ constraintList exprNode_traversEnsuresConstraints (exprNode e) if (exprNode_handleError (e)) { - ret = constraintList_new(); + ret = constraintList_makeNew(); return ret; } @@ -1568,45 +1762,45 @@ constraintList exprNode_traversEnsuresConstraints (exprNode e) { case XPR_WHILEPRED: t1 = exprData_getSingle (data); - ret = constraintList_addList ( ret,exprNode_traversEnsuresConstraints (t1) ); + ret = constraintList_addListFree ( ret,exprNode_traversEnsuresConstraints (t1) ); break; case XPR_FETCH: - ret = constraintList_addList (ret, + ret = constraintList_addListFree (ret, exprNode_traversEnsuresConstraints (exprData_getPairA (data) ) ); - ret = constraintList_addList (ret, + ret = constraintList_addListFree (ret, exprNode_traversEnsuresConstraints (exprData_getPairB (data) ) ); break; case XPR_PREOP: - ret = constraintList_addList (ret, + ret = constraintList_addListFree (ret, exprNode_traversEnsuresConstraints (exprData_getUopNode (data) ) ); break; case XPR_PARENS: - ret = constraintList_addList (ret, exprNode_traversEnsuresConstraints + ret = constraintList_addListFree (ret, exprNode_traversEnsuresConstraints (exprData_getUopNode (data) ) ); break; case XPR_ASSIGN: - ret = constraintList_addList (ret, + ret = constraintList_addListFree (ret, exprNode_traversEnsuresConstraints (exprData_getOpA (data) ) ); - ret = constraintList_addList (ret, + ret = constraintList_addListFree (ret, exprNode_traversEnsuresConstraints (exprData_getOpB (data) ) ); break; case XPR_OP: - ret = constraintList_addList (ret, + ret = constraintList_addListFree (ret, exprNode_traversEnsuresConstraints (exprData_getOpA (data) ) ); - ret = constraintList_addList (ret, + ret = constraintList_addListFree (ret, exprNode_traversEnsuresConstraints (exprData_getOpB (data) ) ); break; @@ -1618,20 +1812,20 @@ constraintList exprNode_traversEnsuresConstraints (exprNode e) case XPR_SIZEOF: - ret = constraintList_addList (ret, + ret = constraintList_addListFree (ret, exprNode_traversEnsuresConstraints (exprData_getSingle (data) ) ); break; case XPR_CALL: - ret = constraintList_addList (ret, + ret = constraintList_addListFree (ret, exprNode_traversEnsuresConstraints (exprData_getFcn (data) ) ); /*@i11*/ // exprNodeList_unparse (exprData_getArgs (data) ); break; case XPR_RETURN: - ret = constraintList_addList (ret, + ret = constraintList_addListFree (ret, exprNode_traversEnsuresConstraints (exprData_getSingle (data) ) ); break; @@ -1641,14 +1835,14 @@ constraintList exprNode_traversEnsuresConstraints (exprNode e) break; case XPR_FACCESS: - ret = constraintList_addList (ret, + ret = constraintList_addListFree (ret, exprNode_traversEnsuresConstraints (exprData_getFieldNode (data) ) ); //exprData_getFieldName (data) ; break; case XPR_ARROW: - ret = constraintList_addList (ret, + ret = constraintList_addListFree (ret, exprNode_traversEnsuresConstraints (exprData_getFieldNode (data) ) ); // exprData_getFieldName (data); @@ -1663,13 +1857,13 @@ constraintList exprNode_traversEnsuresConstraints (exprNode e) break; case XPR_POSTOP: - ret = constraintList_addList (ret, + ret = constraintList_addListFree (ret, exprNode_traversEnsuresConstraints (exprData_getUopNode (data) ) ); break; case XPR_CAST: - ret = constraintList_addList (ret, + ret = constraintList_addListFree (ret, exprNode_traversEnsuresConstraints (exprData_getCastNode (data) ) ); break;