/* ** constraintGeneration.c */ //#define DEBUGPRINT 1 # include /* for isdigit */ # include "lclintMacros.nf" # include "basic.h" # include "cgrammar_tokens.h" # include "exprChecks.h" # include "exprNodeSList.h" //# include "exprDataQuite.i" /*@access exprNode @*/ static bool exprNode_handleError(/*@dependent@*/ exprNode p_e); //static cstring exprNode_findConstraints ( exprNode p_e); static bool exprNode_isMultiStatement(/*@dependent@*/ exprNode p_e); static void exprNode_multiStatement (/*@dependent@*/ exprNode p_e); //static void exprNode_constraintPropagateUp (exprNode p_e); static constraintList exprNode_traversTrueEnsuresConstraints (/*@dependent@*/ exprNode p_e); static constraintList exprNode_traversFalseEnsuresConstraints (/*@dependent@*/ exprNode p_e); static exprNode makeDataTypeConstraints (/*@returned@*/ exprNode p_e); static void checkArgumentList (/*@out@*/ exprNode p_temp, exprNodeList p_arglist, fileloc p_sequencePoint) /*@modifies p_temp @*/; static constraintList checkCall (/*@dependent@*/ exprNode p_fcn, exprNodeList p_arglist); //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) { case XPR_INITBLOCK: case XPR_EMPTY: case XPR_LABEL: case XPR_CONST: case XPR_VAR: case XPR_BODY: case XPR_OFFSETOF: case XPR_ALIGNOFT: case XPR_ALIGNOF: case XPR_VAARG: case XPR_ITERCALL: case XPR_ITER: case XPR_GOTO: case XPR_CONTINUE: case XPR_BREAK: case XPR_COMMA: case XPR_COND: case XPR_TOK: case XPR_FTDEFAULT: case XPR_DEFAULT: // case XPR_SWITCH: case XPR_FTCASE: case XPR_CASE: // case XPR_INIT: case XPR_NODE: DPRINTF((message ("Warning current constraint generation does not handle expression %s", exprNode_unparse(e)) ) ); return TRUE; /*@notreached@*/ break; default: return FALSE; } /*not reached*/ return FALSE; } bool exprNode_handleError( exprNode e) { if (exprNode_isError (e) || exprNode_isUnhandled(e) ) { static /*@only@*/ cstring error = cstring_undefined; if (!cstring_isDefined (error)) { error = cstring_makeLiteral (""); } /*@-unqualifiedtrans*/ return TRUE; /*@=unqualifiedtrans*/ } return FALSE; } bool /*@alt void@*/ exprNode_generateConstraints (/*@dependent@*/ exprNode e) { if (exprNode_isError (e) ) return FALSE; /* e->requiresConstraints = constraintList_makeNew(); e->ensuresConstraints = constraintList_makeNew(); e->trueEnsuresConstraints = constraintList_makeNew(); e->falseEnsuresConstraints = constraintList_makeNew(); */ if (exprNode_isUnhandled (e) ) { DPRINTF( (message("Warning ignoring %s", exprNode_unparse (e) ) ) ); return FALSE; } // e = makeDataTypeConstraints (e); DPRINTF((message ("exprNode_generateConstraints Analysising %s at %s", exprNode_unparse( e), fileloc_unparse(exprNode_getfileloc(e) ) ) ) ); if (exprNode_isMultiStatement ( e) ) { exprNode_multiStatement(e); } else { fileloc loc; loc = exprNode_getNextSequencePoint(e); exprNode_exprTraverse(e, FALSE, FALSE, loc); fileloc_free(loc); return FALSE; } { 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; } /* handles multiple statements */ bool exprNode_isMultiStatement(exprNode e) { if (exprNode_handleError (e) != NULL) return FALSE; switch (e->kind) { case XPR_FOR: case XPR_FORPRED: case XPR_IF: case XPR_IFELSE: case XPR_WHILE: case XPR_WHILEPRED: case XPR_DOWHILE: case XPR_BLOCK: case XPR_STMT: case XPR_STMTLIST: case XPR_SWITCH: return TRUE; default: return FALSE; } } static void exprNode_stmt ( /*@dependent@*/ exprNode e) { exprNode snode; fileloc loc; cstring s; if (exprNode_isError(e) ) { return; // FALSE; } /*e->requiresConstraints = constraintList_makeNew(); e->ensuresConstraints = constraintList_makeNew(); */ // e = makeDataTypeConstraints(e); DPRINTF(( "STMT:") ); 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) { DPRINTF (("Not Stmt") ); DPRINTF ( (message ("%s ", exprNode_unparse (e)) ) ); if (exprNode_isMultiStatement (e) ) { return exprNode_multiStatement (e ); } DPRINTF( (message ("Ignoring non-statement %s", exprNode_unparse(e) ) ) ); return; //TRUE; // llassert(FALSE); } DPRINTF (("Stmt") ); DPRINTF ( (message ("%s ", exprNode_unparse (e)) ) ); snode = exprData_getUopNode (e->edata); /* could be stmt involving multiple statements: i.e. if, while for ect. */ if (exprNode_isMultiStatement (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); 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); DPRINTF ( (message ("smtlist constraints are: pre: %s \n and \t post %s\n", constraintList_print(e->requiresConstraints), constraintList_print(e->ensuresConstraints) ) ) ); return; // notError; } static void exprNode_stmtList (/*@dependent@*/ exprNode e) { exprNode stmt1, stmt2; if (exprNode_isError (e) ) { return; // FALSE; } /* 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) { exprNode_stmt(e); return; } llassert (e->kind == XPR_STMTLIST); DPRINTF(( "STMTLIST:") ); DPRINTF ((cstring_toCharsSafe (exprNode_unparse(e)) ) ); stmt1 = exprData_getPairA (e->edata); stmt2 = exprData_getPairB (e->edata); DPRINTF((" stmtlist ") ); DPRINTF ((message("XW%s | %s", exprNode_unparse(stmt1), exprNode_unparse(stmt2) ) ) ); exprNode_stmt (stmt1); DPRINTF(("\nstmt after stmtList call " )); exprNode_stmt (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; } static exprNode doIf (/*@returned@*/ exprNode e, /*@dependent@*/ exprNode test, /*@dependent@*/ exprNode body) { 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); 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; } void exprNode_multiStatement (/*@dependent@*/ exprNode e) { bool ret; exprData data; exprNode e1, e2; exprNode p, trueBranch, falseBranch; exprNode forPred, forBody; 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; } data = e->edata; ret = TRUE; switch (e->kind) { case XPR_FOR: // ret = message ("%s %s", forPred = exprData_getPairA (data); forBody = exprData_getPairB (data); //first generate the constraints exprNode_generateConstraints (forPred); exprNode_generateConstraints (forBody); doFor (e, forPred, forBody); break; case XPR_FORPRED: // ret = message ("for (%s; %s; %s)", exprNode_generateConstraints (exprData_getTripleInit (data) ); 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: DPRINTF(( "IF:") ); DPRINTF ((exprNode_unparse(e) ) ); // ret = message ("if (%s) %s", e1 = exprData_getPairA (data); e2 = exprData_getPairB (data); exprNode_exprTraverse (e1, 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: DPRINTF(("Starting IFELSE")); // ret = message ("if (%s) %s else %s", p = exprData_getTriplePred (data); trueBranch = exprData_getTripleTrue (data); falseBranch = exprData_getTripleFalse (data); exprNode_exprTraverse (p, FALSE, FALSE, exprNode_loc(p)); 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") ); break; 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) ) )); 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: exprNode_stmtList (e); return ; /*@notreached@*/ break; default: ret=FALSE; } 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; } constraintList exprNode_traversTrueEnsuresConstraints (exprNode e) { exprNode t1; bool handledExprNode; // char * mes; exprData data; constraintList ret; if (exprNode_handleError (e)) { ret = constraintList_makeNew(); return ret; } ret = constraintList_copy (e->trueEnsuresConstraints ); handledExprNode = TRUE; data = e->edata; switch (e->kind) { case XPR_WHILEPRED: t1 = exprData_getSingle (data); ret = constraintList_addListFree ( ret, exprNode_traversTrueEnsuresConstraints (t1) ); break; case XPR_FETCH: ret = constraintList_addListFree (ret, exprNode_traversTrueEnsuresConstraints (exprData_getPairA (data) ) ); ret = constraintList_addListFree (ret, exprNode_traversTrueEnsuresConstraints (exprData_getPairB (data) ) ); break; case XPR_PREOP: ret = constraintList_addListFree (ret, exprNode_traversTrueEnsuresConstraints (exprData_getUopNode (data) ) ); break; case XPR_PARENS: ret = constraintList_addListFree (ret, exprNode_traversTrueEnsuresConstraints (exprData_getUopNode (data) ) ); break; case XPR_INIT: ret = constraintList_addListFree (ret, exprNode_traversTrueEnsuresConstraints (exprData_getInitNode (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) ) ); break; case XPR_SIZEOF: ret = constraintList_addListFree (ret, exprNode_traversTrueEnsuresConstraints (exprData_getSingle (data) ) ); break; case XPR_CALL: ret = constraintList_addListFree (ret, exprNode_traversTrueEnsuresConstraints (exprData_getFcn (data) ) ); /*@i11*/ // exprNodeList_unparse (exprData_getArgs (data) ); break; case XPR_RETURN: ret = constraintList_addListFree (ret, exprNode_traversTrueEnsuresConstraints (exprData_getSingle (data) ) ); break; case XPR_NULLRETURN: // cstring_makeLiteral ("return");; break; case XPR_FACCESS: ret = constraintList_addListFree (ret, exprNode_traversTrueEnsuresConstraints (exprData_getFieldNode (data) ) ); //exprData_getFieldName (data) ; break; case XPR_ARROW: ret = constraintList_addListFree (ret, exprNode_traversTrueEnsuresConstraints (exprData_getFieldNode (data) ) ); // exprData_getFieldName (data); break; case XPR_STRINGLITERAL: // cstring_copy (exprData_getLiteral (data)); break; case XPR_NUMLIT: // cstring_copy (exprData_getLiteral (data)); break; case XPR_POSTOP: ret = constraintList_addListFree (ret, exprNode_traversTrueEnsuresConstraints (exprData_getUopNode (data) ) ); break; case XPR_CAST: ret = constraintList_addListFree (ret, exprNode_traversTrueEnsuresConstraints (exprData_getCastNode (data) ) ); break; default: break; } return ret; } constraintList exprNode_traversFalseEnsuresConstraints (exprNode e) { exprNode t1; bool handledExprNode; // char * mes; exprData data; constraintList ret; if (exprNode_handleError (e)) { ret = constraintList_makeNew(); return ret; } ret = constraintList_copy (e->falseEnsuresConstraints ); handledExprNode = TRUE; data = e->edata; switch (e->kind) { case XPR_WHILEPRED: t1 = exprData_getSingle (data); ret = constraintList_addListFree ( ret,exprNode_traversFalseEnsuresConstraints (t1) ); break; case XPR_FETCH: ret = constraintList_addListFree (ret, exprNode_traversFalseEnsuresConstraints (exprData_getPairA (data) ) ); ret = constraintList_addListFree (ret, exprNode_traversFalseEnsuresConstraints (exprData_getPairB (data) ) ); break; case XPR_PREOP: ret = constraintList_addListFree (ret, exprNode_traversFalseEnsuresConstraints (exprData_getUopNode (data) ) ); break; case XPR_PARENS: 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_addListFree (ret, exprNode_traversFalseEnsuresConstraints (exprData_getOpA (data) ) ); ret = constraintList_addListFree (ret, exprNode_traversFalseEnsuresConstraints (exprData_getOpB (data) ) ); break; case XPR_OP: ret = constraintList_addListFree (ret, exprNode_traversFalseEnsuresConstraints (exprData_getOpA (data) ) ); ret = constraintList_addListFree (ret, exprNode_traversFalseEnsuresConstraints (exprData_getOpB (data) ) ); break; case XPR_SIZEOFT: // ctype_unparse (qtype_getType (exprData_getType (data) ) ); break; case XPR_SIZEOF: ret = constraintList_addListFree (ret, exprNode_traversFalseEnsuresConstraints (exprData_getSingle (data) ) ); break; case XPR_CALL: ret = constraintList_addListFree (ret, exprNode_traversFalseEnsuresConstraints (exprData_getFcn (data) ) ); /*@i11*/ // exprNodeList_unparse (exprData_getArgs (data) ); break; case XPR_RETURN: ret = constraintList_addListFree (ret, exprNode_traversFalseEnsuresConstraints (exprData_getSingle (data) ) ); break; case XPR_NULLRETURN: // cstring_makeLiteral ("return");; break; case XPR_FACCESS: ret = constraintList_addListFree (ret, exprNode_traversFalseEnsuresConstraints (exprData_getFieldNode (data) ) ); //exprData_getFieldName (data) ; break; case XPR_ARROW: ret = constraintList_addListFree (ret, exprNode_traversFalseEnsuresConstraints (exprData_getFieldNode (data) ) ); // exprData_getFieldName (data); break; case XPR_STRINGLITERAL: // cstring_copy (exprData_getLiteral (data)); break; case XPR_NUMLIT: // cstring_copy (exprData_getLiteral (data)); break; case XPR_POSTOP: 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; } return ret; } /* walk down the tree and get all requires Constraints in each subexpression*/ /*@only@*/ constraintList exprNode_traversRequiresConstraints (exprNode e) { exprNode t1; bool handledExprNode; // char * mes; exprData data; constraintList ret; if (exprNode_handleError (e)) { ret = constraintList_makeNew(); return ret; } ret = constraintList_copy (e->requiresConstraints ); handledExprNode = TRUE; data = e->edata; switch (e->kind) { case XPR_WHILEPRED: t1 = exprData_getSingle (data); ret = constraintList_addListFree ( ret, exprNode_traversRequiresConstraints (t1) ); break; case XPR_FETCH: ret = constraintList_addListFree (ret, exprNode_traversRequiresConstraints (exprData_getPairA (data) ) ); ret = constraintList_addListFree (ret, exprNode_traversRequiresConstraints (exprData_getPairB (data) ) ); break; case XPR_PREOP: ret = constraintList_addListFree (ret, exprNode_traversRequiresConstraints (exprData_getUopNode (data) ) ); break; case XPR_PARENS: 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_addListFree (ret, exprNode_traversRequiresConstraints (exprData_getOpA (data) ) ); ret = constraintList_addListFree (ret, exprNode_traversRequiresConstraints (exprData_getOpB (data) ) ); break; case XPR_OP: ret = constraintList_addListFree (ret, exprNode_traversRequiresConstraints (exprData_getOpA (data) ) ); ret = constraintList_addListFree (ret, exprNode_traversRequiresConstraints (exprData_getOpB (data) ) ); break; case XPR_SIZEOFT: // ctype_unparse (qtype_getType (exprData_getType (data) ) ); break; case XPR_SIZEOF: ret = constraintList_addListFree (ret, exprNode_traversRequiresConstraints (exprData_getSingle (data) ) ); break; case XPR_CALL: ret = constraintList_addListFree (ret, exprNode_traversRequiresConstraints (exprData_getFcn (data) ) ); /*@i11*/ // exprNodeList_unparse (exprData_getArgs (data) ); break; case XPR_RETURN: ret = constraintList_addListFree (ret, exprNode_traversRequiresConstraints (exprData_getSingle (data) ) ); break; case XPR_NULLRETURN: // cstring_makeLiteral ("return");; break; case XPR_FACCESS: ret = constraintList_addListFree (ret, exprNode_traversRequiresConstraints (exprData_getFieldNode (data) ) ); //exprData_getFieldName (data) ; break; case XPR_ARROW: ret = constraintList_addListFree (ret, exprNode_traversRequiresConstraints (exprData_getFieldNode (data) ) ); // exprData_getFieldName (data); break; case XPR_STRINGLITERAL: // cstring_copy (exprData_getLiteral (data)); break; case XPR_NUMLIT: // cstring_copy (exprData_getLiteral (data)); break; case XPR_POSTOP: 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; } return ret; } /* walk down the tree and get all Ensures Constraints in each subexpression*/ /*@only@*/ constraintList exprNode_traversEnsuresConstraints (exprNode e) { exprNode t1; bool handledExprNode; // char * mes; exprData data; // constraintExpr tmp; // constraint cons; constraintList ret; if (exprNode_handleError (e)) { ret = constraintList_makeNew(); return ret; } ret = constraintList_copy (e->ensuresConstraints ); handledExprNode = TRUE; data = e->edata; DPRINTF( (message ( "exprnode_traversEnsuresConstraints call for %s with constraintList of %s", exprNode_unparse (e), constraintList_print(e->ensuresConstraints) ) )); switch (e->kind) { case XPR_WHILEPRED: t1 = exprData_getSingle (data); ret = constraintList_addListFree ( ret,exprNode_traversEnsuresConstraints (t1) ); break; case XPR_FETCH: ret = constraintList_addListFree (ret, exprNode_traversEnsuresConstraints (exprData_getPairA (data) ) ); ret = constraintList_addListFree (ret, exprNode_traversEnsuresConstraints (exprData_getPairB (data) ) ); break; case XPR_PREOP: ret = constraintList_addListFree (ret, exprNode_traversEnsuresConstraints (exprData_getUopNode (data) ) ); break; case XPR_PARENS: 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_addListFree (ret, exprNode_traversEnsuresConstraints (exprData_getOpA (data) ) ); ret = constraintList_addListFree (ret, exprNode_traversEnsuresConstraints (exprData_getOpB (data) ) ); break; case XPR_OP: ret = constraintList_addListFree (ret, exprNode_traversEnsuresConstraints (exprData_getOpA (data) ) ); ret = constraintList_addListFree (ret, exprNode_traversEnsuresConstraints (exprData_getOpB (data) ) ); break; case XPR_SIZEOFT: // ctype_unparse (qtype_getType (exprData_getType (data) ) ); break; case XPR_SIZEOF: ret = constraintList_addListFree (ret, exprNode_traversEnsuresConstraints (exprData_getSingle (data) ) ); break; case XPR_CALL: ret = constraintList_addListFree (ret, exprNode_traversEnsuresConstraints (exprData_getFcn (data) ) ); /*@i11*/ // exprNodeList_unparse (exprData_getArgs (data) ); break; case XPR_RETURN: ret = constraintList_addListFree (ret, exprNode_traversEnsuresConstraints (exprData_getSingle (data) ) ); break; case XPR_NULLRETURN: // cstring_makeLiteral ("return");; break; case XPR_FACCESS: ret = constraintList_addListFree (ret, exprNode_traversEnsuresConstraints (exprData_getFieldNode (data) ) ); //exprData_getFieldName (data) ; break; case XPR_ARROW: ret = constraintList_addListFree (ret, exprNode_traversEnsuresConstraints (exprData_getFieldNode (data) ) ); // exprData_getFieldName (data); break; case XPR_STRINGLITERAL: // cstring_copy (exprData_getLiteral (data)); break; case XPR_NUMLIT: // cstring_copy (exprData_getLiteral (data)); break; case XPR_POSTOP: 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; } DPRINTF( (message ( "exprnode_traversEnsuresConstraints call for %s with constraintList of is returning %s", exprNode_unparse (e), // constraintList_print(e->ensuresConstraints), constraintList_print(ret) ) )); 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; }