X-Git-Url: http://andersk.mit.edu/gitweb/splint.git/blobdiff_plain/28bf4b0bfd405a2057d865910f8589c54a40f17b..312c981596ce6202de7686f2d4c46aec1bae3939:/src/constraintGeneration.c diff --git a/src/constraintGeneration.c b/src/constraintGeneration.c index 11f978e..dfb737d 100644 --- a/src/constraintGeneration.c +++ b/src/constraintGeneration.c @@ -1,12 +1,35 @@ +/* +** Splint - annotation-assisted static program checker +** Copyright (C) 1994-2002 University of Virginia, +** Massachusetts Institute of Technology +** +** This program is free software; you can redistribute it and/or modify it +** under the terms of the GNU General Public License as published by the +** Free Software Foundation; either version 2 of the License, or (at your +** option) any later version. +** +** This program is distributed in the hope that it will be useful, but +** WITHOUT ANY WARRANTY; without even the implied warranty of +** MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the GNU +** General Public License for more details. +** +** The GNU General Public License is available from http://www.gnu.org/ or +** the Free Software Foundation, Inc., 59 Temple Place - Suite 330, Boston, +** MA 02111-1307, USA. +** +** For information on splint: info@splint.org +** To report a bug: splint-bug@splint.org +** For more information: http://www.splint.org +*/ /* ** constraintGeneration.c */ -//#define DEBUGPRINT 1 +/* #define DEBUGPRINT 1 */ # include /* for isdigit */ -# include "lclintMacros.nf" +# include "splintMacros.nf" # include "basic.h" # include "cgrammar_tokens.h" @@ -14,44 +37,26 @@ # include "exprChecks.h" # include "exprNodeSList.h" -//# include "exprDataQuite.i" - -/*@access exprNode @*/ - +/*@access exprNode@*/ /* NO! Don't do this recklessly! */ +/*@-nullderef@*/ /* DRL needs to fix this code! */ +/*@-nullpass@*/ /* DRL needs to fix this code! */ +/*@-temptrans@*/ /* DRL needs to fix this code! */ -static bool exprNode_handleError(/*@dependent@*/ exprNode p_e); +static /*@truewhennull@*/ bool exprNode_handleError (/*@temp@*/ 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_stmt (/*@temp@*/ /*@temp@*/ exprNode p_e); +static void exprNode_multiStatement (/*@temp@*/ 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 constraintList exprNode_traversTrueEnsuresConstraints (/*@temp@*/ exprNode p_e); +static constraintList exprNode_traversFalseEnsuresConstraints (/*@temp@*/ exprNode p_e); static void checkArgumentList (/*@out@*/ exprNode p_temp, exprNodeList p_arglist, fileloc p_sequencePoint) /*@modifies p_temp @*/; -static constraintList checkCall (/*@dependent@*/ exprNode p_fcn, exprNodeList p_arglist); - -//constraintList constraintList_makeFixedArrayConstraints (sRefSet s); - -//bool exprNode_testd() -//{ - /* if ( ( (exprNode_isError ) ) ) - { - } - if ( ( (e_1 ) ) ) - { - } - */ -//} +static constraintList checkCall (/*@temp@*/ exprNode p_fcn, exprNodeList p_arglist); -static bool exprNode_isUnhandled (/*@dependent@*/ /*@obsever@*/ exprNode e) +static bool exprNode_isUnhandled (/*@temp@*/ /*@observer@*/ exprNode e) { - llassert( exprNode_isDefined(e) ); + llassert(exprNode_isDefined(e)); switch (e->kind) { case XPR_INITBLOCK: @@ -74,12 +79,10 @@ static bool exprNode_isUnhandled (/*@dependent@*/ /*@obsever@*/ exprNode e) 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)) ) ); + DPRINTF((message ("Warning current constraint generation does not handle expression %s", exprNode_unparse(e)))); return TRUE; /*@notreached@*/ break; @@ -91,58 +94,47 @@ static bool exprNode_isUnhandled (/*@dependent@*/ /*@obsever@*/ exprNode e) return FALSE; } -bool exprNode_handleError( exprNode e) +bool exprNode_handleError (exprNode e) { - if (exprNode_isError (e) || exprNode_isUnhandled(e) ) + if (exprNode_isError (e) || exprNode_isUnhandled (e)) { - static /*@only@*/ cstring error = cstring_undefined; - - if (!cstring_isDefined (error)) - { - error = cstring_makeLiteral (""); - } - - /*@-unqualifiedtrans*/ return TRUE; /*@=unqualifiedtrans*/ + return TRUE; } + return FALSE; } -bool /*@alt void@*/ exprNode_generateConstraints (/*@dependent@*/ exprNode e) +/* evans 2002-03-2 - parameter was dependent */ +bool /*@alt void@*/ exprNode_generateConstraints (/*@temp@*/ exprNode e) { - if (exprNode_isError (e) ) + if (exprNode_isError (e)) return FALSE; - /* - e->requiresConstraints = constraintList_makeNew(); - e->ensuresConstraints = constraintList_makeNew(); - e->trueEnsuresConstraints = constraintList_makeNew(); - e->falseEnsuresConstraints = constraintList_makeNew(); - */ - if (exprNode_isUnhandled (e) ) + if (exprNode_isUnhandled (e)) { - DPRINTF( (message("Warning ignoring %s", exprNode_unparse (e) ) ) ); - return FALSE; + DPRINTF((message("Warning ignoring %s", exprNode_unparse (e)))); + return FALSE; } - - // e = makeDataTypeConstraints (e); - - DPRINTF((message ("exprNode_generateConstraints Analysising %s at %s", exprNode_unparse( e), - fileloc_unparse(exprNode_getfileloc(e) ) ) ) ); + DPRINTF((message ("exprNode_generateConstraints Analysising %s at %s", exprNode_unparse(e), + fileloc_unparse(exprNode_getfileloc(e))))); - if (exprNode_isMultiStatement ( e) ) + if (exprNode_isMultiStatement (e)) { exprNode_multiStatement(e); } else { - fileloc loc; +/* fileloc loc; */ - loc = exprNode_getNextSequencePoint(e); - exprNode_exprTraverse(e, FALSE, FALSE, loc); +/* loc = exprNode_getNextSequencePoint(e); */ +/* exprNode_exprTraverse(e, FALSE, FALSE, loc); */ - fileloc_free(loc); +/* fileloc_free(loc); */ + + exprNode_stmt(e); return FALSE; + } { @@ -150,67 +142,36 @@ bool /*@alt void@*/ exprNode_generateConstraints (/*@dependent@*/ exprNode e) 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) ) ) ); + 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: - return TRUE; - default: - return FALSE; - } - -} - -static void exprNode_stmt ( /*@dependent@*/ exprNode e) +static void exprNode_stmt (/*@temp@*/ exprNode e) { exprNode snode; fileloc loc; cstring s; - if (exprNode_isError(e) ) + if (exprNode_isError(e)) { - return; // FALSE; + return; } + /*e->requiresConstraints = constraintList_makeNew(); e->ensuresConstraints = constraintList_makeNew(); */ - // e = makeDataTypeConstraints(e); - - DPRINTF(( "STMT:") ); + DPRINTF(("expNode_stmt: STMT:")); s = exprNode_unparse(e); - // DPRINTF ( ( message("STMT: %s ") ) ); + DPRINTF ((message("exprNode_stmt: STMT: %s ", s))); if (e->kind == XPR_INIT) { constraintList tempList; - DPRINTF (("Init") ); - DPRINTF ( (message ("%s ", exprNode_unparse (e)) ) ); + DPRINTF (("Init")); + DPRINTF ((message ("%s ", exprNode_unparse (e)))); loc = exprNode_getNextSequencePoint(e); /* reduces to an expression */ exprNode_exprTraverse (e, FALSE, FALSE, loc); fileloc_free(loc); @@ -222,25 +183,48 @@ static void exprNode_stmt ( /*@dependent@*/ exprNode e) tempList = e->ensuresConstraints; e->ensuresConstraints = exprNode_traversEnsuresConstraints(e); constraintList_free(tempList); - return; // notError; + return; + } + + /*drl 2/13/002 patched bug so return statement will be checked*/ + /*return is a stmt not not expression ...*/ + if (e->kind == XPR_RETURN) + { + constraintList tempList; + + loc = exprNode_getNextSequencePoint(e); /* reduces to an expression */ + + exprNode_exprTraverse (exprData_getSingle (e->edata), FALSE, TRUE, loc); + fileloc_free(loc); + + tempList = e->requiresConstraints; + e->requiresConstraints = exprNode_traversRequiresConstraints(e); + constraintList_free(tempList); } if (e->kind != XPR_STMT) { - DPRINTF (("Not Stmt") ); - DPRINTF ( (message ("%s ", exprNode_unparse (e)) ) ); - if (exprNode_isMultiStatement (e) ) + DPRINTF (("Not Stmt")); + DPRINTF ((message ("%s ", exprNode_unparse (e)))); + + if (exprNode_isMultiStatement (e)) { - return exprNode_multiStatement (e ); + exprNode_multiStatement (e); /* evans 2001-08-21: spurious return removed */ } - DPRINTF( (message ("Ignoring non-statement %s", exprNode_unparse(e) ) ) ); - return; //TRUE; - // llassert(FALSE); + else + { + loc = exprNode_getNextSequencePoint(e); /* reduces to an expression */ + + exprNode_exprTraverse (e, FALSE, TRUE, loc); + fileloc_free(loc); + + } + return; } - DPRINTF (("Stmt") ); - DPRINTF ( (message ("%s ", exprNode_unparse (e)) ) ); + DPRINTF (("Stmt")); + DPRINTF ((message ("%s ", exprNode_unparse (e)))); snode = exprData_getUopNode (e->edata); @@ -250,107 +234,97 @@ static void exprNode_stmt ( /*@dependent@*/ exprNode e) if (exprNode_isMultiStatement (snode)) { - 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); 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", + DPRINTF ((message ("smtlist constraints are: pre: %s \n and \t post %s\n", constraintList_print(e->requiresConstraints), - constraintList_print(e->ensuresConstraints) ) ) ); + constraintList_print(e->ensuresConstraints)))); - return; // notError; - + return; } - static void exprNode_stmtList (/*@dependent@*/ exprNode e) { exprNode stmt1, stmt2; - if (exprNode_isError (e) ) + if (exprNode_isError (e)) { - return; // FALSE; + return; } /* - e->requiresConstraints = constraintList_makeNew(); - e->ensuresConstraints = constraintList_makeNew(); + Handle case of stmtList with only one statement: + The parse tree stores this as stmt instead of stmtList */ - // 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)) ) ); + DPRINTF(("exprNode_stmtList 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) ) ) ); + DPRINTF(("exprNode_stmtlist ")); + DPRINTF ((message("XW%s | %s", exprNode_unparse(stmt1), exprNode_unparse(stmt2)))); exprNode_stmt (stmt1); - DPRINTF(("\nstmt after stmtList call " )); + DPRINTF(("\nstmt after stmtList call ")); exprNode_stmt (stmt2); - exprNode_mergeResolve (e, stmt1, stmt2 ); + exprNode_mergeResolve (e, stmt1, stmt2); - DPRINTF ( (message ("smtlist constraints are: pre: %s \n and \t post %s\n", + DPRINTF ((message ("smtlist constraints are: pre: %s \n and \t post %s\n", constraintList_print(e->requiresConstraints), - constraintList_print(e->ensuresConstraints) ) ) ); - return; // TRUE; + constraintList_print(e->ensuresConstraints)))); + return; } static exprNode doIf (/*@returned@*/ exprNode e, /*@dependent@*/ exprNode test, /*@dependent@*/ exprNode body) { constraintList temp; - DPRINTF ((message ("doIf: %s ", exprNode_unparse(e) ) ) ); + DPRINTF ((message ("doIf: %s ", exprNode_unparse(e)))); - llassert(exprNode_isDefined(test) ); - llassert (exprNode_isDefined (e) ); - llassert (exprNode_isDefined (body) ); + llassert(exprNode_isDefined(test)); + llassert (exprNode_isDefined (e)); + llassert (exprNode_isDefined (body)); - DPRINTF((message ("ensures constraints for %s are %s", exprNode_unparse(e), constraintList_printDetailed(e->ensuresConstraints) ) )); + DPRINTF((message ("ensures constraints for %s are %s", exprNode_unparse(e), constraintList_printDetailed(e->ensuresConstraints)))); - DPRINTF((message ("Requires constraints for %s are %s", exprNode_unparse(e), constraintList_printDetailed(e->ensuresConstraints) ) )); + DPRINTF((message ("Requires constraints for %s are %s", exprNode_unparse(e), constraintList_printDetailed(e->ensuresConstraints)))); - DPRINTF((message ("trueEnsures constraints for %s are %s", exprNode_unparse(e), constraintList_printDetailed(e->trueEnsuresConstraints) ) )); + DPRINTF((message ("trueEnsures constraints for %s are %s", exprNode_unparse(e), constraintList_printDetailed(e->trueEnsuresConstraints)))); - DPRINTF((message ("falseEnsures constraints for %s are %s", exprNode_unparse(e), constraintList_printDetailed(e->falseEnsuresConstraints) ) )); + DPRINTF((message ("falseEnsures constraints for %s are %s", exprNode_unparse(e), constraintList_printDetailed(e->falseEnsuresConstraints)))); - DPRINTF((message ("ensures constraints for %s are %s", exprNode_unparse(test), constraintList_printDetailed(test->ensuresConstraints) ) )); + DPRINTF((message ("ensures constraints for %s are %s", exprNode_unparse(test), constraintList_printDetailed(test->ensuresConstraints)))); - DPRINTF((message ("Requires constraints for %s are %s", exprNode_unparse(test), constraintList_printDetailed(test->ensuresConstraints) ) )); + DPRINTF((message ("Requires constraints for %s are %s", exprNode_unparse(test), constraintList_printDetailed(test->ensuresConstraints)))); - DPRINTF((message ("trueEnsures constraints for %s are %s", exprNode_unparse(test), constraintList_printDetailed(test->trueEnsuresConstraints) ) )); + DPRINTF((message ("trueEnsures constraints for %s are %s", exprNode_unparse(test), constraintList_printDetailed(test->trueEnsuresConstraints)))); - DPRINTF((message ("falseEnsures constraints for %s are %s", exprNode_unparse(test), constraintList_printDetailed(test->falseEnsuresConstraints) ) )); + DPRINTF((message ("falseEnsures constraints for %s are %s", exprNode_unparse(test), constraintList_printDetailed(test->falseEnsuresConstraints)))); @@ -369,11 +343,13 @@ static exprNode doIf (/*@returned@*/ exprNode e, /*@dependent@*/ exprNode test, test->trueEnsuresConstraints = constraintList_substituteFreeTarget(test->trueEnsuresConstraints, test->ensuresConstraints); - DPRINTF ((message ("doIf: test ensures %s ", constraintList_print(test->ensuresConstraints) ) ) ); + DPRINTF ((message ("doIf: test ensures %s ", constraintList_print(test->ensuresConstraints)))); - DPRINTF ((message ("doIf: test true ensures %s ", constraintList_print(test->trueEnsuresConstraints) ) ) ); + DPRINTF ((message ("doIf: test true ensures %s ", constraintList_print(test->trueEnsuresConstraints)))); constraintList_free(e->requiresConstraints); + + e->requiresConstraints = constraintList_reflectChanges(body->requiresConstraints, test->trueEnsuresConstraints); e->requiresConstraints = constraintList_reflectChangesFreePre (e->requiresConstraints, @@ -383,18 +359,18 @@ static exprNode doIf (/*@returned@*/ exprNode e, /*@dependent@*/ exprNode test, constraintList_free(temp); -//drl possible problem : warning bad + /* drl possible problem : warning bad */ constraintList_free(e->ensuresConstraints); e->ensuresConstraints = constraintList_copy (test->ensuresConstraints); - if (exprNode_mayEscape (body) ) + if (exprNode_mayEscape (body)) { - DPRINTF (( message("doIf: the if statement body %s returns or exits", exprNode_unparse(body) ) )); + DPRINTF ((message("doIf: the if statement body %s returns or exits", exprNode_unparse(body)))); e->ensuresConstraints = constraintList_mergeEnsuresFreeFirst (e->ensuresConstraints, test->falseEnsuresConstraints); } - DPRINTF ((message ("doIf: if requiers %s ", constraintList_print(e->requiresConstraints) ) ) ); + DPRINTF ((message ("doIf: if requiers %s ", constraintList_print(e->requiresConstraints)))); return e; } @@ -409,59 +385,63 @@ static exprNode doIf (/*@returned@*/ exprNode e, /*@dependent@*/ exprNode test, exprNode_traversFalseEnsuresConstraints have all been run */ - static exprNode doIfElse (/*@returned@*/ exprNode e, /*@dependent@*/ exprNode p, /*@dependent@*/ exprNode trueBranch, /*@dependent@*/ exprNode falseBranch) { + constraintList c1, cons, t, t2, f, f2; - 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); + llassert (exprNode_isDefined (e)); + llassert (exprNode_isDefined (p)); + llassert (exprNode_isDefined (trueBranch)); + llassert (exprNode_isDefined (falseBranch)); + DPRINTF ((message ("doIfElse: %s ", exprNode_unparse(e)))); + + /* do requires clauses */ + c1 = constraintList_copy (p->ensuresConstraints); + + 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 + */ - DPRINTF ((message ("doIfElse: if requires %q ", constraintList_print(e->requiresConstraints) ) ) ); - DPRINTF ((message ("doIfElse: if ensures %q ", constraintList_print(e->ensuresConstraints) ) ) ); - - return e; + 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) ) ) ); + DPRINTF ((message ("doWhile: %s ", exprNode_unparse(e)))); return doIf (e, test, body); } @@ -473,47 +453,46 @@ static exprNode doWhile (/*@returned@*/ exprNode e, /*@dependent@*/ exprNode tes 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);*/ - } - } + if (sRef_isFixedArray(el)) + { + size_t size; + DPRINTF((message("%s is a fixed array", + sRef_unparse(el)))); + size = sRef_getArraySize(el); + DPRINTF((message("%s is a fixed array with size %d", + sRef_unparse(el), (int)size))); + con = constraint_makeSRefSetBufferSize (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; + end_sRefSet_elements ; + + DPRINTF((message("constraintList_makeFixedArrayConstraints returning %s", + constraintList_print(ret)))); + return ret; } +# if 0 exprNode makeDataTypeConstraints (/*@returned@*/ exprNode e) { constraintList c; @@ -525,68 +504,347 @@ exprNode makeDataTypeConstraints (/*@returned@*/ exprNode e) return e; } +# endif 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) ) ) ) + /* merge the constraints: modle as if statement */ + + /* init + if (test) + for body + inc */ + + llassert (exprNode_isDefined (e)); + llassert (exprNode_isDefined (forPred)); + llassert (exprNode_isDefined (forBody)); + + init = exprData_getTripleInit (forPred->edata); + test = exprData_getTripleTest (forPred->edata); + inc = exprData_getTripleInc (forPred->edata); + + if (((exprNode_isError (test) /*|| (exprNode_isError(init))*/) || (exprNode_isError (inc)))) + { + DPRINTF ((message ("strange for statement:%s, ignoring it", exprNode_unparse(e)))); + 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)); + } + else + { + DPRINTF(("Can break")); + } +} + +static /*@dependent@*/ exprNode exprNode_makeDependent(/*@returned@*/ exprNode e) +{ + /* !!! DRL - this is ridiculous! Read the manual on memory annotations please! */ + return e; +} + +static void +exprNode_doGenerateConstraintSwitch + (/*@dependent@*/ exprNode switchExpr, + /*@dependent@*/ exprNode body, + /*@special@*/ constraintList *currentRequires, + /*@special@*/ constraintList *currentEnsures, + /*@special@*/ constraintList *savedRequires, + /*@special@*/ constraintList *savedEnsures) + /*@post:only *currentRequires, *currentEnsures, *savedRequires, *savedEnsures @*/ + /*@sets *currentRequires, *currentEnsures, *savedRequires, *savedEnsures @*/ +{ + exprNode stmt, stmtList; + + DPRINTF((message("exprNode_doGenerateConstraintSwitch: (switch %s) %s", + exprNode_unparse(switchExpr), exprNode_unparse(body) + ))); + + if (exprNode_isError(body)) + { + *currentRequires = constraintList_makeNew (); + *currentEnsures = constraintList_makeNew (); + + *savedRequires = constraintList_makeNew (); + *savedEnsures = constraintList_makeNew (); + /*@-onlytrans@*/ + return; + /*@=onlytrans@*/ + } + + if (body->kind != XPR_STMTLIST) + { + DPRINTF((message("exprNode_doGenerateConstraintSwitch: non stmtlist: %s", + exprNode_unparse(body)))); + stmt = body; + stmtList = exprNode_undefined; + stmt = exprNode_makeDependent(stmt); + stmtList = exprNode_makeDependent(stmtList); + } + else + { + stmt = exprData_getPairB(body->edata); + stmtList = exprData_getPairA(body->edata); + stmt = exprNode_makeDependent(stmt); + stmtList = exprNode_makeDependent(stmtList); + } + + DPRINTF((message("exprNode_doGenerateConstraintSwitch: stmtlist: %s stmt: %s", + exprNode_unparse(stmtList), exprNode_unparse(stmt)) + )); + + + exprNode_doGenerateConstraintSwitch (switchExpr, stmtList, currentRequires, currentEnsures, + savedRequires, savedEnsures); + + if (exprNode_isError(stmt)) + /*@-onlytrans@*/ + return; + /*@=onlytrans@*/ + + exprNode_stmt(stmt); + + switchExpr = exprNode_makeDependent (switchExpr); + + if (! exprNode_isCaseMarker(stmt)) + { + + constraintList temp; + + DPRINTF ((message("Got normal statement %s (requires %s ensures %s)", exprNode_unparse(stmt), + constraintList_unparse(stmt->requiresConstraints), constraintList_unparse(stmt->ensuresConstraints)))); + + temp = constraintList_reflectChanges (stmt->requiresConstraints, + *currentEnsures); + + *currentRequires = constraintList_mergeRequiresFreeFirst( + *currentRequires, + temp); + + constraintList_free(temp); + + *currentEnsures = constraintList_mergeEnsuresFreeFirst + (*currentEnsures, + stmt->ensuresConstraints); + DPRINTF((message("returning from exprNode_doGenerateConstraintSwitch: (switch %s) %s currentRequires:" + "%s currentEnsures:%s", + exprNode_unparse(switchExpr), exprNode_unparse(body), + constraintList_print(*currentRequires), constraintList_print(*currentEnsures) + ))); + /*@-onlytrans@*/ + return; + /*@=onlytrans@*/ + + } + + if (exprNode_isCaseMarker(stmt) && exprNode_mustEscape(stmtList)) + { + /* + ** merge current and saved constraint with Logical Or... + ** make a constraint for ensures + */ + + constraintList temp; + constraint con; + + DPRINTF ((message("Got case marker"))); + + if (constraintList_isUndefined(*savedEnsures) && + constraintList_isUndefined(*savedRequires)) { - DPRINTF ((message ("strange for statement:%s, ignoring it", exprNode_unparse(e) ) ) ); - return; + llassert(constraintList_isUndefined(*savedEnsures)); + llassert(constraintList_isUndefined(*savedRequires)); + *savedEnsures = constraintList_copy(*currentEnsures); + *savedRequires = constraintList_copy(*currentRequires); } + else + { + DPRINTF ((message("Doing logical or"))); + temp = constraintList_logicalOr (*savedEnsures, *currentEnsures); + constraintList_free (*savedEnsures); + *savedEnsures = temp; + + *savedRequires = constraintList_mergeRequiresFreeFirst (*savedRequires, *currentRequires); + } + + con = constraint_makeEnsureEqual (switchExpr, exprData_getSingle + (stmt->edata), exprNode_getfileloc(stmt)); + - exprNode_forLoopHeuristics(e, forPred, forBody); + constraintList_free(*currentEnsures); + *currentEnsures = constraintList_makeNew(); + *currentEnsures = constraintList_add(*currentEnsures, con); + + constraintList_free(*currentRequires); + *currentRequires = constraintList_makeNew(); + DPRINTF((message("exprNode_doGenerateConstraintSwitch: (switch %s) %s savedRequires:" + "%s savedEnsures:%s", + exprNode_unparse(switchExpr), exprNode_unparse(body), + constraintList_print(*savedRequires), constraintList_print(*savedEnsures) + ))); + + } + + else if (exprNode_isCaseMarker(stmt)) + /* prior case has no break. */ + { + /* + We don't do anything to the sved constraints because the case hasn't ended + The new ensures constraints for the case will be: + the constraint for the case statement (CASE_LABEL == SWITCH_EXPR) logicalOr currentEnsures + */ - 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); + constraintList temp; + constraint con; + + constraintList ensuresTemp; + + DPRINTF ((message("Got case marker with no prior break"))); + + con = constraint_makeEnsureEqual (switchExpr, exprData_getSingle + (stmt->edata), exprNode_getfileloc(stmt)); - if (!forBody->canBreak) + ensuresTemp = constraintList_makeNew(); + + ensuresTemp = constraintList_add (ensuresTemp, con); + + if (exprNode_isError(stmtList)) { - 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; + constraintList_free(*currentEnsures); + + *currentEnsures = constraintList_copy(ensuresTemp); + constraintList_free(ensuresTemp); + } else { - DPRINTF(("Can break") ); + + temp = constraintList_logicalOr (*currentEnsures, ensuresTemp); + + constraintList_free(*currentEnsures); + constraintList_free(ensuresTemp); + + *currentEnsures = temp; } + constraintList_free(*currentRequires); + *currentRequires = constraintList_makeNew(); + } + else + { + /* + we handle the case of ! exprNode_isCaseMarker above + the else if clause should always be true. + */ + BADEXIT; + } + + DPRINTF((message("returning from exprNode_doGenerateConstraintSwitch: (switch %s) %s currentRequires:" + "%s currentEnsures:%s", + exprNode_unparse(switchExpr), exprNode_unparse(body), + constraintList_print(*currentRequires), constraintList_print(*currentEnsures) + ))); + /*@-onlytrans@*/ + return; + /*@=onlytrans@*/ } -static exprNode doSwitch (/*@returned@*/ exprNode e) + +static void exprNode_generateConstraintSwitch (/*@notnull@*/ exprNode switchStmt) +{ + constraintList constraintsRequires; + constraintList constraintsEnsures; + constraintList lastRequires; + constraintList lastEnsures; + + exprNode body; + exprNode switchExpr; + + switchExpr = exprData_getPairA (switchStmt->edata); + body = exprData_getPairB (switchStmt->edata); + + if (!exprNode_isDefined (body)) + { + return; + } + + /*@i22*/ + DPRINTF((message(""))); + + if (body->kind == XPR_BLOCK) + body = exprData_getSingle(body->edata); + + /* + constraintsRequires = constraintList_undefined; + constraintsEnsures = constraintList_undefined; + + lastRequires = constraintList_makeNew(); + lastEnsures = constraintList_makeNew(); + */ + + /*@-mustfree@*/ + /*@i6534 - evans 2002-01-01: spurious warnings for these becuase of stack allocated storage */ + exprNode_doGenerateConstraintSwitch (switchExpr, body, &lastRequires, + &lastEnsures, &constraintsRequires, &constraintsEnsures); + /*@=mustfree@*/ + + /* + merge current and saved constraint with Logical Or... + make a constraint for ensures + */ + + constraintList_free(switchStmt->requiresConstraints); + constraintList_free(switchStmt->ensuresConstraints); + + if (constraintList_isDefined(constraintsEnsures) && constraintList_isDefined(constraintsRequires)) + { + switchStmt->ensuresConstraints = constraintList_logicalOr(constraintsEnsures, lastEnsures); + switchStmt->requiresConstraints = constraintList_mergeRequires(constraintsRequires, lastRequires); + constraintList_free (constraintsRequires); + constraintList_free (constraintsEnsures); + } + else + { + switchStmt->ensuresConstraints = constraintList_copy(lastEnsures); + switchStmt->requiresConstraints = constraintList_copy(lastRequires); + } + + constraintList_free (lastRequires); + constraintList_free (lastEnsures); + + DPRINTF(((message(" exprNode_generateConstraintSwitch returning requires: %s and ensures %s", + constraintList_print(switchStmt->requiresConstraints), + constraintList_print(switchStmt->ensuresConstraints) + ) + ))); +} + +static exprNode doSwitch (/*@returned@*/ /*@notnull@*/ 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))) )); + DPRINTF ((message ("doSwitch for: switch (%s) %s", + exprNode_unparse (exprData_getPairA (data)), + exprNode_unparse (exprData_getPairB (data))))); body = exprData_getPairB (data); - - // exprNode_generateConstraints(body); - - // e->requiresConstraints = constraintList_copy ( body->requiresConstraints ); - //e->ensuresConstraints = constraintList_copy ( body->ensuresConstraints ); - + exprNode_generateConstraintSwitch (e); return e; } - void exprNode_multiStatement (/*@dependent@*/ exprNode e) { @@ -599,20 +857,12 @@ void exprNode_multiStatement (/*@dependent@*/ exprNode e) 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) ) ) ) ); + DPRINTF((message ("exprNode_multistatement Analysising %s %s at", exprNode_unparse(e), + fileloc_unparse(exprNode_getfileloc(e))))); if (exprNode_handleError (e)) { - return; // FALSE; + return; } data = e->edata; @@ -623,11 +873,10 @@ void exprNode_multiStatement (/*@dependent@*/ exprNode e) { case XPR_FOR: - // ret = message ("%s %s", forPred = exprData_getPairA (data); forBody = exprData_getPairB (data); - //first generate the constraints + /* First generate the constraints */ exprNode_generateConstraints (forPred); exprNode_generateConstraints (forBody); @@ -637,13 +886,12 @@ void exprNode_multiStatement (/*@dependent@*/ exprNode e) break; case XPR_FORPRED: - // ret = message ("for (%s; %s; %s)", - exprNode_generateConstraints (exprData_getTripleInit (data) ); + exprNode_generateConstraints (exprData_getTripleInit (data)); test = exprData_getTripleTest (data); exprNode_exprTraverse (test,FALSE, FALSE, exprNode_loc(e)); - exprNode_generateConstraints (exprData_getTripleInc (data) ); + exprNode_generateConstraints (exprData_getTripleInc (data)); - if (!exprNode_isError(test) ) + if (!exprNode_isError(test)) { constraintList temp2; temp2 = test->trueEnsuresConstraints; @@ -668,27 +916,21 @@ void exprNode_multiStatement (/*@dependent@*/ exprNode e) break; case XPR_IF: - DPRINTF(( "IF:") ); - DPRINTF ((exprNode_unparse(e) ) ); - // ret = message ("if (%s) %s", + DPRINTF(("IF:")); + DPRINTF ((exprNode_unparse(e))); e1 = exprData_getPairA (data); e2 = exprData_getPairB (data); - exprNode_exprTraverse (e1, - FALSE, FALSE, exprNode_loc(e1)); + 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); @@ -697,6 +939,7 @@ void exprNode_multiStatement (/*@dependent@*/ exprNode e) exprNode_generateConstraints (trueBranch); exprNode_generateConstraints (falseBranch); + llassert (exprNode_isDefined (p)); temp = p->ensuresConstraints; p->ensuresConstraints = exprNode_traversEnsuresConstraints (p); constraintList_free(temp); @@ -709,37 +952,52 @@ void exprNode_multiStatement (/*@dependent@*/ exprNode e) p->trueEnsuresConstraints = exprNode_traversTrueEnsuresConstraints(p); constraintList_free(temp); + + + DPRINTF((message("p->trueEnsuresConstraints before substitue %s", constraintList_print(p->trueEnsuresConstraints) ) + )); + + /*drl 10/10/2002 this is a bit of a hack but the reason why we do this is so that any function post conditions or similar things get applied correctly to each branch. e.g. in strlen(s) < 5 we want the trueEnsures to be maxRead(s) < 5*/ + + p->trueEnsuresConstraints = constraintList_substituteFreeTarget (p->trueEnsuresConstraints, + p->ensuresConstraints); + + DPRINTF(( message ("p->trueEnsuresConstraints after substitue %s", constraintList_print(p->trueEnsuresConstraints) ) + )); + temp = p->falseEnsuresConstraints; p->falseEnsuresConstraints = exprNode_traversFalseEnsuresConstraints(p); constraintList_free(temp); - e = doIfElse (e, p, trueBranch, falseBranch); - DPRINTF( ("Done IFELSE") ); + /*See comment on trueEnsures*/ + p->falseEnsuresConstraints = constraintList_substituteFreeTarget (p->falseEnsuresConstraints, + p->ensuresConstraints); + + e = doIfElse (e, p, trueBranch, falseBranch); + DPRINTF(("Done IFELSE")); break; - + case XPR_DOWHILE: e2 = (exprData_getPairB (data)); e1 = (exprData_getPairA (data)); - DPRINTF((message ("do { %s } while (%s)", exprNode_unparse(e2), exprNode_unparse(e1) ) )); + DPRINTF((message ("do { %s } while (%s)", exprNode_unparse(e2), exprNode_unparse(e1)))); exprNode_generateConstraints (e2); exprNode_generateConstraints (e1); e = exprNode_copyConstraints (e, e2); - DPRINTF ((message ("e = %s ", constraintList_print(e->requiresConstraints) ) )); + DPRINTF ((message ("e = %s ", constraintList_print(e->requiresConstraints)))); break; 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; + 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); break; case XPR_SWITCH: @@ -754,7 +1012,7 @@ void exprNode_multiStatement (/*@dependent@*/ exprNode e) default: ret=FALSE; } - return; // ret; + return; } static bool lltok_isBoolean_Op (lltok tok) @@ -763,36 +1021,36 @@ static bool lltok_isBoolean_Op (lltok tok) I don't want to violate the abstraction maybe this should go in lltok.c */ - if (lltok_isEq_Op (tok) ) + if (lltok_isEq_Op (tok)) { return TRUE; } - if (lltok_isAnd_Op (tok) ) + if (lltok_isAnd_Op (tok)) { return TRUE; } - if (lltok_isOr_Op (tok) ) + if (lltok_isOr_Op (tok)) { return TRUE; } - if (lltok_isGt_Op (tok) ) + if (lltok_isGt_Op (tok)) { return TRUE; } - if (lltok_isLt_Op (tok) ) + if (lltok_isLt_Op (tok)) { return TRUE; } - if (lltok_isLe_Op (tok) ) + if (lltok_isLe_Op (tok)) { return TRUE; } - if (lltok_isGe_Op (tok) ) + if (lltok_isGe_Op (tok)) { return TRUE; } @@ -804,100 +1062,89 @@ static bool lltok_isBoolean_Op (lltok tok) 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) ) -{ + constraint cons; + exprNode t1, t2; + exprData data; + lltok tok; + constraintList tempList, temp; + data = e->edata; - cons = constraint_makeEnsureGreaterThanEqual (t1, t2, sequencePoint); - e->trueEnsuresConstraints = constraintList_add(e->trueEnsuresConstraints, cons); + tok = exprData_getOpTok (data); + t1 = exprData_getOpA (data); + t2 = exprData_getOpB (data); - cons = constraint_makeEnsureLessThan (t1, t2, sequencePoint); - e->falseEnsuresConstraints = constraintList_add(e->falseEnsuresConstraints, cons); + tempList = constraintList_undefined; -} - - - 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); + /* arithmetic tests */ - cons = constraint_makeEnsureGreaterThan (t1, t2, sequencePoint); - e->falseEnsuresConstraints = constraintList_add(e->falseEnsuresConstraints, cons); -} + if (lltok_isEq_Op (tok)) + { + cons = constraint_makeEnsureEqual (t1, t2, sequencePoint); + e->trueEnsuresConstraints = constraintList_add(e->trueEnsuresConstraints, cons); + } - - -/*Logical operations */ - - - if (lltok_isAnd_Op (tok) ) + + 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); + } - { - //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); - - e->falseEnsuresConstraints =constraintList_addList(e->falseEnsuresConstraints, tempList); + if (lltok_isGe_Op (tok)) + { + cons = constraint_makeEnsureGreaterThanEqual (t1, t2, sequencePoint); + e->trueEnsuresConstraints = constraintList_add(e->trueEnsuresConstraints, cons); - } - else if (lltok_isOr_Op (tok) ) - { - //false ensures + 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 splint */ + 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 + /* true ensures: tens t1 or fens t1 and tens t2 */ tempList = constraintList_copy (t1->falseEnsuresConstraints); tempList = constraintList_addList (tempList, t2->trueEnsuresConstraints); @@ -905,17 +1152,13 @@ if (lltok_isLe_Op (tok) ) tempList = constraintList_logicalOr (tempList, t1->trueEnsuresConstraints); constraintList_free(temp); - - e->trueEnsuresConstraints =constraintList_addListFree(e->trueEnsuresConstraints, tempList); + e->trueEnsuresConstraints = constraintList_addListFree(e->trueEnsuresConstraints, tempList); tempList = constraintList_undefined; - - } - else + else { - DPRINTF((message("%s is not a boolean operation", lltok_unparse(tok) ) )); - } - + DPRINTF((message("%s is not a boolean operation", lltok_unparse(tok)))); + } } void exprNode_exprTraverse (exprNode e, bool definatelv, bool definaterv, /*@observer@*/ /*@temp@*/ fileloc sequencePoint) @@ -928,27 +1171,27 @@ void exprNode_exprTraverse (exprNode e, bool definatelv, bool definaterv, /*@ob constraintList temp; - if (exprNode_isError(e) ) + if (exprNode_isError(e)) { - return; // FALSE; + return; } - DPRINTF((message ("exprNode_exprTraverset Analysising %s %s at", exprNode_unparse( e), - fileloc_unparse(exprNode_getfileloc(e) ) ) ) ); + DPRINTF((message ("exprNode_exprTraverset Analysising %s %s at", exprNode_unparse(e), + fileloc_unparse(exprNode_getfileloc(e))))); /*e->requiresConstraints = constraintList_makeNew(); e->ensuresConstraints = constraintList_makeNew(); e->trueEnsuresConstraints = constraintList_makeNew();; e->falseEnsuresConstraints = constraintList_makeNew();; */ - if (exprNode_isUnhandled (e) ) + + if (exprNode_isUnhandled (e)) { - return; // FALSE; + return; } - // e = makeDataTypeConstraints (e); - - handledExprNode = TRUE; - + + handledExprNode = TRUE; + data = e->edata; switch (e->kind) @@ -961,17 +1204,17 @@ void exprNode_exprTraverse (exprNode e, bool definatelv, bool definaterv, /*@ob case XPR_FETCH: - if (definatelv ) + if (definatelv) { - t1 = (exprData_getPairA (data) ); - t2 = (exprData_getPairB (data) ); + t1 = (exprData_getPairA (data)); + t2 = (exprData_getPairB (data)); cons = constraint_makeWriteSafeExprNode (t1, t2); } else { - t1 = (exprData_getPairA (data) ); - t2 = (exprData_getPairB (data) ); - cons = constraint_makeReadSafeExprNode (t1, t2 ); + t1 = (exprData_getPairA (data)); + t2 = (exprData_getPairB (data)); + cons = constraint_makeReadSafeExprNode (t1, t2); } e->requiresConstraints = constraintList_add(e->requiresConstraints, cons); @@ -981,18 +1224,14 @@ void exprNode_exprTraverse (exprNode e, bool definatelv, bool definaterv, /*@ob 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. */ + /*@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: { @@ -1008,18 +1247,16 @@ void exprNode_exprTraverse (exprNode e, bool definatelv, bool definaterv, /*@ob */ t2 = exprData_getInitNode (data); - /* DPRINTF(( (message("initialization: %s = %s", + /* DPRINTF(((message("initialization: %s = %s", exprNode_unparse(lhs), exprNode_unparse(t2) - ) - ) )); */ - - //exprNode_exprTraverse (t1, TRUE, FALSE, sequencePoint ); + ) + ))); */ - exprNode_exprTraverse (t2, definatelv, TRUE, sequencePoint ); + exprNode_exprTraverse (t2, definatelv, TRUE, sequencePoint); /* this test is nessecary because some expressions generate a null expression node. function pointer do that -- drl */ - if ( (!exprNode_isError (e)) && (!exprNode_isError(t2)) ) + if ((!exprNode_isError (e)) && (!exprNode_isError(t2))) { cons = constraint_makeEnsureEqual (e, t2, sequencePoint); e->ensuresConstraints = constraintList_add(e->ensuresConstraints, cons); @@ -1030,13 +1267,11 @@ void exprNode_exprTraverse (exprNode e, bool definatelv, bool definaterv, /*@ob case XPR_ASSIGN: t1 = exprData_getOpA (data); t2 = exprData_getOpB (data); - exprNode_exprTraverse (t1, TRUE, definaterv, sequencePoint ); - //lltok_unparse (exprData_getOpTok (data)); - - exprNode_exprTraverse (t2, definatelv, TRUE, sequencePoint ); + exprNode_exprTraverse (t1, TRUE, definaterv, sequencePoint); + exprNode_exprTraverse (t2, definatelv, TRUE, sequencePoint); /* this test is nessecary because some expressions generate a null expression node. function pointer do that -- drl */ - if ( (!exprNode_isError (t1)) && (!exprNode_isError(t2)) ) + if ((!exprNode_isError (t1)) && (!exprNode_isError(t2))) { cons = constraint_makeEnsureEqual (t1, t2, sequencePoint); e->ensuresConstraints = constraintList_add(e->ensuresConstraints, cons); @@ -1045,73 +1280,67 @@ void exprNode_exprTraverse (exprNode e, bool definatelv, bool definaterv, /*@ob case XPR_OP: t1 = exprData_getOpA (data); t2 = exprData_getOpB (data); - tok = exprData_getOpTok (data); - + tok = exprData_getOpTok (data); - if (tok.tok == ADD_ASSIGN) + if (lltok_getTok (tok) == ADD_ASSIGN) { - exprNode_exprTraverse (t1, TRUE, definaterv, sequencePoint ); - exprNode_exprTraverse (t2, definatelv, TRUE, sequencePoint ); + exprNode_exprTraverse (t1, TRUE, definaterv, sequencePoint); + exprNode_exprTraverse (t2, definatelv, TRUE, sequencePoint); - cons = constraint_makeAddAssign (t1, t2, sequencePoint ); + cons = constraint_makeAddAssign (t1, t2, sequencePoint); e->ensuresConstraints = constraintList_add(e->ensuresConstraints, cons); } - else if (tok.tok == SUB_ASSIGN) + else if (lltok_getTok (tok) == SUB_ASSIGN) { - exprNode_exprTraverse (t1, TRUE, definaterv, sequencePoint ); - exprNode_exprTraverse (t2, definatelv, TRUE, sequencePoint ); + exprNode_exprTraverse (t1, TRUE, definaterv, sequencePoint); + exprNode_exprTraverse (t2, definatelv, TRUE, sequencePoint); - cons = constraint_makeSubtractAssign (t1, t2, sequencePoint ); + cons = constraint_makeSubtractAssign (t1, t2, sequencePoint); e->ensuresConstraints = constraintList_add(e->ensuresConstraints, cons); } else { - exprNode_exprTraverse (t1, definatelv, definaterv, sequencePoint ); - exprNode_exprTraverse (t2, definatelv, definaterv, sequencePoint ); + exprNode_exprTraverse (t1, definatelv, definaterv, sequencePoint); + exprNode_exprTraverse (t2, definatelv, definaterv, sequencePoint); } - if (lltok_isBoolean_Op (tok) ) + if (lltok_isBoolean_Op (tok)) exprNode_booleanTraverse (e, definatelv, definaterv, sequencePoint); - // 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.. + /*@i43 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); + case XPR_SIZEOF: + /* drl 7-16-01 + C standard says operand to sizeof isn't evaluated unless + its a variable length array. So we don't generate constraints. + */ + 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) ) ) ) ); + exprNode_exprTraverse (fcn, definatelv, definaterv, sequencePoint); + DPRINTF ((message ("Got call that %s (%s) ", exprNode_unparse(fcn), exprNodeList_unparse (exprData_getArgs (data))))); fcn->requiresConstraints = constraintList_addListFree (fcn->requiresConstraints, - checkCall (fcn, exprData_getArgs (data) ) ); + checkCall (fcn, exprData_getArgs (data) )); fcn->ensuresConstraints = constraintList_addListFree (fcn->ensuresConstraints, - exprNode_getPostConditions(fcn, exprData_getArgs (data),e ) ); + exprNode_getPostConditions(fcn, exprData_getArgs (data),e )); - t1 = exprNode_createNew (exprNode_getType (e) ); - + t1 = exprNode_createNew (exprNode_getType (e)); checkArgumentList (t1, exprData_getArgs(data), sequencePoint); - - exprNode_mergeResolve (e, t1, fcn); - exprNode_free(t1); - - // 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 ); + exprNode_exprTraverse (exprData_getSingle (data), definatelv, definaterv, sequencePoint); break; case XPR_NULLRETURN: @@ -1120,11 +1349,11 @@ void exprNode_exprTraverse (exprNode e, bool definatelv, bool definaterv, /*@ob case XPR_FACCESS: - exprNode_exprTraverse (exprData_getFieldNode (data), definatelv, definaterv, sequencePoint ); + exprNode_exprTraverse (exprData_getFieldNode (data), definatelv, definaterv, sequencePoint); break; case XPR_ARROW: - exprNode_exprTraverse (exprData_getFieldNode (data), definatelv, definaterv, sequencePoint ); + exprNode_exprTraverse (exprData_getFieldNode (data), definatelv, definaterv, sequencePoint); break; case XPR_STRINGLITERAL: @@ -1138,24 +1367,23 @@ void exprNode_exprTraverse (exprNode e, bool definatelv, bool definaterv, /*@ob case XPR_PREOP: t1 = exprData_getUopNode(data); tok = (exprData_getUopTok (data)); - //lltok_unparse (exprData_getUopTok (data)); - exprNode_exprTraverse (t1, definatelv, definaterv, sequencePoint ); + exprNode_exprTraverse (t1, definatelv, definaterv, sequencePoint); /*handle * pointer access */ - if (lltok_isInc_Op (tok) ) + if (lltok_isInc_Op (tok)) { DPRINTF(("doing ++(var)")); t1 = exprData_getUopNode (data); - cons = constraint_makeMaxSetSideEffectPostIncrement (t1, sequencePoint ); + cons = constraint_makeMaxSetSideEffectPostIncrement (t1, sequencePoint); e->ensuresConstraints = constraintList_add (e->ensuresConstraints, cons); } - else if (lltok_isDec_Op (tok) ) + else if (lltok_isDec_Op (tok)) { DPRINTF(("doing --(var)")); t1 = exprData_getUopNode (data); - cons = constraint_makeMaxSetSideEffectPostDecrement (t1, sequencePoint ); + cons = constraint_makeMaxSetSideEffectPostDecrement (t1, sequencePoint); e->ensuresConstraints = constraintList_add (e->ensuresConstraints, cons); } - else if (lltok_isMult( tok ) ) + else if (lltok_isMult(tok )) { if (definatelv) { @@ -1167,7 +1395,7 @@ void exprNode_exprTraverse (exprNode e, bool definatelv, bool definaterv, /*@ob } e->requiresConstraints = constraintList_add(e->requiresConstraints, cons); } - else if (lltok_isNot_Op (tok) ) + else if (lltok_isNot_Op (tok)) /* ! expr */ { constraintList_free(e->trueEnsuresConstraints); @@ -1177,137 +1405,136 @@ void exprNode_exprTraverse (exprNode e, bool definatelv, bool definaterv, /*@ob e->falseEnsuresConstraints = constraintList_copy (t1->trueEnsuresConstraints); } - else if (lltok_isAmpersand_Op (tok) ) + else if (lltok_isAmpersand_Op (tok)) { break; } - else if (lltok_isMinus_Op (tok) ) + else if (lltok_isMinus_Op (tok)) { break; } - else if ( lltok_isExcl_Op (tok) ) + else if (lltok_isExcl_Op (tok)) { break; } - else if (lltok_isTilde_Op (tok) ) + else if (lltok_isTilde_Op (tok)) { break; } else { - llcontbug((message("Unsupported preop in %s", exprNode_unparse(e) ) )); + llcontbug (message("Unsupported preop in %s", exprNode_unparse(e))); BADEXIT; } - break; - - case XPR_POSTOP: - - exprNode_exprTraverse (exprData_getUopNode (data), TRUE, definaterv, sequencePoint ); - - 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); - + break; - 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 */ + case XPR_POSTOP: + exprNode_exprTraverse (exprData_getUopNode (data), TRUE, + definaterv, sequencePoint); - 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); + 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); + + llassert (exprNode_isDefined (pred)); + llassert (exprNode_isDefined (trueBranch)); + llassert (exprNode_isDefined (falseBranch)); + + exprNode_exprTraverse (pred, FALSE, TRUE, sequencePoint); + + temp = pred->ensuresConstraints; + pred->ensuresConstraints = exprNode_traversEnsuresConstraints(pred); + constraintList_free(temp); + + temp = pred->requiresConstraints; + pred->requiresConstraints = exprNode_traversRequiresConstraints(pred); + constraintList_free(temp); + + temp = pred->trueEnsuresConstraints; + pred->trueEnsuresConstraints = exprNode_traversTrueEnsuresConstraints(pred); + constraintList_free(temp); + + temp = pred->falseEnsuresConstraints; + pred->falseEnsuresConstraints = exprNode_traversFalseEnsuresConstraints(pred); + constraintList_free(temp); + + exprNode_exprTraverse (trueBranch, FALSE, TRUE, sequencePoint); + + temp = trueBranch->ensuresConstraints; + trueBranch->ensuresConstraints = exprNode_traversEnsuresConstraints(trueBranch); + constraintList_free(temp); + + temp = trueBranch->requiresConstraints; + trueBranch->requiresConstraints = exprNode_traversRequiresConstraints(trueBranch); + constraintList_free(temp); + + + temp = trueBranch->trueEnsuresConstraints; + trueBranch->trueEnsuresConstraints = exprNode_traversTrueEnsuresConstraints(trueBranch); + constraintList_free(temp); + + temp = trueBranch->falseEnsuresConstraints; + trueBranch->falseEnsuresConstraints = exprNode_traversFalseEnsuresConstraints(trueBranch); + constraintList_free(temp); + + exprNode_exprTraverse (falseBranch, FALSE, TRUE, sequencePoint); + + temp = falseBranch->ensuresConstraints; + falseBranch->ensuresConstraints = exprNode_traversEnsuresConstraints(falseBranch); + constraintList_free(temp); + + + temp = falseBranch->requiresConstraints; + falseBranch->requiresConstraints = exprNode_traversRequiresConstraints(falseBranch); + constraintList_free(temp); + + temp = falseBranch->trueEnsuresConstraints; + falseBranch->trueEnsuresConstraints = exprNode_traversTrueEnsuresConstraints(falseBranch); + constraintList_free(temp); + + temp = falseBranch->falseEnsuresConstraints; + falseBranch->falseEnsuresConstraints = exprNode_traversFalseEnsuresConstraints(falseBranch); + constraintList_free(temp); + + /* if pred is true e equals true otherwise pred equals false */ + + cons = constraint_makeEnsureEqual (e, trueBranch, sequencePoint); + trueBranch->ensuresConstraints = constraintList_add(trueBranch->ensuresConstraints, cons); + + cons = constraint_makeEnsureEqual (e, trueBranch, sequencePoint); + falseBranch->ensuresConstraints = constraintList_add(falseBranch->ensuresConstraints, cons); + + e = doIfElse (e, pred, trueBranch, falseBranch); } break; case XPR_COMMA: @@ -1317,8 +1544,8 @@ void exprNode_exprTraverse (exprNode e, bool definatelv, bool definaterv, /*@ob /* we essiantially treat this like expr1; expr2 of course sequencePoint isn't adjusted so this isn't completely accurate problems../ */ - exprNode_exprTraverse (t1, FALSE, FALSE, sequencePoint ); - exprNode_exprTraverse (t2, definatelv, definaterv, sequencePoint ); + exprNode_exprTraverse (t1, FALSE, FALSE, sequencePoint); + exprNode_exprTraverse (t2, definatelv, definaterv, sequencePoint); exprNode_mergeResolve (e, t1, t2); break; @@ -1326,21 +1553,24 @@ void exprNode_exprTraverse (exprNode e, bool definatelv, bool definaterv, /*@ob handledExprNode = FALSE; } - e->requiresConstraints = constraintList_preserveOrig ( e->requiresConstraints); - e->ensuresConstraints = constraintList_preserveOrig ( e->ensuresConstraints); - e->requiresConstraints = constraintList_addGeneratingExpr ( e->requiresConstraints, e); + e->requiresConstraints = constraintList_preserveOrig (e->requiresConstraints); + e->ensuresConstraints = constraintList_preserveOrig (e->ensuresConstraints); + e->requiresConstraints = constraintList_addGeneratingExpr (e->requiresConstraints, e); - e->ensuresConstraints = constraintList_addGeneratingExpr ( e->ensuresConstraints, e); + e->ensuresConstraints = constraintList_addGeneratingExpr (e->ensuresConstraints, e); - 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) ) )); + e->requiresConstraints = constraintList_removeSurpressed(e->requiresConstraints); + + 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 ("trueEnsures constraints for %s are %s", exprNode_unparse(e), constraintList_printDetailed(e->trueEnsuresConstraints)))); - DPRINTF((message ("falseEnsures constraints for %s are %s", exprNode_unparse(e), constraintList_printDetailed(e->falseEnsuresConstraints) ) )); + DPRINTF((message ("falseEnsures constraints for %s are %s", exprNode_unparse(e), constraintList_printDetailed(e->falseEnsuresConstraints)))); - return; // handledExprNode; + return; } @@ -1349,18 +1579,18 @@ 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 ); + if (exprNode_handleError (e)) + { + ret = constraintList_makeNew(); + return ret; + } + + ret = constraintList_copy (e->trueEnsuresConstraints); - handledExprNode = TRUE; + handledExprNode = TRUE; data = e->edata; @@ -1368,111 +1598,111 @@ constraintList exprNode_traversTrueEnsuresConstraints (exprNode e) { case XPR_WHILEPRED: t1 = exprData_getSingle (data); - ret = constraintList_addListFree ( ret, exprNode_traversTrueEnsuresConstraints (t1) ); + ret = constraintList_addListFree (ret, exprNode_traversTrueEnsuresConstraints (t1)); break; case XPR_FETCH: ret = constraintList_addListFree (ret, exprNode_traversTrueEnsuresConstraints - (exprData_getPairA (data) ) ); + (exprData_getPairA (data))); ret = constraintList_addListFree (ret, exprNode_traversTrueEnsuresConstraints - (exprData_getPairB (data) ) ); + (exprData_getPairB (data))); break; case XPR_PREOP: ret = constraintList_addListFree (ret, exprNode_traversTrueEnsuresConstraints - (exprData_getUopNode (data) ) ); + (exprData_getUopNode (data))); break; case XPR_PARENS: ret = constraintList_addListFree (ret, exprNode_traversTrueEnsuresConstraints - (exprData_getUopNode (data) ) ); + (exprData_getUopNode (data))); break; + + case XPR_INIT: + ret = constraintList_addListFree (ret, + exprNode_traversTrueEnsuresConstraints + (exprData_getInitNode (data))); + break; + + case XPR_ASSIGN: ret = constraintList_addListFree (ret, exprNode_traversTrueEnsuresConstraints - (exprData_getOpA (data) ) ); + (exprData_getOpA (data))); ret = constraintList_addListFree (ret, exprNode_traversTrueEnsuresConstraints - (exprData_getOpB (data) ) ); + (exprData_getOpB (data))); break; case XPR_OP: ret = constraintList_addListFree (ret, exprNode_traversTrueEnsuresConstraints - (exprData_getOpA (data) ) ); + (exprData_getOpA (data))); ret = constraintList_addListFree (ret, exprNode_traversTrueEnsuresConstraints - (exprData_getOpB (data) ) ); + (exprData_getOpB (data))); break; case XPR_SIZEOFT: - - // ctype_unparse (qtype_getType (exprData_getType (data) ) ); - break; case XPR_SIZEOF: ret = constraintList_addListFree (ret, exprNode_traversTrueEnsuresConstraints - (exprData_getSingle (data) ) ); + (exprData_getSingle (data))); break; case XPR_CALL: ret = constraintList_addListFree (ret, exprNode_traversTrueEnsuresConstraints - (exprData_getFcn (data) ) ); - /*@i11*/ // exprNodeList_unparse (exprData_getArgs (data) ); - break; + (exprData_getFcn (data))); + /*@i11*/ /* exprNodeList_unparse (exprData_getArgs (data)); */ + break; case XPR_RETURN: ret = constraintList_addListFree (ret, exprNode_traversTrueEnsuresConstraints - (exprData_getSingle (data) ) ); + (exprData_getSingle (data))); break; case XPR_NULLRETURN: - // cstring_makeLiteral ("return");; break; case XPR_FACCESS: - ret = constraintList_addListFree (ret, - exprNode_traversTrueEnsuresConstraints - (exprData_getFieldNode (data) ) ); - //exprData_getFieldName (data) ; + ret = constraintList_addListFree (ret, + exprNode_traversTrueEnsuresConstraints + (exprData_getFieldNode (data))); break; case XPR_ARROW: - ret = constraintList_addListFree (ret, - exprNode_traversTrueEnsuresConstraints - (exprData_getFieldNode (data) ) ); - // exprData_getFieldName (data); + ret = constraintList_addListFree (ret, + exprNode_traversTrueEnsuresConstraints + (exprData_getFieldNode (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) ) ); + (exprData_getUopNode (data))); break; case XPR_CAST: ret = constraintList_addListFree (ret, exprNode_traversTrueEnsuresConstraints - (exprData_getCastNode (data) ) ); + (exprData_getCastNode (data))); break; default: @@ -1484,133 +1714,128 @@ constraintList exprNode_traversTrueEnsuresConstraints (exprNode e) constraintList exprNode_traversFalseEnsuresConstraints (exprNode e) { - exprNode t1; - + 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; - + + if (exprNode_handleError (e)) + { + ret = constraintList_makeNew(); + return ret; + } + + ret = constraintList_copy (e->falseEnsuresConstraints); + handledExprNode = TRUE; data = e->edata; switch (e->kind) { case XPR_WHILEPRED: t1 = exprData_getSingle (data); - ret = constraintList_addListFree ( ret,exprNode_traversFalseEnsuresConstraints (t1) ); + ret = constraintList_addListFree (ret,exprNode_traversFalseEnsuresConstraints (t1)); break; case XPR_FETCH: ret = constraintList_addListFree (ret, exprNode_traversFalseEnsuresConstraints - (exprData_getPairA (data) ) ); + (exprData_getPairA (data))); ret = constraintList_addListFree (ret, exprNode_traversFalseEnsuresConstraints - (exprData_getPairB (data) ) ); + (exprData_getPairB (data))); break; case XPR_PREOP: ret = constraintList_addListFree (ret, exprNode_traversFalseEnsuresConstraints - (exprData_getUopNode (data) ) ); + (exprData_getUopNode (data))); break; case XPR_PARENS: ret = constraintList_addListFree (ret, exprNode_traversFalseEnsuresConstraints - (exprData_getUopNode (data) ) ); + (exprData_getUopNode (data))); break; + case XPR_INIT: + ret = constraintList_addListFree (ret, + exprNode_traversFalseEnsuresConstraints + ( exprData_getInitNode (data))); + break; + case XPR_ASSIGN: ret = constraintList_addListFree (ret, exprNode_traversFalseEnsuresConstraints - (exprData_getOpA (data) ) ); + (exprData_getOpA (data))); ret = constraintList_addListFree (ret, exprNode_traversFalseEnsuresConstraints - (exprData_getOpB (data) ) ); + (exprData_getOpB (data))); break; case XPR_OP: ret = constraintList_addListFree (ret, exprNode_traversFalseEnsuresConstraints - (exprData_getOpA (data) ) ); + (exprData_getOpA (data))); ret = constraintList_addListFree (ret, exprNode_traversFalseEnsuresConstraints - (exprData_getOpB (data) ) ); + (exprData_getOpB (data))); break; case XPR_SIZEOFT: - - // ctype_unparse (qtype_getType (exprData_getType (data) ) ); - break; case XPR_SIZEOF: ret = constraintList_addListFree (ret, exprNode_traversFalseEnsuresConstraints - (exprData_getSingle (data) ) ); + (exprData_getSingle (data))); break; case XPR_CALL: ret = constraintList_addListFree (ret, exprNode_traversFalseEnsuresConstraints - (exprData_getFcn (data) ) ); - /*@i11*/ // exprNodeList_unparse (exprData_getArgs (data) ); - break; + (exprData_getFcn (data))); + /*@i11*/ /* exprNodeList_unparse (exprData_getArgs (data)); */ + break; case XPR_RETURN: ret = constraintList_addListFree (ret, exprNode_traversFalseEnsuresConstraints - (exprData_getSingle (data) ) ); + (exprData_getSingle (data))); break; case XPR_NULLRETURN: - // cstring_makeLiteral ("return");; break; case XPR_FACCESS: - ret = constraintList_addListFree (ret, - exprNode_traversFalseEnsuresConstraints - (exprData_getFieldNode (data) ) ); - //exprData_getFieldName (data) ; + ret = constraintList_addListFree (ret, + exprNode_traversFalseEnsuresConstraints + (exprData_getFieldNode (data))); break; - + case XPR_ARROW: - ret = constraintList_addListFree (ret, - exprNode_traversFalseEnsuresConstraints - (exprData_getFieldNode (data) ) ); - // exprData_getFieldName (data); + ret = constraintList_addListFree (ret, + exprNode_traversFalseEnsuresConstraints + (exprData_getFieldNode (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) ) ); + (exprData_getUopNode (data))); break; case XPR_CAST: ret = constraintList_addListFree (ret, exprNode_traversFalseEnsuresConstraints - (exprData_getCastNode (data) ) ); + (exprData_getCastNode (data))); break; default: @@ -1627,7 +1852,6 @@ constraintList exprNode_traversFalseEnsuresConstraints (exprNode e) exprNode t1; bool handledExprNode; - // char * mes; exprData data; constraintList ret; @@ -1636,121 +1860,118 @@ constraintList exprNode_traversFalseEnsuresConstraints (exprNode e) ret = constraintList_makeNew(); return ret; } - ret = constraintList_copy (e->requiresConstraints ); - - handledExprNode = TRUE; - + + ret = constraintList_copy (e->requiresConstraints); + handledExprNode = TRUE; data = e->edata; switch (e->kind) { case XPR_WHILEPRED: t1 = exprData_getSingle (data); - ret = constraintList_addListFree ( ret, exprNode_traversRequiresConstraints (t1) ); + ret = constraintList_addListFree (ret, exprNode_traversRequiresConstraints (t1)); break; case XPR_FETCH: ret = constraintList_addListFree (ret, exprNode_traversRequiresConstraints - (exprData_getPairA (data) ) ); + (exprData_getPairA (data))); ret = constraintList_addListFree (ret, exprNode_traversRequiresConstraints - (exprData_getPairB (data) ) ); + (exprData_getPairB (data))); break; case XPR_PREOP: ret = constraintList_addListFree (ret, exprNode_traversRequiresConstraints - (exprData_getUopNode (data) ) ); + (exprData_getUopNode (data))); break; case XPR_PARENS: ret = constraintList_addListFree (ret, exprNode_traversRequiresConstraints - (exprData_getUopNode (data) ) ); + (exprData_getUopNode (data))); break; + case XPR_INIT: + ret = constraintList_addListFree (ret, + exprNode_traversRequiresConstraints + (exprData_getInitNode (data))); + break; + case XPR_ASSIGN: ret = constraintList_addListFree (ret, exprNode_traversRequiresConstraints - (exprData_getOpA (data) ) ); + (exprData_getOpA (data))); ret = constraintList_addListFree (ret, exprNode_traversRequiresConstraints - (exprData_getOpB (data) ) ); + (exprData_getOpB (data))); break; case XPR_OP: ret = constraintList_addListFree (ret, exprNode_traversRequiresConstraints - (exprData_getOpA (data) ) ); + (exprData_getOpA (data))); ret = constraintList_addListFree (ret, exprNode_traversRequiresConstraints - (exprData_getOpB (data) ) ); + (exprData_getOpB (data))); break; case XPR_SIZEOFT: - - // ctype_unparse (qtype_getType (exprData_getType (data) ) ); - break; case XPR_SIZEOF: ret = constraintList_addListFree (ret, exprNode_traversRequiresConstraints - (exprData_getSingle (data) ) ); + (exprData_getSingle (data))); break; case XPR_CALL: ret = constraintList_addListFree (ret, exprNode_traversRequiresConstraints - (exprData_getFcn (data) ) ); - /*@i11*/ // exprNodeList_unparse (exprData_getArgs (data) ); - break; + (exprData_getFcn (data))); + /*@i11*/ /* exprNodeList_unparse (exprData_getArgs (data)); */ + break; case XPR_RETURN: ret = constraintList_addListFree (ret, exprNode_traversRequiresConstraints - (exprData_getSingle (data) ) ); + (exprData_getSingle (data))); break; case XPR_NULLRETURN: - // cstring_makeLiteral ("return");; break; case XPR_FACCESS: - ret = constraintList_addListFree (ret, - exprNode_traversRequiresConstraints - (exprData_getFieldNode (data) ) ); - //exprData_getFieldName (data) ; + ret = constraintList_addListFree (ret, + exprNode_traversRequiresConstraints + (exprData_getFieldNode (data))); break; - + case XPR_ARROW: - ret = constraintList_addListFree (ret, - exprNode_traversRequiresConstraints - (exprData_getFieldNode (data) ) ); - // exprData_getFieldName (data); + ret = constraintList_addListFree (ret, + exprNode_traversRequiresConstraints + (exprData_getFieldNode (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) ) ); + (exprData_getUopNode (data))); break; case XPR_CAST: ret = constraintList_addListFree (ret, exprNode_traversRequiresConstraints - (exprData_getCastNode (data) ) ); + (exprData_getCastNode (data))); break; default: @@ -1767,26 +1988,22 @@ constraintList exprNode_traversFalseEnsuresConstraints (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; - + if (exprNode_handleError (e)) + { + ret = constraintList_makeNew(); + return ret; + } + + ret = constraintList_copy (e->ensuresConstraints); + handledExprNode = TRUE; + data = e->edata; - - DPRINTF( (message ( - "exprnode_traversEnsuresConstraints call for %s with constraintList of %s", + + DPRINTF ((message ("exprnode_traversEnsuresConstraints call for %s with " + "constraintList of %s", exprNode_unparse (e), constraintList_print(e->ensuresConstraints) ) @@ -1795,131 +2012,116 @@ constraintList exprNode_traversFalseEnsuresConstraints (exprNode e) switch (e->kind) { - case XPR_WHILEPRED: + case XPR_WHILEPRED: t1 = exprData_getSingle (data); - ret = constraintList_addListFree ( ret,exprNode_traversEnsuresConstraints (t1) ); + ret = constraintList_addListFree (ret,exprNode_traversEnsuresConstraints (t1)); break; case XPR_FETCH: - ret = constraintList_addListFree (ret, - exprNode_traversEnsuresConstraints - (exprData_getPairA (data) ) ); - + exprNode_traversEnsuresConstraints + (exprData_getPairA (data))); + ret = constraintList_addListFree (ret, - exprNode_traversEnsuresConstraints - (exprData_getPairB (data) ) ); + exprNode_traversEnsuresConstraints + (exprData_getPairB (data))); break; case XPR_PREOP: - ret = constraintList_addListFree (ret, - exprNode_traversEnsuresConstraints - (exprData_getUopNode (data) ) ); + exprNode_traversEnsuresConstraints + (exprData_getUopNode (data))); break; case XPR_PARENS: ret = constraintList_addListFree (ret, exprNode_traversEnsuresConstraints - (exprData_getUopNode (data) ) ); + (exprData_getUopNode (data))); + break; + + case XPR_INIT: + ret = constraintList_addListFree (ret, + exprNode_traversEnsuresConstraints + (exprData_getInitNode (data))); break; + + 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: + ret = constraintList_addListFree (ret, + exprNode_traversEnsuresConstraints + (exprData_getOpA (data))); - // ctype_unparse (qtype_getType (exprData_getType (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: break; case XPR_SIZEOF: - - ret = constraintList_addListFree (ret, - exprNode_traversEnsuresConstraints - (exprData_getSingle (data) ) ); - break; - + ret = constraintList_addListFree (ret, + exprNode_traversEnsuresConstraints + (exprData_getSingle (data))); + break; case XPR_CALL: ret = constraintList_addListFree (ret, - exprNode_traversEnsuresConstraints - (exprData_getFcn (data) ) ); - /*@i11*/ // exprNodeList_unparse (exprData_getArgs (data) ); - break; - + exprNode_traversEnsuresConstraints + (exprData_getFcn (data))); + /*@i11*/ /* exprNodeList_unparse (exprData_getArgs (data)); */ + break; case XPR_RETURN: ret = constraintList_addListFree (ret, - exprNode_traversEnsuresConstraints - (exprData_getSingle (data) ) ); + exprNode_traversEnsuresConstraints + (exprData_getSingle (data))); break; - case XPR_NULLRETURN: - // cstring_makeLiteral ("return");; break; - case XPR_FACCESS: - ret = constraintList_addListFree (ret, - exprNode_traversEnsuresConstraints - (exprData_getFieldNode (data) ) ); - //exprData_getFieldName (data) ; + ret = constraintList_addListFree (ret, + exprNode_traversEnsuresConstraints + (exprData_getFieldNode (data))); break; - case XPR_ARROW: - ret = constraintList_addListFree (ret, - exprNode_traversEnsuresConstraints - (exprData_getFieldNode (data) ) ); - // exprData_getFieldName (data); + ret = constraintList_addListFree (ret, + exprNode_traversEnsuresConstraints + (exprData_getFieldNode (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; + ret = constraintList_addListFree (ret, + exprNode_traversEnsuresConstraints + (exprData_getUopNode (data))); + break; case XPR_CAST: - ret = constraintList_addListFree (ret, - exprNode_traversEnsuresConstraints - (exprData_getCastNode (data) ) ); + exprNode_traversEnsuresConstraints + (exprData_getCastNode (data))); break; - default: break; } -DPRINTF( (message ( - "exprnode_traversEnsuresConstraints call for %s with constraintList of is returning %s", - exprNode_unparse (e), - // constraintList_print(e->ensuresConstraints), - constraintList_print(ret) - ) - )); - + DPRINTF((message ("exprnode_traversEnsuresConstraints call for %s with " + "constraintList of is returning %s", + exprNode_unparse (e), + constraintList_print(ret)))); + return ret; } /*drl moved out of constraintResolve.c 07-02-001 */ -void checkArgumentList (/*@out@*/ exprNode temp, exprNodeList arglist, fileloc sequencePoint) +void checkArgumentList (/*@out@*/ exprNode temp, exprNodeList arglist, + fileloc sequencePoint) { temp->requiresConstraints = constraintList_makeNew(); temp->ensuresConstraints = constraintList_makeNew(); @@ -1953,13 +2155,13 @@ constraintList exprNode_getPostConditions (exprNode fcn, exprNodeList arglist, e { constraintList postconditions; uentry temp; - DPRINTF( (message ("Got call that %s ( %s) ", exprNode_unparse(fcn), exprNodeList_unparse (arglist ) ) ) ); + DPRINTF((message ("Got call that %s (%s) ", exprNode_unparse(fcn), exprNodeList_unparse (arglist)))); temp = exprNode_getUentry (fcn); postconditions = uentry_getFcnPostconditions (temp); - if (constraintList_isDefined(postconditions) ) + if (constraintList_isDefined (postconditions)) { postconditions = constraintList_doSRefFixConstraintParam (postconditions, arglist); postconditions = constraintList_doFixResult (postconditions, fcnCall); @@ -1972,19 +2174,63 @@ constraintList exprNode_getPostConditions (exprNode fcn, exprNodeList arglist, e return postconditions; } +/* +comment this out for now +we'll include it in a production release when its stable... + + void findStructs (exprNodeList arglist) +{ + + ctype ct, rt; + + DPRINTF(( + message("doing findStructs: %s", exprNodeList_unparse(arglist)) + )); + + + exprNodeList_elements(arglist, expr) + { + ct = exprNode_getType(expr); + + rt = ctype_realType (ct); + + if (ctype_isStruct (rt)) + TPRINTF((message("Found structure %s", exprNode_unparse(expr)) + )); + if (hasInvariants(ct)) + { + constraintList invars; + + invars = getInvariants(ct); + + + TPRINTF((message ("findStructs has invariants %s ", constraintList_print (invars)) + )); + + invars = constraintList_doSRefFixStructConstraint(invars, exprNode_getSref(expr), ct); + + + TPRINTF((message ("findStructs finded invariants to be %s ", constraintList_print (invars)) + )); + } + } + end_exprNodeList_elements; +} + +*/ /*drl moved out of constraintResolve.c 07-02-001 */ constraintList checkCall (/*@dependent@*/ exprNode fcn, exprNodeList arglist) { constraintList preconditions; uentry temp; - DPRINTF( (message ("Got call that %s ( %s) ", exprNode_unparse(fcn), exprNodeList_unparse (arglist ) ) ) ); + DPRINTF((message ("Got call that %s (%s) ", exprNode_unparse(fcn), exprNodeList_unparse (arglist)))); temp = exprNode_getUentry (fcn); preconditions = uentry_getFcnPreconditions (temp); - if (constraintList_isDefined(preconditions) ) + if (constraintList_isDefined(preconditions)) { preconditions = constraintList_togglePost (preconditions); preconditions = constraintList_preserveCallInfo(preconditions, fcn); @@ -1992,10 +2238,124 @@ constraintList checkCall (/*@dependent@*/ exprNode fcn, exprNodeList arglist) } else { - if (constraintList_isUndefined(preconditions) ) + if (constraintList_isUndefined(preconditions)) preconditions = constraintList_makeNew(); } - DPRINTF (( message("Done checkCall\n") )); - DPRINTF (( message("Returning list %q ", constraintList_printDetailed(preconditions) ) )); + + // drl remember to remove this code before you make a pslint release. + /* + if (context_getFlag (FLG_IMPLICTCONSTRAINT) ) + { + + uentryList_elements (params, el) + { + DPRINTF((message("setImplictfcnConstraints doing: %s", uentry_unparse(el) ) )); + + s = uentry_getSref(el); + if (sRef_isReference (s) ) + { + DPRINTF((message ("%s is a pointer", sRef_unparse(s) ) )); + } + else + { + DPRINTF((message ("%s is NOT a pointer", sRef_unparse(s) ) )); + } + //drl 4/26/01 + //chagned this from MaxSet(s) == 0 to MaxSet(s) >= 0 + c = constraint_makeSRefWriteSafeInt (s, 0); + + implicitFcnConstraints = constraintList_add(implicitFcnConstraints , c); + + //drl 10/23/2002 added support for out + if (!uentry_isOut(el) ) + { + c = constraint_makeSRefReadSafeInt (s, 0); + + implicitFcnConstraints = constraintList_add(implicitFcnConstraints , c); + } + + + } + + } + */ + DPRINTF ((message("Done checkCall\n"))); + DPRINTF ((message("Returning list %q ", constraintList_printDetailed(preconditions)))); + + /* + drl we're going to comment this out for now + we'll include it if we're sure it's working + + findStructs(arglist); + */ + return preconditions; } + +/*drl added this function 10.29.001 + takes an exprNode of the form const + const + and sets the value +*/ +/*drl + I'm a bit nervous about modifying the exprNode + but this is the easy way to do this + If I have time I'd like to cause the exprNode to get created correctly in the first place */ +/*@i223*/ +void exprNode_findValue(exprNode e) +{ + exprData data; + + exprNode t1, t2; + lltok tok; + + data = e->edata; + + if (exprNode_hasValue(e)) + return; + + if (e->kind == XPR_OP) + { + t1 = exprData_getOpA (data); + t2 = exprData_getOpB (data); + tok = exprData_getOpTok (data); + + exprNode_findValue(t1); + exprNode_findValue(t2); + + if (!(exprNode_knownIntValue(t1) && (exprNode_knownIntValue(t2)))) + return; + + if (lltok_isPlus_Op (tok)) + { + long v1, v2; + + v1 = exprNode_getLongValue(t1); + v2 = exprNode_getLongValue(t2); + + if (multiVal_isDefined(e->val)) + multiVal_free (e->val); + + e->val = multiVal_makeInt (v1 + v2); + } + + if (lltok_isMinus_Op (tok)) + { + long v1, v2; + + v1 = exprNode_getLongValue(t1); + v2 = exprNode_getLongValue(t2); + + if (multiVal_isDefined(e->val)) + { + multiVal_free (e->val); + } + + e->val = multiVal_makeInt (v1 - v2); + } + + /*drl I should really do * and / at some point */ + + } + +} +