X-Git-Url: http://andersk.mit.edu/gitweb/splint.git/blobdiff_plain/38496f1137eec2c51c72e9853f4ef8eb0a33a1d3..119f0b939487be7edf6e68d5696eee3e605340a5:/src/constraintGeneration.c diff --git a/src/constraintGeneration.c b/src/constraintGeneration.c index 942abcc..251ce53 100644 --- a/src/constraintGeneration.c +++ b/src/constraintGeneration.c @@ -1,39 +1,55 @@ /* -** constraintList.c +** constraintGeneration.c */ +//#define DEBUGPRINT 1 + # include /* for isdigit */ # include "lclintMacros.nf" # include "basic.h" -# include "cgrammar.h" + # include "cgrammar_tokens.h" # include "exprChecks.h" -# include "aliasChecks.h" # include "exprNodeSList.h" -# include "exprData.i" -void /*@alt bool@*/ exprNode_generateConstraints (/*@temp@*/ exprNode e); -static bool exprNode_handleError( exprNode p_e); +//# include "exprDataQuite.i" + +/*@access exprNode @*/ + + +static bool exprNode_handleError(/*@dependent@*/ 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 bool exprNode_isMultiStatement(/*@dependent@*/ exprNode p_e); +static void exprNode_multiStatement (/*@dependent@*/ 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); +static constraintList exprNode_traversTrueEnsuresConstraints (/*@dependent@*/ exprNode p_e); +static constraintList exprNode_traversFalseEnsuresConstraints (/*@dependent@*/ exprNode p_e); -extern constraintList reflectChanges (constraintList pre2, constraintList post1); +static exprNode makeDataTypeConstraints (/*@returned@*/ exprNode p_e); -void mergeResolve (exprNode parent, exprNode child1, exprNode child2); +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); - -bool exprNode_isUnhandled (exprNode e) +//constraintList constraintList_makeFixedArrayConstraints (sRefSet s); + +//bool exprNode_testd() +//{ + /* if ( ( (exprNode_isError ) ) ) + { + } + if ( ( (e_1 ) ) ) + { + } + */ +//} + +static bool exprNode_isUnhandled (/*@dependent@*/ /*@obsever@*/ exprNode e) { llassert( exprNode_isDefined(e) ); switch (e->kind) @@ -50,7 +66,6 @@ bool exprNode_isUnhandled (exprNode e) case XPR_VAARG: case XPR_ITERCALL: case XPR_ITER: - case XPR_CAST: case XPR_GOTO: case XPR_CONTINUE: case XPR_BREAK: @@ -59,12 +74,12 @@ bool exprNode_isUnhandled (exprNode e) case XPR_TOK: case XPR_FTDEFAULT: case XPR_DEFAULT: - case XPR_SWITCH: + // case XPR_SWITCH: case XPR_FTCASE: case XPR_CASE: - case XPR_INIT: + // case XPR_INIT: case XPR_NODE: - TPRINTF((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,25 +107,21 @@ bool exprNode_handleError( exprNode e) return FALSE; } -void /*@alt bool@*/ exprNode_generateConstraints (/*@temp@*/ exprNode e) +bool /*@alt void@*/ exprNode_generateConstraints (/*@dependent@*/ exprNode e) { if (exprNode_isError (e) ) return FALSE; - + if (exprNode_isUnhandled (e) ) { - TPRINTF( (message("Warning ignoring %s", exprNode_unparse (e) ) ) ); - e->requiresConstraints = constraintList_new(); - e->ensuresConstraints = constraintList_new(); - e->trueEnsuresConstraints = constraintList_new(); - e->falseEnsuresConstraints = constraintList_new(); - llassert(FALSE); - return FALSE; + DPRINTF( (message("Warning ignoring %s", exprNode_unparse (e) ) ) ); + return FALSE; } - - TPRINTF((message ("exprNode_generateConstraints Analysising %s at %s", exprNode_unparse( e), + // e = makeDataTypeConstraints (e); + + DPRINTF((message ("exprNode_generateConstraints Analysising %s at %s", exprNode_unparse( e), fileloc_unparse(exprNode_getfileloc(e) ) ) ) ); if (exprNode_isMultiStatement ( e) ) @@ -119,11 +130,27 @@ void /*@alt bool@*/ exprNode_generateConstraints (/*@temp@*/ exprNode e) } else { - // llassert(FALSE); + fileloc loc; + + loc = exprNode_getNextSequencePoint(e); + exprNode_exprTraverse(e, FALSE, FALSE, loc); + + fileloc_free(loc); return FALSE; } - printf ("%s", (message ("%s", constraintList_printDetailed (e->requiresConstraints) ) ) ); - printf ("%s", (message ("%s", constraintList_printDetailed (e->ensuresConstraints) ) ) ); + + { + constraintList c; + + c = constraintList_makeFixedArrayConstraints (e->uses); + e->requiresConstraints = constraintList_reflectChangesFreePre (e->requiresConstraints, c); + + // e->ensuresConstraints = constraintList_mergeEnsures(c, e->ensuresConstraints); + + constraintList_free(c); + } + + DPRINTF ( (message ("e->requiresConstraints %s", constraintList_printDetailed (e->requiresConstraints) ) ) ); return FALSE; } @@ -147,6 +174,7 @@ if (exprNode_handleError (e) != NULL) case XPR_BLOCK: case XPR_STMT: case XPR_STMTLIST: + case XPR_SWITCH: return TRUE; default: return FALSE; @@ -154,37 +182,60 @@ if (exprNode_handleError (e) != NULL) } -bool exprNode_stmt (exprNode e) +static void exprNode_stmt ( /*@dependent@*/ exprNode e) { exprNode snode; fileloc loc; - bool notError; - + 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); DPRINTF(( "STMT:") ); - DPRINTF ( ( cstring_toCharsSafe ( exprNode_unparse(e)) ) - ); + s = exprNode_unparse(e); + // DPRINTF ( ( message("STMT: %s ") ) ); + + if (e->kind == XPR_INIT) + { + constraintList tempList; + 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); + + tempList = e->requiresConstraints; + e->requiresConstraints = exprNode_traversRequiresConstraints(e); + constraintList_free(tempList); + + tempList = e->ensuresConstraints; + e->ensuresConstraints = exprNode_traversEnsuresConstraints(e); + constraintList_free(tempList); + return; // notError; + } + if (e->kind != XPR_STMT) { - TPRINTF (("Not Stmt") ); - TPRINTF ( (message ("%s ", exprNode_unparse (e)) ) ); + DPRINTF (("Not Stmt") ); + DPRINTF ( (message ("%s ", exprNode_unparse (e)) ) ); if (exprNode_isMultiStatement (e) ) { return exprNode_multiStatement (e ); } - // llassert(FALSE); + DPRINTF( (message ("Ignoring non-statement %s", exprNode_unparse(e) ) ) ); + return; //TRUE; + // llassert(FALSE); } - TPRINTF (("Stmt") ); - TPRINTF ( (message ("%s ", exprNode_unparse (e)) ) ); + DPRINTF (("Stmt") ); + DPRINTF ( (message ("%s ", exprNode_unparse (e)) ) ); snode = exprData_getUopNode (e->edata); @@ -194,43 +245,60 @@ bool exprNode_stmt (exprNode e) if (exprNode_isMultiStatement (snode)) { - // llassert(FALSE); - return exprNode_multiStatement (snode); + 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) ); + // 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) ); + // 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 (/*@dependent@*/ 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); - TPRINTF(( "STMTLIST:") ); - TPRINTF ((cstring_toCharsSafe (exprNode_unparse(e)) ) ); + DPRINTF(( "STMTLIST:") ); + DPRINTF ((cstring_toCharsSafe (exprNode_unparse(e)) ) ); stmt1 = exprData_getPairA (e->edata); stmt2 = exprData_getPairB (e->edata); @@ -242,27 +310,285 @@ bool exprNode_stmtList (exprNode e) DPRINTF(("\nstmt after stmtList call " )); exprNode_stmt (stmt2); - mergeResolve (e, stmt1, stmt2 ); + exprNode_mergeResolve (e, stmt1, stmt2 ); 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, /*@dependent@*/ exprNode test, /*@dependent@*/ exprNode body) { - test->trueEnsuresConstraints = exprNode_traversTrueEnsuresConstraints(test); - e->requiresConstraints = reflectChanges (body->requiresConstraints, test->trueEnsuresConstraints); - e->requiresConstraints = reflectChanges (e->requiresConstraints, + constraintList temp; + + DPRINTF ((message ("doIf: %s ", exprNode_unparse(e) ) ) ); + + 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); + 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 = constraintList_reflectChanges(body->requiresConstraints, test->trueEnsuresConstraints); + + e->requiresConstraints = constraintList_reflectChangesFreePre (e->requiresConstraints, test->ensuresConstraints); -#warning bad + temp = e->requiresConstraints; + e->requiresConstraints = constraintList_mergeRequires (e->requiresConstraints, test->requiresConstraints); + constraintList_free(temp); + + +//drl possible problem : warning bad + constraintList_free(e->ensuresConstraints); e->ensuresConstraints = constraintList_copy (test->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; +} + +/*drl added 3/4/2001 + Also used for condition i.e. ?: operation + + Precondition + This function assumes that p, trueBranch, falseBranch have have all been traversed + for constraints i.e. we assume that exprNode_traversEnsuresConstraints, + exprNode_traversRequiresConstraints, exprNode_traversTrueEnsuresConstraints, + 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) ) ) ); + + // do requires clauses + c1 = constraintList_copy (p->ensuresConstraints); + + t = constraintList_reflectChanges(trueBranch->requiresConstraints, p->trueEnsuresConstraints); + t = constraintList_reflectChangesFreePre (t, p->ensuresConstraints); + + cons = constraintList_reflectChanges(falseBranch->requiresConstraints, p->falseEnsuresConstraints); + cons = constraintList_reflectChangesFreePre (cons, c1); + + 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; +} + +static exprNode doWhile (/*@returned@*/ exprNode e, /*@dependent@*/ exprNode test, /*@dependent@*/ exprNode body) +{ + DPRINTF ((message ("doWhile: %s ", exprNode_unparse(e) ) ) ); + return doIf (e, test, body); +} + +/*@only@*/ constraintList constraintList_makeFixedArrayConstraints (/*@observer@*/ sRefSet s) +{ + constraintList ret; + constraint con; + ret = constraintList_makeNew(); + + sRefSet_elements (s, el) + { + // llassert (el); + if (sRef_isFixedArray(el) ) + { + 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 + size = sRef_getArraySize(el); + DPRINTF( (message("%s is a fixed array with size %d", + sRef_unparse(el), (int)size) ) ); + con = constraint_makeSRefSetBufferSize (el, (size - 1)); + //con = constraint_makeSRefWriteSafeInt (el, (size - 1)); + ret = constraintList_add(ret, con); + } + else + { + DPRINTF( (message("%s is not a fixed array", + sRef_unparse(el)) ) ); + + + if (sRef_isExternallyVisible (el) ) + { + /*DPRINTF( (message("%s is externally visible", + sRef_unparse(el) ) )); + con = constraint_makeSRefWriteSafeInt(el, 0); + ret = constraintList_add(ret, con); + + con = constraint_makeSRefReadSafeInt(el, 0); + + ret = constraintList_add(ret, con);*/ + } + } + } + end_sRefSet_elements + + DPRINTF(( message("constraintList_makeFixedArrayConstraints returning %s", + constraintList_print(ret) ) )); + return ret; +} + +exprNode makeDataTypeConstraints (/*@returned@*/ exprNode e) +{ + constraintList c; + DPRINTF(("makeDataTypeConstraints")); + + c = constraintList_makeFixedArrayConstraints (e->uses); + + e->ensuresConstraints = constraintList_addListFree (e->ensuresConstraints, c); + + return e; +} + +static void doFor (/*@dependent@*/ exprNode e, /*@dependent@*/ exprNode forPred, /*@dependent@*/ exprNode forBody) +{ + 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); + + if ( ( (exprNode_isError (test) /*|| (exprNode_isError(init) )*/ ) || (exprNode_isError (inc) ) ) ) + { + DPRINTF ((message ("strange for statement:%s, ignoring it", exprNode_unparse(e) ) ) ); + return; + } + + exprNode_forLoopHeuristics(e, forPred, forBody); + + constraintList_free(e->requiresConstraints); + e->requiresConstraints = constraintList_reflectChanges(forBody->requiresConstraints, test->ensuresConstraints); + e->requiresConstraints = constraintList_reflectChangesFreePre (e->requiresConstraints, test->trueEnsuresConstraints); + e->requiresConstraints = constraintList_reflectChangesFreePre (e->requiresConstraints, forPred->ensuresConstraints); + + if (!forBody->canBreak) + { + 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 + { + DPRINTF(("Can break") ); + } + +} + +static exprNode doSwitch (/*@returned@*/ exprNode e) +{ + exprNode body; + exprData data; + + data = e->edata; + // llassert(FALSE); + DPRINTF (( message ("doSwitch for: switch (%s) %s", + exprNode_unparse (exprData_getPairA (data)), + exprNode_unparse (exprData_getPairB (data))) )); + + body = exprData_getPairB (data); + + exprNode_generateConstraints(body); + + constraintList_free(e->requiresConstraints); + constraintList_free(e->ensuresConstraints); + + e->requiresConstraints = NULL; + e->ensuresConstraints = NULL; + + e->requiresConstraints = constraintList_copy ( body->requiresConstraints ); + e->ensuresConstraints = constraintList_copy ( body->ensuresConstraints ); + return e; } -bool exprNode_multiStatement (exprNode e) + +void exprNode_multiStatement (/*@dependent@*/ exprNode e) { bool ret; @@ -270,21 +596,24 @@ bool exprNode_multiStatement (exprNode e) exprNode e1, e2; exprNode p, trueBranch, falseBranch; exprNode forPred, forBody; - exprNode init, test, inc; - constraintList cons; - constraintList t, f; - e->requiresConstraints = constraintList_new(); - e->ensuresConstraints = constraintList_new(); - e->trueEnsuresConstraints = constraintList_new(); - e->falseEnsuresConstraints = constraintList_new(); - + exprNode test; + + 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), fileloc_unparse(exprNode_getfileloc(e) ) ) ) ); if (exprNode_handleError (e)) { - return FALSE; + return; // FALSE; } data = e->edata; @@ -299,35 +628,49 @@ bool exprNode_multiStatement (exprNode e) forPred = exprData_getPairA (data); forBody = exprData_getPairB (data); - //first generate the constraints exprNode_generateConstraints (forPred); exprNode_generateConstraints (forBody); - - //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); - test->trueEnsuresConstraints = exprNode_traversTrueEnsuresConstraints(test); - // e->requiresConstraints = reflectChanges (body->requiresConstraints, test->trueEnsuresConstraints); - e->requiresConstraints = reflectChanges (e->requiresConstraints, test->ensuresConstraints); - + + doFor (e, forPred, forBody); + break; case XPR_FORPRED: // ret = message ("for (%s; %s; %s)", exprNode_generateConstraints (exprData_getTripleInit (data) ); - exprNode_exprTraverse (exprData_getTripleTest (data),FALSE, FALSE, exprNode_loc(e)); + test = exprData_getTripleTest (data); + exprNode_exprTraverse (test,FALSE, FALSE, exprNode_loc(e)); + exprNode_generateConstraints (exprData_getTripleInc (data) ); + + if (!exprNode_isError(test) ) + { + constraintList temp2; + temp2 = test->trueEnsuresConstraints; + test->trueEnsuresConstraints = exprNode_traversTrueEnsuresConstraints(test); + constraintList_free(temp2); + } + exprNode_generateConstraints (exprData_getTripleInc (data)); break; + + case XPR_WHILE: + e1 = exprData_getPairA (data); + e2 = exprData_getPairB (data); + + exprNode_exprTraverse (e1, + FALSE, FALSE, exprNode_loc(e1)); + + exprNode_generateConstraints (e2); + + e = doWhile (e, e1, e2); + + break; + case XPR_IF: - TPRINTF(( "IF:") ); - TPRINTF ((exprNode_unparse(e) ) ); + DPRINTF(( "IF:") ); + DPRINTF ((exprNode_unparse(e) ) ); // ret = message ("if (%s) %s", e1 = exprData_getPairA (data); e2 = exprData_getPairB (data); @@ -336,15 +679,15 @@ bool exprNode_multiStatement (exprNode e) FALSE, FALSE, exprNode_loc(e1)); exprNode_generateConstraints (e2); - e = doIf (e, e1, e2); // e->constraints = constraintList_exprNodemerge (exprData_getPairA (data),exprData_getPairB(data)); break; - + + case XPR_IFELSE: - TPRINTF(("Starting IFELSE")); + DPRINTF(("Starting IFELSE")); // ret = message ("if (%s) %s else %s", p = exprData_getTriplePred (data); trueBranch = exprData_getTripleTrue (data); @@ -355,304 +698,798 @@ bool exprNode_multiStatement (exprNode e) exprNode_generateConstraints (trueBranch); exprNode_generateConstraints (falseBranch); - // do requires clauses - - cons = reflectChanges (trueBranch->requiresConstraints, p->trueEnsuresConstraints); - cons = reflectChanges (cons, - p->ensuresConstraints); - e->requiresConstraints = constraintList_copy (cons); + temp = p->ensuresConstraints; + p->ensuresConstraints = exprNode_traversEnsuresConstraints (p); + constraintList_free(temp); - cons = reflectChanges (falseBranch->requiresConstraints, p->falseEnsuresConstraints); - cons = reflectChanges (cons, - p->ensuresConstraints); - e->requiresConstraints = constraintList_addList (e->requiresConstraints, - cons); - e->requiresConstraints = constraintList_addList (e->requiresConstraints, - p->requiresConstraints); - - // do ensures clauses - // find the the ensures lists for each subbranch - t = constraintList_mergeEnsures (p->trueEnsuresConstraints, trueBranch->ensuresConstraints); - t = constraintList_mergeEnsures (p->ensuresConstraints, t); + temp = p->requiresConstraints; + p->requiresConstraints = exprNode_traversRequiresConstraints (p); + constraintList_free(temp); - f = constraintList_mergeEnsures (p->falseEnsuresConstraints, falseBranch->ensuresConstraints); - f = constraintList_mergeEnsures (p->ensuresConstraints, f); + temp = p->trueEnsuresConstraints; + p->trueEnsuresConstraints = exprNode_traversTrueEnsuresConstraints(p); + constraintList_free(temp); - // find ensures for whole if/else statement - - e->ensuresConstraints = constraintList_logicalOr (t, f); - TPRINTF( ("Done IFELSE") ); + temp = p->falseEnsuresConstraints; + p->falseEnsuresConstraints = exprNode_traversFalseEnsuresConstraints(p); + constraintList_free(temp); + + e = doIfElse (e, p, trueBranch, falseBranch); + DPRINTF( ("Done IFELSE") ); break; - case XPR_WHILE: - e1 = exprData_getPairA (data); - e2 = exprData_getPairB (data); - exprNode_exprTraverse (e1, - FALSE, FALSE, exprNode_loc(e1)); + + case XPR_DOWHILE: + + e2 = (exprData_getPairB (data)); + e1 = (exprData_getPairA (data)); + 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) ) )); - e1->trueEnsuresConstraints = exprNode_traversTrueEnsuresConstraints(e1); - - e->requiresConstraints = reflectChanges (e2->requiresConstraints, e1->trueEnsuresConstraints); - - e->requiresConstraints = reflectChanges (e->requiresConstraints, - e1->ensuresConstraints); -#warning bad - e->ensuresConstraints = constraintList_copy (e1->ensuresConstraints); - - // ret = message ("while (%s) %s", - exprNode_generateConstraints (exprData_getPairA (data)); - exprNode_generateConstraints (exprData_getPairB (data)); - // e->constraints = constraintList_exprNodemerge (exprData_getPairA (data), exprData_getPairB (data) ); - break; - - case XPR_DOWHILE: - // ret = message ("do { %s } while (%s)", - exprNode_generateConstraints (exprData_getPairB (data)); - exprNode_generateConstraints (exprData_getPairA (data)); break; 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; + case XPR_SWITCH: + e = doSwitch (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; +} + +static bool lltok_isBoolean_Op (lltok tok) +{ + /*this should really be a switch statement but + I don't want to violate the abstraction + maybe this should go in lltok.c */ + + if (lltok_isEq_Op (tok) ) + { + return TRUE; + } + if (lltok_isAnd_Op (tok) ) + + { + + return TRUE; + } + if (lltok_isOr_Op (tok) ) + { + return TRUE; + } + + if (lltok_isGt_Op (tok) ) + { + return TRUE; + } + if (lltok_isLt_Op (tok) ) + { + return TRUE; + } + + if (lltok_isLe_Op (tok) ) + { + return TRUE; + } + + if (lltok_isGe_Op (tok) ) + { + return TRUE; + } + + return FALSE; + +} + + +static void exprNode_booleanTraverse (/*@dependent@*/ exprNode e, /*@unused@*/ bool definatelv, /*@unused@*/ bool definaterv, fileloc sequencePoint) +{ + constraint cons; +exprNode t1, t2; +exprData data; +lltok tok; +constraintList tempList, temp; +data = e->edata; + +tok = exprData_getOpTok (data); + + +t1 = exprData_getOpA (data); +t2 = exprData_getOpB (data); + + + tempList = constraintList_undefined; + +/* arithmetic tests */ + +if (lltok_isEq_Op (tok) ) +{ + cons = constraint_makeEnsureEqual (t1, t2, sequencePoint); + e->trueEnsuresConstraints = constraintList_add(e->trueEnsuresConstraints, cons); +} + + + if (lltok_isLt_Op (tok) ) + { + cons = constraint_makeEnsureLessThan (t1, t2, sequencePoint); + e->trueEnsuresConstraints = constraintList_add(e->trueEnsuresConstraints, cons); + cons = constraint_makeEnsureGreaterThanEqual (t1, t2, sequencePoint); + e->falseEnsuresConstraints = constraintList_add(e->falseEnsuresConstraints, cons); + } + + +if (lltok_isGe_Op (tok) ) +{ + + cons = constraint_makeEnsureGreaterThanEqual (t1, t2, sequencePoint); + e->trueEnsuresConstraints = constraintList_add(e->trueEnsuresConstraints, cons); + + cons = constraint_makeEnsureLessThan (t1, t2, sequencePoint); + e->falseEnsuresConstraints = constraintList_add(e->falseEnsuresConstraints, cons); + +} + + + if (lltok_isGt_Op (tok) ) +{ + cons = constraint_makeEnsureGreaterThan (t1, t2, sequencePoint); + e->trueEnsuresConstraints = constraintList_add(e->trueEnsuresConstraints, cons); + cons = constraint_makeEnsureLessThanEqual (t1, t2, sequencePoint); + e->falseEnsuresConstraints = constraintList_add(e->falseEnsuresConstraints, cons); +} + +if (lltok_isLe_Op (tok) ) +{ + cons = constraint_makeEnsureLessThanEqual (t1, t2, sequencePoint); + e->trueEnsuresConstraints = constraintList_add(e->trueEnsuresConstraints, cons); + + cons = constraint_makeEnsureGreaterThan (t1, t2, sequencePoint); + e->falseEnsuresConstraints = constraintList_add(e->falseEnsuresConstraints, cons); +} + + + +/*Logical operations */ + + + if (lltok_isAnd_Op (tok) ) + + { + //true ensures + tempList = constraintList_copy (t1->trueEnsuresConstraints); + tempList = constraintList_addList (tempList, t2->trueEnsuresConstraints); + 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); + + /* evans - was constraintList_addList - memory leak detected by lclint */ + e->falseEnsuresConstraints =constraintList_addListFree (e->falseEnsuresConstraints, tempList); + } + else if (lltok_isOr_Op (tok) ) + { + //false ensures + tempList = constraintList_copy (t1->falseEnsuresConstraints); + tempList = constraintList_addList (tempList, t2->falseEnsuresConstraints); + 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); + constraintList_free(temp); + + e->trueEnsuresConstraints = constraintList_addListFree(e->trueEnsuresConstraints, tempList); + tempList = constraintList_undefined; + } + else + { + DPRINTF((message("%s is not a boolean operation", lltok_unparse(tok) ) )); + } +} + +void exprNode_exprTraverse (exprNode e, bool definatelv, bool definaterv, /*@observer@*/ /*@temp@*/ fileloc sequencePoint) +{ + exprNode t1, t2, fcn; + lltok tok; + bool handledExprNode; + exprData data; + constraint cons; + + constraintList temp; + + if (exprNode_isError(e) ) + { + return; // FALSE; + } + + DPRINTF((message ("exprNode_exprTraverset Analysising %s %s at", exprNode_unparse( e), + fileloc_unparse(exprNode_getfileloc(e) ) ) ) ); + + /*e->requiresConstraints = constraintList_makeNew(); + e->ensuresConstraints = constraintList_makeNew(); + e->trueEnsuresConstraints = constraintList_makeNew();; + e->falseEnsuresConstraints = constraintList_makeNew();; + */ + if (exprNode_isUnhandled (e) ) + { + return; // FALSE; + } + // e = makeDataTypeConstraints (e); + + handledExprNode = TRUE; + + data = e->edata; + + switch (e->kind) + { + case XPR_WHILEPRED: + t1 = exprData_getSingle (data); + exprNode_exprTraverse (t1, definatelv, definaterv, sequencePoint); + e = exprNode_copyConstraints (e, t1); + break; + + case XPR_FETCH: + + if (definatelv ) + { + 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 ); + } + + e->requiresConstraints = constraintList_add(e->requiresConstraints, cons); + cons = constraint_makeEnsureMaxReadAtLeast (t1, t2, sequencePoint); + e->ensuresConstraints = constraintList_add(e->ensuresConstraints, cons); + + cons = constraint_makeEnsureLteMaxRead (t2, t1); + e->trueEnsuresConstraints = constraintList_add(e->trueEnsuresConstraints, cons); + + // 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); + + /*@i325 Should check which is array/index. */ + break; + + case XPR_PARENS: + exprNode_exprTraverse (exprData_getUopNode (e->edata), definatelv, definaterv, sequencePoint); + // e->constraints = constraintList_exprNodemerge (exprData_getUopNode (e->edata), exprNode_undefined); + break; + case XPR_INIT: + { + /* + idDecl t; + + uentry ue; + exprNode lhs; + + t = exprData_getInitId (data); + ue = usymtab_lookup (idDecl_observeId (t)); + lhs = exprNode_createId (ue); + */ + t2 = exprData_getInitNode (data); + + /* DPRINTF(( (message("initialization: %s = %s", + exprNode_unparse(lhs), + exprNode_unparse(t2) + ) + ) )); */ + + //exprNode_exprTraverse (t1, TRUE, FALSE, 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)) ) + { + cons = constraint_makeEnsureEqual (e, t2, sequencePoint); + e->ensuresConstraints = constraintList_add(e->ensuresConstraints, cons); + } + } + + break; + case XPR_ASSIGN: + t1 = exprData_getOpA (data); + t2 = exprData_getOpB (data); + exprNode_exprTraverse (t1, TRUE, definaterv, sequencePoint ); + //lltok_unparse (exprData_getOpTok (data)); + + 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)) ) + { + cons = constraint_makeEnsureEqual (t1, t2, sequencePoint); + e->ensuresConstraints = constraintList_add(e->ensuresConstraints, cons); + } + break; + case XPR_OP: + t1 = exprData_getOpA (data); + t2 = exprData_getOpB (data); + tok = exprData_getOpTok (data); + + + if (tok.tok == ADD_ASSIGN) + { + exprNode_exprTraverse (t1, TRUE, definaterv, sequencePoint ); + exprNode_exprTraverse (t2, definatelv, TRUE, sequencePoint ); + + cons = constraint_makeAddAssign (t1, t2, sequencePoint ); + e->ensuresConstraints = constraintList_add(e->ensuresConstraints, cons); + } + else if (tok.tok == SUB_ASSIGN) + { + exprNode_exprTraverse (t1, TRUE, definaterv, sequencePoint ); + exprNode_exprTraverse (t2, definatelv, TRUE, 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 ); + } + + 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: + //drl possible problem : warning make sure the case can be ignored.. + + break; + + case XPR_SIZEOF: + exprNode_exprTraverse (exprData_getSingle (data), definatelv, definaterv, sequencePoint ); + // e->constraints = constraintList_exprNodemerge (exprData_getSingle (e->edata), exprNode_undefined); + break; + + 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) ) ) ) ); + + fcn->requiresConstraints = constraintList_addListFree (fcn->requiresConstraints, + checkCall (fcn, exprData_getArgs (data) ) ); + + fcn->ensuresConstraints = constraintList_addListFree (fcn->ensuresConstraints, + exprNode_getPostConditions(fcn, exprData_getArgs (data),e ) ); + + t1 = exprNode_createNew (exprNode_getType (e) ); + + checkArgumentList (t1, exprData_getArgs(data), sequencePoint); + + + exprNode_mergeResolve (e, t1, fcn); + + exprNode_free(t1); + + // e->constraints = constraintList_add (e->constraints, constraint_create (e,exprNode_undefined, GT, CALLSAFE ) ); + + break; + + case XPR_RETURN: + exprNode_exprTraverse (exprData_getSingle (data), definatelv, definaterv, sequencePoint ); + break; + + case XPR_NULLRETURN: + + break; + + + case XPR_FACCESS: + exprNode_exprTraverse (exprData_getFieldNode (data), definatelv, definaterv, sequencePoint ); + break; + + case XPR_ARROW: + exprNode_exprTraverse (exprData_getFieldNode (data), definatelv, definaterv, sequencePoint ); + break; + + case XPR_STRINGLITERAL: + + break; + + case XPR_NUMLIT: + + break; + + case XPR_PREOP: + t1 = exprData_getUopNode(data); + tok = (exprData_getUopTok (data)); + //lltok_unparse (exprData_getUopTok (data)); + exprNode_exprTraverse (t1, definatelv, definaterv, sequencePoint ); + /*handle * pointer access */ + if (lltok_isInc_Op (tok) ) + { + DPRINTF(("doing ++(var)")); + t1 = exprData_getUopNode (data); + cons = constraint_makeMaxSetSideEffectPostIncrement (t1, sequencePoint ); + e->ensuresConstraints = constraintList_add (e->ensuresConstraints, cons); + } + else if (lltok_isDec_Op (tok) ) + { + DPRINTF(("doing --(var)")); + t1 = exprData_getUopNode (data); + cons = constraint_makeMaxSetSideEffectPostDecrement (t1, sequencePoint ); + e->ensuresConstraints = constraintList_add (e->ensuresConstraints, cons); + } + else if (lltok_isMult( tok ) ) + { + if (definatelv) + { + cons = constraint_makeWriteSafeInt (t1, 0); + } + else + { + cons = constraint_makeReadSafeInt (t1, 0); + } + e->requiresConstraints = constraintList_add(e->requiresConstraints, cons); + } + 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 ); + + if (lltok_isInc_Op (exprData_getUopTok (data) ) ) + { + DPRINTF(("doing ++")); + t1 = exprData_getUopNode (data); + cons = constraint_makeMaxSetSideEffectPostIncrement (t1, sequencePoint ); + e->ensuresConstraints = constraintList_add (e->ensuresConstraints, cons); + } + if (lltok_isDec_Op (exprData_getUopTok (data) ) ) + { + DPRINTF(("doing --")); + t1 = exprData_getUopNode (data); + 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", + qtype_unparse (exprData_getCastType (data)), + 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); + + //dfdf + 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: + llassert(FALSE); + t1 = exprData_getPairA (data); + t2 = exprData_getPairB (data); + /* 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_mergeResolve (e, t1, t2); + break; + + default: + handledExprNode = FALSE; + } + + 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); + + 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) ) )); + + return; // handledExprNode; } -bool exprNode_exprTraverse (exprNode e, bool definatelv, bool definaterv, fileloc sequencePoint) +constraintList exprNode_traversTrueEnsuresConstraints (exprNode e) { - exprNode t1, t2; - lltok tok; + exprNode t1; + bool handledExprNode; + // char * mes; exprData data; - constraint cons; - constraintList tempList; - - if (exprNode_handleError (e)) - { - return FALSE; - } - - TPRINTF((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();; + constraintList ret; + if (exprNode_handleError (e)) + { + ret = constraintList_makeNew(); + return ret; + } + ret = constraintList_copy (e->trueEnsuresConstraints ); - handledExprNode = TRUE; + handledExprNode = TRUE; data = e->edata; switch (e->kind) { - - case XPR_WHILEPRED: t1 = exprData_getSingle (data); - exprNode_exprTraverse (t1, definatelv, definaterv, sequencePoint); - e = exprNode_copyConstraints (e, t1); + ret = constraintList_addListFree ( ret, exprNode_traversTrueEnsuresConstraints (t1) ); break; - - case XPR_FETCH: - - if (definatelv ) - { - 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 ); - } - e->requiresConstraints = constraintList_add(e->requiresConstraints, cons); - cons = constraint_makeEnsureMaxReadAtLeast (t1, t2, sequencePoint); - e->ensuresConstraints = constraintList_add(e->ensuresConstraints, cons); - // 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); + case XPR_FETCH: - /*@i325 Should check which is array/index. */ + ret = constraintList_addListFree (ret, + exprNode_traversTrueEnsuresConstraints + (exprData_getPairA (data) ) ); + + ret = constraintList_addListFree (ret, + exprNode_traversTrueEnsuresConstraints + (exprData_getPairB (data) ) ); break; - case XPR_PREOP: - t1 = exprData_getUopNode(data); - //lltok_unparse (exprData_getUopTok (data)); - exprNode_exprTraverse (t1, definatelv, definaterv, sequencePoint ); - /*handle * pointer access */ - - /*@ i 325 do ++ and -- */ - if (lltok_isMult( exprData_getUopTok (data) ) ) - { - if (definatelv) - { - cons = constraint_makeWriteSafeInt (t1, 0); - } - else - { - cons = constraint_makeReadSafeInt (t1, 0); - } - e->requiresConstraints = constraintList_add(e->requiresConstraints, cons); - } - - /* ! expr */ - if (lltok_isNot_Op (exprData_getUopTok (data) ) ) - { - e->trueEnsuresConstraints = constraintList_copy (t1->falseEnsuresConstraints); - e->falseEnsuresConstraints = constraintList_copy (t1->trueEnsuresConstraints); - } + case XPR_PREOP: + + ret = constraintList_addListFree (ret, + exprNode_traversTrueEnsuresConstraints + (exprData_getUopNode (data) ) ); break; case XPR_PARENS: - exprNode_exprTraverse (exprData_getUopNode (e->edata), definatelv, definaterv, sequencePoint); - // e->constraints = constraintList_exprNodemerge (exprData_getUopNode (e->edata), exprNode_undefined); - break; - case XPR_ASSIGN: - t1 = exprData_getOpA (data); - t2 = exprData_getOpB (data); - exprNode_exprTraverse (t1, TRUE, definaterv, sequencePoint ); - lltok_unparse (exprData_getOpTok (data)); - exprNode_exprTraverse (t2, definatelv, TRUE, sequencePoint ); + ret = constraintList_addListFree (ret, exprNode_traversTrueEnsuresConstraints + (exprData_getUopNode (data) ) ); + break; - // TPRINTF ( ("Doing ASSign")); - cons = constraint_makeEnsureEqual (t1, t2, sequencePoint); - - e->ensuresConstraints = constraintList_add(e->ensuresConstraints, cons); + case XPR_INIT: + ret = constraintList_addListFree (ret, + exprNode_traversTrueEnsuresConstraints + (exprData_getInitNode (data) ) ); + break; - break; - case XPR_OP: - t1 = exprData_getOpA (data); - t2 = exprData_getOpB (data); - - exprNode_exprTraverse (t1, definatelv, definaterv, sequencePoint ); - tok = exprData_getOpTok (data); - exprNode_exprTraverse (t2, definatelv, definaterv, sequencePoint ); - if (lltok_isEq_Op (tok) ) - { - cons = constraint_makeEnsureEqual (t1, t2, sequencePoint); - e->trueEnsuresConstraints = constraintList_add(e->trueEnsuresConstraints, cons); - } - if (lltok_isAnd_Op (tok) ) - { - //true ensures - tempList = constraintList_copy (t1->trueEnsuresConstraints); - tempList = constraintList_addList (tempList, t2->trueEnsuresConstraints); - e->trueEnsuresConstraints = constraintList_addList(e->trueEnsuresConstraints, tempList); - - //false ensures: fens t1 or tens t1 and fens t2 - tempList = constraintList_copy (t1->trueEnsuresConstraints); - tempList = constraintList_addList (tempList, t2->falseEnsuresConstraints); - tempList = constraintList_logicalOr (tempList, t1->falseEnsuresConstraints); - e->falseEnsuresConstraints =constraintList_addList(e->falseEnsuresConstraints, tempList); - - } - 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); - - //true ensures: tens t1 or fens t1 and tens t2 - tempList = constraintList_copy (t1->falseEnsuresConstraints); - tempList = constraintList_addList (tempList, t2->trueEnsuresConstraints); - tempList = constraintList_logicalOr (tempList, t1->trueEnsuresConstraints); - e->trueEnsuresConstraints =constraintList_addList(e->trueEnsuresConstraints, tempList); - - } - // e->constraints = constraintList_exprNodemerge (exprData_getOpA (data), exprData_getOpB (data)); - break; + case XPR_ASSIGN: + ret = constraintList_addListFree (ret, + exprNode_traversTrueEnsuresConstraints + (exprData_getOpA (data) ) ); + + ret = constraintList_addListFree (ret, + exprNode_traversTrueEnsuresConstraints + (exprData_getOpB (data) ) ); + break; + case XPR_OP: + ret = constraintList_addListFree (ret, + exprNode_traversTrueEnsuresConstraints + (exprData_getOpA (data) ) ); + + ret = constraintList_addListFree (ret, + exprNode_traversTrueEnsuresConstraints + (exprData_getOpB (data) ) ); + break; case XPR_SIZEOFT: - ctype_unparse (qtype_getType (exprData_getType (data) ) ); + + // ctype_unparse (qtype_getType (exprData_getType (data) ) ); break; case XPR_SIZEOF: - exprNode_exprTraverse (exprData_getSingle (data), definatelv, definaterv, sequencePoint ); - // e->constraints = constraintList_exprNodemerge (exprData_getSingle (e->edata), exprNode_undefined); - break; + + ret = constraintList_addListFree (ret, + exprNode_traversTrueEnsuresConstraints + (exprData_getSingle (data) ) ); + break; case XPR_CALL: - exprNode_exprTraverse (exprData_getFcn (data), definatelv, definaterv, sequencePoint ); - exprNodeList_unparse (exprData_getArgs (data) ); - // e->constraints = constraintList_add (e->constraints, constraint_create (e,exprNode_undefined, GT, CALLSAFE ) ); - break; + ret = constraintList_addListFree (ret, + exprNode_traversTrueEnsuresConstraints + (exprData_getFcn (data) ) ); + /*@i11*/ // exprNodeList_unparse (exprData_getArgs (data) ); + break; case XPR_RETURN: - exprNode_exprTraverse (exprData_getSingle (data), definatelv, definaterv, sequencePoint ); + ret = constraintList_addListFree (ret, + exprNode_traversTrueEnsuresConstraints + (exprData_getSingle (data) ) ); break; case XPR_NULLRETURN: - cstring_makeLiteral ("return");; + // cstring_makeLiteral ("return");; break; - - + case XPR_FACCESS: - exprNode_exprTraverse (exprData_getFieldNode (data), definatelv, definaterv, sequencePoint ); - exprData_getFieldName (data) ; + ret = constraintList_addListFree (ret, + exprNode_traversTrueEnsuresConstraints + (exprData_getFieldNode (data) ) ); + //exprData_getFieldName (data) ; break; case XPR_ARROW: - exprNode_exprTraverse (exprData_getFieldNode (data), definatelv, definaterv, sequencePoint ); - exprData_getFieldName (data); + ret = constraintList_addListFree (ret, + exprNode_traversTrueEnsuresConstraints + (exprData_getFieldNode (data) ) ); + // exprData_getFieldName (data); break; case XPR_STRINGLITERAL: - cstring_copy (exprData_getLiteral (data)); + // cstring_copy (exprData_getLiteral (data)); break; case XPR_NUMLIT: - cstring_copy (exprData_getLiteral (data)); + // cstring_copy (exprData_getLiteral (data)); 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 ++")); - t1 = exprData_getUopNode (data); - cons = constraint_makeMaxSetSideEffectPostIncrement (t1, sequencePoint ); - e->ensuresConstraints = constraintList_add (e->ensuresConstraints, cons); - // cons = constraint_makeMaxReadSideEffectPostIncrement (t1, sequencePoint ); - //e->ensuresConstraints = constraintList_add (e->ensuresConstraints, cons); - } + + ret = constraintList_addListFree (ret, + exprNode_traversTrueEnsuresConstraints + (exprData_getUopNode (data) ) ); + break; + + case XPR_CAST: + + ret = constraintList_addListFree (ret, + exprNode_traversTrueEnsuresConstraints + (exprData_getCastNode (data) ) ); break; + default: - handledExprNode = FALSE; + break; } - e->requiresConstraints = constraintList_preserveOrig ( e->requiresConstraints); - e->ensuresConstraints = constraintList_preserveOrig ( e->ensuresConstraints); - - return handledExprNode; + return ret; } - -constraintList exprNode_traversTrueEnsuresConstraints (exprNode e) +constraintList exprNode_traversFalseEnsuresConstraints (exprNode e) { - // exprNode t1, t2; + exprNode t1; bool handledExprNode; // char * mes; @@ -661,10 +1498,10 @@ constraintList exprNode_traversTrueEnsuresConstraints (exprNode e) if (exprNode_handleError (e)) { - ret = constraintList_new(); + ret = constraintList_makeNew(); return ret; } - ret = constraintList_copy (e->trueEnsuresConstraints ); + ret = constraintList_copy (e->falseEnsuresConstraints ); handledExprNode = TRUE; @@ -672,44 +1509,54 @@ constraintList exprNode_traversTrueEnsuresConstraints (exprNode e) switch (e->kind) { + case XPR_WHILEPRED: + t1 = exprData_getSingle (data); + ret = constraintList_addListFree ( ret,exprNode_traversFalseEnsuresConstraints (t1) ); + break; case XPR_FETCH: - ret = constraintList_addList (ret, - exprNode_traversTrueEnsuresConstraints + ret = constraintList_addListFree (ret, + exprNode_traversFalseEnsuresConstraints (exprData_getPairA (data) ) ); - ret = constraintList_addList (ret, - exprNode_traversTrueEnsuresConstraints + ret = constraintList_addListFree (ret, + exprNode_traversFalseEnsuresConstraints (exprData_getPairB (data) ) ); break; case XPR_PREOP: - ret = constraintList_addList (ret, - exprNode_traversTrueEnsuresConstraints + ret = constraintList_addListFree (ret, + exprNode_traversFalseEnsuresConstraints (exprData_getUopNode (data) ) ); break; case XPR_PARENS: - ret = constraintList_addList (ret, exprNode_traversTrueEnsuresConstraints + ret = constraintList_addListFree (ret, exprNode_traversFalseEnsuresConstraints (exprData_getUopNode (data) ) ); break; + case XPR_INIT: + ret = constraintList_addListFree (ret, + exprNode_traversFalseEnsuresConstraints + ( exprData_getInitNode (data) ) ); + break; + case XPR_ASSIGN: - ret = constraintList_addList (ret, - exprNode_traversTrueEnsuresConstraints + ret = constraintList_addListFree (ret, + exprNode_traversFalseEnsuresConstraints (exprData_getOpA (data) ) ); - ret = constraintList_addList (ret, - exprNode_traversTrueEnsuresConstraints + ret = constraintList_addListFree (ret, + exprNode_traversFalseEnsuresConstraints (exprData_getOpB (data) ) ); break; case XPR_OP: - ret = constraintList_addList (ret, - exprNode_traversTrueEnsuresConstraints + ret = constraintList_addListFree (ret, + exprNode_traversFalseEnsuresConstraints (exprData_getOpA (data) ) ); - ret = constraintList_addList (ret, - exprNode_traversTrueEnsuresConstraints + ret = constraintList_addListFree (ret, + exprNode_traversFalseEnsuresConstraints (exprData_getOpB (data) ) ); break; case XPR_SIZEOFT: @@ -720,21 +1567,21 @@ constraintList exprNode_traversTrueEnsuresConstraints (exprNode e) case XPR_SIZEOF: - ret = constraintList_addList (ret, - exprNode_traversTrueEnsuresConstraints + ret = constraintList_addListFree (ret, + exprNode_traversFalseEnsuresConstraints (exprData_getSingle (data) ) ); break; case XPR_CALL: - ret = constraintList_addList (ret, - exprNode_traversTrueEnsuresConstraints + ret = constraintList_addListFree (ret, + exprNode_traversFalseEnsuresConstraints (exprData_getFcn (data) ) ); /*@i11*/ // exprNodeList_unparse (exprData_getArgs (data) ); break; case XPR_RETURN: - ret = constraintList_addList (ret, - exprNode_traversTrueEnsuresConstraints + ret = constraintList_addListFree (ret, + exprNode_traversFalseEnsuresConstraints (exprData_getSingle (data) ) ); break; @@ -743,15 +1590,15 @@ constraintList exprNode_traversTrueEnsuresConstraints (exprNode e) break; case XPR_FACCESS: - ret = constraintList_addList (ret, - exprNode_traversTrueEnsuresConstraints + ret = constraintList_addListFree (ret, + exprNode_traversFalseEnsuresConstraints (exprData_getFieldNode (data) ) ); //exprData_getFieldName (data) ; break; case XPR_ARROW: - ret = constraintList_addList (ret, - exprNode_traversTrueEnsuresConstraints + ret = constraintList_addListFree (ret, + exprNode_traversFalseEnsuresConstraints (exprData_getFieldNode (data) ) ); // exprData_getFieldName (data); break; @@ -765,10 +1612,18 @@ constraintList exprNode_traversTrueEnsuresConstraints (exprNode e) break; case XPR_POSTOP: - ret = constraintList_addList (ret, - exprNode_traversTrueEnsuresConstraints + ret = constraintList_addListFree (ret, + exprNode_traversFalseEnsuresConstraints (exprData_getUopNode (data) ) ); break; + + case XPR_CAST: + + ret = constraintList_addListFree (ret, + exprNode_traversFalseEnsuresConstraints + (exprData_getCastNode (data) ) ); + break; + default: break; } @@ -778,9 +1633,9 @@ constraintList exprNode_traversTrueEnsuresConstraints (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, t2; + exprNode t1; bool handledExprNode; // char * mes; @@ -789,7 +1644,7 @@ constraintList exprNode_traversRequiresConstraints (exprNode e) if (exprNode_handleError (e)) { - ret = constraintList_new(); + ret = constraintList_makeNew(); return ret; } ret = constraintList_copy (e->requiresConstraints ); @@ -800,43 +1655,53 @@ constraintList exprNode_traversRequiresConstraints (exprNode e) switch (e->kind) { + case XPR_WHILEPRED: + t1 = exprData_getSingle (data); + 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_INIT: + ret = constraintList_addListFree (ret, + exprNode_traversRequiresConstraints + (exprData_getInitNode (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; @@ -848,20 +1713,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; @@ -871,14 +1736,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); @@ -893,10 +1758,18 @@ 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_addListFree (ret, + exprNode_traversRequiresConstraints + (exprData_getCastNode (data) ) ); + break; + default: break; } @@ -906,9 +1779,9 @@ 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, t2; + exprNode t1; bool handledExprNode; // char * mes; @@ -920,7 +1793,7 @@ constraintList exprNode_traversEnsuresConstraints (exprNode e) if (exprNode_handleError (e)) { - ret = constraintList_new(); + ret = constraintList_makeNew(); return ret; } @@ -939,43 +1812,55 @@ constraintList exprNode_traversEnsuresConstraints (exprNode e) switch (e->kind) { + case XPR_WHILEPRED: + t1 = exprData_getSingle (data); + 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_INIT: + ret = constraintList_addListFree (ret, + exprNode_traversEnsuresConstraints + (exprData_getInitNode (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; @@ -987,20 +1872,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; @@ -1010,14 +1895,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); @@ -1032,10 +1917,17 @@ 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_addListFree (ret, + exprNode_traversEnsuresConstraints + (exprData_getCastNode (data) ) ); + break; + default: break; } @@ -1051,3 +1943,84 @@ DPRINTF( (message ( return ret; } +/*drl moved out of constraintResolve.c 07-02-001 */ +void checkArgumentList (/*@out@*/ exprNode temp, exprNodeList arglist, fileloc sequencePoint) +{ + temp->requiresConstraints = constraintList_makeNew(); + temp->ensuresConstraints = constraintList_makeNew(); + temp->trueEnsuresConstraints = constraintList_makeNew(); + temp->falseEnsuresConstraints = constraintList_makeNew(); + + exprNodeList_elements (arglist, el) + { + constraintList temp2; + exprNode_exprTraverse (el, FALSE, FALSE, sequencePoint); + temp2 = el->requiresConstraints; + el->requiresConstraints = exprNode_traversRequiresConstraints(el); + constraintList_free(temp2); + + temp2 = el->ensuresConstraints; + el->ensuresConstraints = exprNode_traversEnsuresConstraints(el); + constraintList_free(temp2); + + temp->requiresConstraints = constraintList_addList(temp->requiresConstraints, + el->requiresConstraints); + + temp->ensuresConstraints = constraintList_addList(temp->ensuresConstraints, + el->ensuresConstraints); + } + end_exprNodeList_elements; + +} + +/*drl moved out of constraintResolve.c 07-03-001 */ +constraintList exprNode_getPostConditions (exprNode fcn, exprNodeList arglist, exprNode fcnCall) +{ + constraintList postconditions; + uentry temp; + DPRINTF( (message ("Got call that %s ( %s) ", exprNode_unparse(fcn), exprNodeList_unparse (arglist ) ) ) ); + + temp = exprNode_getUentry (fcn); + + postconditions = uentry_getFcnPostconditions (temp); + + if (constraintList_isDefined(postconditions) ) + { + postconditions = constraintList_doSRefFixConstraintParam (postconditions, arglist); + postconditions = constraintList_doFixResult (postconditions, fcnCall); + } + else + { + postconditions = constraintList_makeNew(); + } + + return postconditions; +} + + +/*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 ) ) ) ); + + temp = exprNode_getUentry (fcn); + + preconditions = uentry_getFcnPreconditions (temp); + + if (constraintList_isDefined(preconditions) ) + { + preconditions = constraintList_togglePost (preconditions); + preconditions = constraintList_preserveCallInfo(preconditions, fcn); + preconditions = constraintList_doSRefFixConstraintParam (preconditions, arglist); + } + else + { + if (constraintList_isUndefined(preconditions) ) + preconditions = constraintList_makeNew(); + } + DPRINTF (( message("Done checkCall\n") )); + DPRINTF (( message("Returning list %q ", constraintList_printDetailed(preconditions) ) )); + return preconditions; +}