/*
** Splint - annotation-assisted static program checker
-** Copyright (C) 1994-2002 University of Virginia,
+** Copyright (C) 1994-2003 University of Virginia,
** Massachusetts Institute of Technology
**
** This program is free software; you can redistribute it and/or modify it
** the Free Software Foundation, Inc., 59 Temple Place - Suite 330, Boston,
** MA 02111-1307, USA.
**
-** For information on splint: splint@cs.virginia.edu
-** To report a bug: splint-bug@cs.virginia.edu
+** For information on splint: info@splint.org
+** To report a bug: splint-bug@splint.org
** For more information: http://www.splint.org
*/
# include "exprChecks.h"
# include "exprNodeSList.h"
-/*@access exprNode @*/
-
+/*drl We need to access the internal representation of exprNode
+ because these functions walk down the parse tree and need a richer
+information than is accessible through the exprNode interface.*/
+
+/*@access exprNode@*/
-static bool exprNode_handleError(/*@dependent@*/ exprNode p_e);
+static /*@nullwhentrue@*/ bool exprNode_handleError (/*@temp@*/ 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 constraintList exprNode_traversTrueEnsuresConstraints (/*@dependent@*/ exprNode p_e);
-static constraintList exprNode_traversFalseEnsuresConstraints (/*@dependent@*/ exprNode p_e);
+static constraintList exprNode_traverseTrueEnsuresConstraints (/*@temp@*/ exprNode p_e);
+static constraintList exprNode_traverseFalseEnsuresConstraints (/*@temp@*/ exprNode p_e);
static void checkArgumentList (/*@out@*/ exprNode p_temp, exprNodeList p_arglist, fileloc p_sequencePoint) /*@modifies p_temp @*/;
-static constraintList checkCall (/*@dependent@*/ exprNode p_fcn, exprNodeList p_arglist);
+static constraintList checkCall (/*@temp@*/ exprNode p_fcn, exprNodeList p_arglist);
-static bool exprNode_isUnhandled (/*@dependent@*/ /*@observer@*/ exprNode e)
+static bool exprNode_isUnhandled (/*@temp@*/ /*@observer@*/ exprNode e)
{
- llassert( exprNode_isDefined(e) );
+ llassert(exprNode_isDefined(e));
switch (e->kind)
{
case XPR_INITBLOCK:
case XPR_FTCASE:
case XPR_CASE:
case XPR_NODE:
- DPRINTF((message ("Warning current constraint generation does not handle expression %s", exprNode_unparse(e)) ) );
+ DPRINTF((message ("Warning current constraint generation does not handle expression %s", exprNode_unparse(e))));
return TRUE;
/*@notreached@*/
break;
return FALSE;
}
-bool exprNode_handleError( exprNode e)
+/*@nullwhentrue@*/ 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 ("<error>");
- }
-
- /*@-unqualifiedtrans*/ return TRUE; /*@=unqualifiedtrans*/
+ return TRUE;
}
+
return FALSE;
}
-bool /*@alt void@*/ exprNode_generateConstraints (/*@dependent@*/ exprNode e)
+/* evans 2002-03-2 - parameter was dependent */
+bool /*@alt void@*/ exprNode_generateConstraints (/*@temp@*/ exprNode e)
{
- if (exprNode_isError (e) )
+ if (exprNode_isError (e))
return FALSE;
- if (exprNode_isUnhandled (e) )
+ if (exprNode_isUnhandled (e))
{
- DPRINTF((message("Warning ignoring %s", exprNode_unparse (e) ) ) );
- return FALSE;
+ DPRINTF((message("Warning ignoring %s", exprNode_unparse (e))));
+ return FALSE;
}
- DPRINTF((message ("exprNode_generateConstraints Analysising %s at %s", exprNode_unparse( e),
- fileloc_unparse(exprNode_getfileloc(e) ) ) ) );
-
- if (exprNode_isMultiStatement ( e) )
+ DPRINTF ((message ("exprNode_generateConstraints Analyzing %s at %s", exprNode_unparse(e),
+ fileloc_unparse(exprNode_loc (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;
+
}
{
constraintList c;
-
+
c = constraintList_makeFixedArrayConstraints (e->uses);
e->requiresConstraints = constraintList_reflectChangesFreePre (e->requiresConstraints, c);
constraintList_free(c);
}
-
- DPRINTF ((message ("e->requiresConstraints %s", constraintList_printDetailed (e->requiresConstraints) ) ) );
- return FALSE;
-}
-
-
-/* handles multiple statements */
-
-bool exprNode_isMultiStatement(exprNode e)
-{
-if (exprNode_handleError (e) != NULL)
+
+ DPRINTF ((message ("e->requiresConstraints %s",
+ constraintList_unparseDetailed (e->requiresConstraints))));
return FALSE;
-
- switch (e->kind)
- {
- case XPR_FOR:
- case XPR_FORPRED:
- case XPR_IF:
- case XPR_IFELSE:
- case XPR_WHILE:
- case XPR_WHILEPRED:
- case XPR_DOWHILE:
- case XPR_BLOCK:
- case XPR_STMT:
- case XPR_STMTLIST:
- case XPR_SWITCH:
- return TRUE;
- default:
- return FALSE;
- }
-
}
-static void exprNode_stmt ( /*@dependent@*/ /*@temp@*/ exprNode e)
+static void exprNode_stmt (/*@temp@*/ exprNode e)
{
exprNode snode;
fileloc loc;
- cstring s;
- if (exprNode_isError(e) )
+ DPRINTF (("Generating constraint for: %s", exprNode_unparse (e)));
+
+ if (exprNode_isError(e))
{
return;
}
/*e->requiresConstraints = constraintList_makeNew();
e->ensuresConstraints = constraintList_makeNew(); */
-
- DPRINTF(( "expNode_stmt: STMT:") );
- s = exprNode_unparse(e);
- DPRINTF (( message("exprNode_stmt: STMT: %s ", s) ) );
+
+ /*!! s = exprNode_unparse (e); */
if (e->kind == XPR_INIT)
{
constraintList tempList;
- DPRINTF (("Init") );
- DPRINTF ((message ("%s ", exprNode_unparse (e)) ) );
- loc = exprNode_getNextSequencePoint(e); /* reduces to an expression */
+ DPRINTF (("Init: %s ", exprNode_unparse (e)));
+ loc = exprNode_getNextSequencePoint (e); /* reduces to an expression */
+ DPRINTF (("Location: %s", fileloc_unparse (loc)));
+ DPRINTF (("Ensures before: %s", constraintList_unparse (e->ensuresConstraints)));
exprNode_exprTraverse (e, FALSE, FALSE, loc);
+ DPRINTF (("Ensures after: %s", constraintList_unparse (e->ensuresConstraints)));
+ DPRINTF (("After traversing..."));
fileloc_free(loc);
-
+
tempList = e->requiresConstraints;
- e->requiresConstraints = exprNode_traversRequiresConstraints(e);
+ DPRINTF (("Requires before: %s", constraintList_unparse (e->requiresConstraints)));
+ e->requiresConstraints = exprNode_traverseRequiresConstraints (e);
+ DPRINTF (("Requires after: %s", constraintList_unparse (e->requiresConstraints)));
constraintList_free(tempList);
tempList = e->ensuresConstraints;
- e->ensuresConstraints = exprNode_traversEnsuresConstraints(e);
+ DPRINTF (("Ensures before: %s", constraintList_unparse (e->ensuresConstraints)));
+ e->ensuresConstraints = exprNode_traverseEnsuresConstraints(e);
+ DPRINTF (("Ensures before: %s", constraintList_unparse (e->ensuresConstraints)));
constraintList_free(tempList);
return;
}
+
+ /*drl 2/13/002 patched bug so return statement will be checked*/
+ /*return is a stmt not not expression ...*/
+ if (e->kind == XPR_RETURN)
+ {
+ constraintList tempList;
+
+ loc = exprNode_getNextSequencePoint(e); /* reduces to an expression */
+
+ exprNode_exprTraverse (exprData_getSingle (e->edata), FALSE, TRUE, loc);
+ fileloc_free(loc);
+
+ tempList = e->requiresConstraints;
+ e->requiresConstraints = exprNode_traverseRequiresConstraints(e);
+ constraintList_free(tempList);
+ }
if (e->kind != XPR_STMT)
{
-
- DPRINTF (("Not Stmt") );
- DPRINTF ((message ("%s ", exprNode_unparse (e)) ) );
+ DPRINTF (("Not Stmt"));
+ DPRINTF ((message ("%s ", exprNode_unparse (e))));
if (exprNode_isMultiStatement (e))
{
exprNode_multiStatement (e); /* evans 2001-08-21: spurious return removed */
}
-
- DPRINTF((message ("Ignoring non-statement %s", exprNode_unparse(e) ) ) );
- return;
+ else
+ {
+ loc = exprNode_getNextSequencePoint(e); /* reduces to an expression */
+
+ exprNode_exprTraverse (e, FALSE, TRUE, loc);
+ fileloc_free(loc);
+
+ }
+ return;
}
- DPRINTF (("Stmt") );
- DPRINTF ((message ("%s ", exprNode_unparse (e)) ) );
+ DPRINTF (("Stmt"));
+ DPRINTF ((message ("%s ", exprNode_unparse (e))));
snode = exprData_getUopNode (e->edata);
fileloc_free(loc);
constraintList_free (e->requiresConstraints);
- e->requiresConstraints = exprNode_traversRequiresConstraints(snode);
+ e->requiresConstraints = exprNode_traverseRequiresConstraints(snode);
constraintList_free (e->ensuresConstraints);
- e->ensuresConstraints = exprNode_traversEnsuresConstraints(snode);
-
+ e->ensuresConstraints = exprNode_traverseEnsuresConstraints(snode);
+
DPRINTF ((message ("smtlist constraints are: pre: %s \n and \t post %s\n",
- constraintList_print(e->requiresConstraints),
- constraintList_print(e->ensuresConstraints) ) ) );
+ constraintList_unparse(e->requiresConstraints),
+ constraintList_unparse(e->ensuresConstraints))));
return;
}
static void exprNode_stmtList (/*@dependent@*/ exprNode e)
{
exprNode stmt1, stmt2;
- if (exprNode_isError (e) )
+ if (exprNode_isError (e))
{
return;
}
return;
}
llassert (e->kind == XPR_STMTLIST);
- DPRINTF(( "exprNode_stmtList STMTLIST:") );
- DPRINTF ((cstring_toCharsSafe (exprNode_unparse(e)) ) );
+ DPRINTF(("exprNode_stmtList STMTLIST:"));
+ DPRINTF ((cstring_toCharsSafe (exprNode_unparse(e))));
stmt1 = exprData_getPairA (e->edata);
stmt2 = exprData_getPairB (e->edata);
- DPRINTF(("exprNode_stmtlist ") );
- DPRINTF ((message("XW%s | %s", exprNode_unparse(stmt1), exprNode_unparse(stmt2) ) ) );
+ DPRINTF(("exprNode_stmtlist "));
+ DPRINTF ((message("XW%s | %s", exprNode_unparse(stmt1), exprNode_unparse(stmt2))));
exprNode_stmt (stmt1);
- DPRINTF(("\nstmt after stmtList call " ));
+ DPRINTF(("\nstmt after stmtList call "));
exprNode_stmt (stmt2);
- exprNode_mergeResolve (e, stmt1, stmt2 );
+ exprNode_mergeResolve (e, stmt1, stmt2);
DPRINTF ((message ("smtlist constraints are: pre: %s \n and \t post %s\n",
- constraintList_print(e->requiresConstraints),
- constraintList_print(e->ensuresConstraints) ) ) );
+ constraintList_unparse(e->requiresConstraints),
+ constraintList_unparse(e->ensuresConstraints))));
return;
}
{
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_unparseDetailed(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_unparseDetailed(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_unparseDetailed(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_unparseDetailed(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_unparseDetailed(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_unparseDetailed(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_unparseDetailed(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_unparseDetailed(test->falseEnsuresConstraints))));
temp = test->trueEnsuresConstraints;
- test->trueEnsuresConstraints = exprNode_traversTrueEnsuresConstraints(test);
+ test->trueEnsuresConstraints = exprNode_traverseTrueEnsuresConstraints(test);
constraintList_free(temp);
temp = test->ensuresConstraints;
- test->ensuresConstraints = exprNode_traversEnsuresConstraints (test);
+ test->ensuresConstraints = exprNode_traverseEnsuresConstraints (test);
constraintList_free(temp);
temp = test->requiresConstraints;
- test->requiresConstraints = exprNode_traversRequiresConstraints (test);
+ test->requiresConstraints = exprNode_traverseRequiresConstraints (test);
constraintList_free(temp);
test->trueEnsuresConstraints = constraintList_substituteFreeTarget(test->trueEnsuresConstraints, test->ensuresConstraints);
- DPRINTF ((message ("doIf: test ensures %s ", constraintList_print(test->ensuresConstraints) ) ) );
+ DPRINTF ((message ("doIf: test ensures %s ", constraintList_unparse(test->ensuresConstraints))));
- DPRINTF ((message ("doIf: test true ensures %s ", constraintList_print(test->trueEnsuresConstraints) ) ) );
+ DPRINTF ((message ("doIf: test true ensures %s ", constraintList_unparse(test->trueEnsuresConstraints))));
constraintList_free(e->requiresConstraints);
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_unparse(e->requiresConstraints))));
return e;
}
Precondition
This function assumes that p, trueBranch, falseBranch have have all been traversed
- for constraints i.e. we assume that exprNode_traversEnsuresConstraints,
- exprNode_traversRequiresConstraints, exprNode_traversTrueEnsuresConstraints,
- exprNode_traversFalseEnsuresConstraints have all been run
+ for constraints i.e. we assume that exprNode_traverseEnsuresConstraints,
+ exprNode_traverseRequiresConstraints, exprNode_traverseTrueEnsuresConstraints,
+ exprNode_traverseFalseEnsuresConstraints have all been run
*/
-
static exprNode doIfElse (/*@returned@*/ exprNode e, /*@dependent@*/ exprNode p, /*@dependent@*/ exprNode trueBranch, /*@dependent@*/ exprNode falseBranch)
{
constraintList c1, cons, t, t2, f, f2;
- DPRINTF ((message ("doIfElse: %s ", exprNode_unparse(e) ) ) );
+ llassert (exprNode_isDefined (e));
+ llassert (exprNode_isDefined (p));
+ llassert (exprNode_isDefined (trueBranch));
+ llassert (exprNode_isDefined (falseBranch));
+ DPRINTF ((message ("doIfElse: %s ", exprNode_unparse(e))));
/* do requires clauses */
c1 = constraintList_copy (p->ensuresConstraints);
cons = constraintList_reflectChanges(falseBranch->requiresConstraints, p->falseEnsuresConstraints);
cons = constraintList_reflectChangesFreePre (cons, c1);
- constraintList_free(e->requiresConstraints);
+ constraintList_free (e->requiresConstraints);
e->requiresConstraints = constraintList_mergeRequiresFreeFirst (t, cons);
e->requiresConstraints = constraintList_mergeRequiresFreeFirst (e->requiresConstraints, p->requiresConstraints);
constraintList_free(cons);
constraintList_free(c1);
- DPRINTF ((message ("doIfElse: if requires %q ", constraintList_print(e->requiresConstraints) ) ) );
- DPRINTF ((message ("doIfElse: if ensures %q ", constraintList_print(e->ensuresConstraints) ) ) );
+ DPRINTF ((message ("doIfElse: if requires %q ", constraintList_unparse(e->requiresConstraints))));
+ DPRINTF ((message ("doIfElse: if ensures %q ", constraintList_unparse(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);
}
sRefSet_elements (s, el)
{
- if (sRef_isFixedArray(el) )
+ if (sRef_isFixedArray(el))
{
- long int size;
+ size_t size;
DPRINTF((message("%s is a fixed array",
- sRef_unparse(el)) ) );
+ 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));
+ sRef_unparse(el), (int)size)));
+ con = constraint_makeSRefSetBufferSize (el, size_toLong (size - 1));
ret = constraintList_add(ret, con);
}
else
{
DPRINTF((message("%s is not a fixed array",
- sRef_unparse(el)) ) );
+ sRef_unparse(el))));
- if (sRef_isExternallyVisible (el) )
+ if (sRef_isExternallyVisible (el))
{
/*
DPRINTF((message("%s is externally visible",
- sRef_unparse(el) ) ));
+ sRef_unparse(el))));
con = constraint_makeSRefWriteSafeInt(el, 0);
ret = constraintList_add(ret, con);
}
end_sRefSet_elements ;
- DPRINTF(( message("constraintList_makeFixedArrayConstraints returning %s",
- constraintList_print(ret) ) ));
+ DPRINTF((message("constraintList_makeFixedArrayConstraints returning %s",
+ constraintList_unparse(ret))));
return ret;
}
exprNode init, test, inc;
/* merge the constraints: modle as if statement */
- /* init
- if (test)
- for body
- inc */
- init = exprData_getTripleInit (forPred->edata);
- test = exprData_getTripleTest (forPred->edata);
- inc = exprData_getTripleInc (forPred->edata);
+ /* init
+ if (test)
+ for body
+ inc */
+
+ 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) ) ) )
+ if (((exprNode_isError (test) /*|| (exprNode_isError(init))*/) || (exprNode_isError (inc))))
{
- DPRINTF ((message ("strange for statement:%s, ignoring it", exprNode_unparse(e) ) ) );
+ DPRINTF ((message ("strange for statement:%s, ignoring it", exprNode_unparse(e))));
return;
}
if (!forBody->canBreak)
{
- e->ensuresConstraints = constraintList_addListFree(e->ensuresConstraints, constraintList_copy(forPred->ensuresConstraints) );
- e->ensuresConstraints = constraintList_addListFree(e->ensuresConstraints,constraintList_copy( test->falseEnsuresConstraints));
+ e->ensuresConstraints = constraintList_addListFree(e->ensuresConstraints, constraintList_copy(forPred->ensuresConstraints));
+ e->ensuresConstraints = constraintList_addListFree(e->ensuresConstraints,constraintList_copy(test->falseEnsuresConstraints));
}
else
{
- DPRINTF(("Can break") );
+ DPRINTF(("Can break"));
}
}
static /*@dependent@*/ exprNode exprNode_makeDependent(/*@returned@*/ exprNode e)
{
- /*@-temptrans@*/
+ /* !!! DRL - this is ridiculous! Read the manual on memory annotations please! */
return e;
- /*@=temptrans@*/
}
static void
{
exprNode stmt, stmtList;
- DPRINTF(( message("exprNode_doGenerateConstraintSwitch: (switch %s) %s",
+ DPRINTF((message("exprNode_doGenerateConstraintSwitch: (switch %s) %s",
exprNode_unparse(switchExpr), exprNode_unparse(body)
- ) ));
+ )));
- if (exprNode_isError(body) )
+ if (exprNode_isError(body))
{
*currentRequires = constraintList_makeNew ();
*currentEnsures = constraintList_makeNew ();
/*@=onlytrans@*/
}
- if (body->kind != XPR_STMTLIST )
+ if (body->kind != XPR_STMTLIST)
{
DPRINTF((message("exprNode_doGenerateConstraintSwitch: non stmtlist: %s",
- exprNode_unparse(body) )));
+ exprNode_unparse(body))));
stmt = body;
stmtList = exprNode_undefined;
stmt = exprNode_makeDependent(stmt);
}
DPRINTF((message("exprNode_doGenerateConstraintSwitch: stmtlist: %s stmt: %s",
- exprNode_unparse(stmtList), exprNode_unparse(stmt) )
- ));
+ exprNode_unparse(stmtList), exprNode_unparse(stmt))
+ ));
exprNode_doGenerateConstraintSwitch (switchExpr, stmtList, currentRequires, currentEnsures,
- savedRequires, savedEnsures );
+ savedRequires, savedEnsures);
- if (exprNode_isError(stmt) )
+ if (exprNode_isError(stmt))
/*@-onlytrans@*/
return;
/*@=onlytrans@*/
switchExpr = exprNode_makeDependent (switchExpr);
- if (! exprNode_isCaseMarker(stmt) )
+ if (! exprNode_isCaseMarker(stmt))
{
constraintList temp;
- DPRINTF (( message("Got normal statement %s (requires %s ensures %s)", exprNode_unparse(stmt),
- constraintList_unparse(stmt->requiresConstraints), constraintList_unparse(stmt->ensuresConstraints) ) ));
+ DPRINTF ((message("Got normal statement %s (requires %s ensures %s)", exprNode_unparse(stmt),
+ constraintList_unparse(stmt->requiresConstraints), constraintList_unparse(stmt->ensuresConstraints))));
temp = constraintList_reflectChanges (stmt->requiresConstraints,
*currentEnsures);
*currentEnsures = constraintList_mergeEnsuresFreeFirst
(*currentEnsures,
stmt->ensuresConstraints);
- DPRINTF(( message("returning from exprNode_doGenerateConstraintSwitch: (switch %s) %s currentRequires:"
+ DPRINTF((message("returning from exprNode_doGenerateConstraintSwitch: (switch %s) %s currentRequires:"
"%s currentEnsures:%s",
exprNode_unparse(switchExpr), exprNode_unparse(body),
- constraintList_print(*currentRequires), constraintList_print(*currentEnsures)
- ) ));
+ constraintList_unparse(*currentRequires), constraintList_unparse(*currentEnsures)
+ )));
/*@-onlytrans@*/
return;
/*@=onlytrans@*/
}
- if (exprNode_isCaseMarker(stmt) && exprNode_mustEscape(stmtList) )
+ if (exprNode_isCaseMarker(stmt) && exprNode_mustEscape(stmtList))
{
/*
** merge current and saved constraint with Logical Or...
constraintList temp;
constraint con;
- DPRINTF (( message("Got case marker") ));
+ DPRINTF ((message("Got case marker")));
if (constraintList_isUndefined(*savedEnsures) &&
- constraintList_isUndefined(*savedRequires) )
+ constraintList_isUndefined(*savedRequires))
{
- llassert(constraintList_isUndefined(*savedEnsures) );
- llassert(constraintList_isUndefined(*savedRequires) );
+ llassert(constraintList_isUndefined(*savedEnsures));
+ llassert(constraintList_isUndefined(*savedRequires));
*savedEnsures = constraintList_copy(*currentEnsures);
*savedRequires = constraintList_copy(*currentRequires);
}
else
{
- DPRINTF (( message("Doing logical or") ));
+ DPRINTF ((message("Doing logical or")));
temp = constraintList_logicalOr (*savedEnsures, *currentEnsures);
constraintList_free (*savedEnsures);
*savedEnsures = temp;
*savedRequires = constraintList_mergeRequiresFreeFirst (*savedRequires, *currentRequires);
}
- con = constraint_makeEnsureEqual (switchExpr, exprData_getSingle
- (stmt->edata), exprNode_getfileloc(stmt) );
-
+ con = constraint_makeEnsureEqual (switchExpr, exprData_getSingle (stmt->edata), exprNode_loc (stmt));
- constraintList_free(*currentEnsures);
+ 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)
- ) ));
-
+ DPRINTF (("exprNode_doGenerateConstraintSwitch: (switch %s) %s savedRequires:"
+ "%s savedEnsures:%s",
+ exprNode_unparse(switchExpr), exprNode_unparse(body),
+ constraintList_unparse(*savedRequires), constraintList_unparse(*savedEnsures)
+ ));
}
-
- else if (exprNode_isCaseMarker(stmt) )
- /* prior case has no break. */
+ 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
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) );
-
- ensuresTemp = constraintList_makeNew();
-
+ con = constraint_makeEnsureEqual (switchExpr, exprData_getSingle (stmt->edata), exprNode_loc (stmt));
+
+ ensuresTemp = constraintList_makeNew ();
ensuresTemp = constraintList_add (ensuresTemp, con);
- if (exprNode_isError(stmtList) )
+ if (exprNode_isError (stmtList))
{
- constraintList_free(*currentEnsures);
-
- *currentEnsures = constraintList_copy(ensuresTemp);
- constraintList_free(ensuresTemp);
-
+ constraintList_free (*currentEnsures);
+ *currentEnsures = constraintList_copy (ensuresTemp);
+ constraintList_free (ensuresTemp);
}
else
{
-
temp = constraintList_logicalOr (*currentEnsures, ensuresTemp);
-
- constraintList_free(*currentEnsures);
- constraintList_free(ensuresTemp);
-
+ constraintList_free (*currentEnsures);
+ constraintList_free (ensuresTemp);
*currentEnsures = temp;
}
- constraintList_free(*currentRequires);
-
+
+ constraintList_free (*currentRequires);
*currentRequires = constraintList_makeNew();
}
else
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)
- ) ));
+ DPRINTF (("returning from exprNode_doGenerateConstraintSwitch: (switch %s) %s currentRequires:"
+ "%s currentEnsures:%s",
+ exprNode_unparse(switchExpr), exprNode_unparse(body),
+ constraintList_unparse(*currentRequires), constraintList_unparse(*currentEnsures)
+ ));
+
/*@-onlytrans@*/
return;
/*@=onlytrans@*/
-
}
-static void exprNode_generateConstraintSwitch (exprNode switchStmt)
+static void exprNode_generateConstraintSwitch (/*@notnull@*/ exprNode switchStmt)
{
constraintList constraintsRequires;
constraintList constraintsEnsures;
exprNode body;
exprNode switchExpr;
- switchExpr = exprData_getPairA(switchStmt->edata);
- body = exprData_getPairB(switchStmt->edata);
+ switchExpr = exprData_getPairA (switchStmt->edata);
+ body = exprData_getPairB (switchStmt->edata);
+
+ if (!exprNode_isDefined (body))
+ {
+ return;
+ }
- /*@i22*/
- DPRINTF((message("") ));
+ DPRINTF((message("")));
- if ( body->kind == XPR_BLOCK)
+ if (body->kind == XPR_BLOCK)
body = exprData_getSingle(body->edata);
- /*
+
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 */
+ /* evans 2002-01-01: spurious warnings for these becuase of stack allocated storage */
exprNode_doGenerateConstraintSwitch (switchExpr, body, &lastRequires,
&lastEnsures, &constraintsRequires, &constraintsEnsures);
/*@=mustfree@*/
constraintList_free(switchStmt->requiresConstraints);
constraintList_free(switchStmt->ensuresConstraints);
- if (constraintList_isDefined(constraintsEnsures) && constraintList_isDefined(constraintsRequires) )
+ if (constraintList_isDefined(constraintsEnsures) && constraintList_isDefined(constraintsRequires))
{
switchStmt->ensuresConstraints = constraintList_logicalOr(constraintsEnsures, lastEnsures);
switchStmt->requiresConstraints = constraintList_mergeRequires(constraintsRequires, lastRequires);
constraintList_free (lastEnsures);
DPRINTF(((message(" exprNode_generateConstraintSwitch returning requires: %s and ensures %s",
- constraintList_print( switchStmt->requiresConstraints),
- constraintList_print( switchStmt->ensuresConstraints)
- )
- ) ));
+ constraintList_unparse(switchStmt->requiresConstraints),
+ constraintList_unparse(switchStmt->ensuresConstraints)
+ )
+ )));
}
-static exprNode doSwitch (/*@returned@*/ exprNode e)
+static exprNode doSwitch (/*@returned@*/ /*@notnull@*/ exprNode e)
{
exprNode body;
exprData data;
data = e->edata;
- DPRINTF (( message ("doSwitch for: switch (%s) %s",
+ DPRINTF ((message ("doSwitch for: switch (%s) %s",
exprNode_unparse (exprData_getPairA (data)),
- exprNode_unparse (exprData_getPairB (data))) ));
+ exprNode_unparse (exprData_getPairB (data)))));
body = exprData_getPairB (data);
exprNode_generateConstraintSwitch (e);
constraintList temp;
- DPRINTF((message ("exprNode_multistatement Analysising %s %s at", exprNode_unparse( e),
- fileloc_unparse(exprNode_getfileloc(e) ) ) ) );
+ DPRINTF((message ("exprNode_multistatement Analysising %s %s at", exprNode_unparse(e),
+ fileloc_unparse(exprNode_getfileloc(e)))));
if (exprNode_handleError (e))
{
break;
case XPR_FORPRED:
- exprNode_generateConstraints (exprData_getTripleInit (data) );
+ exprNode_generateConstraints (exprData_getTripleInit (data));
test = exprData_getTripleTest (data);
exprNode_exprTraverse (test,FALSE, FALSE, exprNode_loc(e));
- exprNode_generateConstraints (exprData_getTripleInc (data) );
+ exprNode_generateConstraints (exprData_getTripleInc (data));
- if (!exprNode_isError(test) )
+ if (!exprNode_isError(test))
{
constraintList temp2;
temp2 = test->trueEnsuresConstraints;
- test->trueEnsuresConstraints = exprNode_traversTrueEnsuresConstraints(test);
+ test->trueEnsuresConstraints = exprNode_traverseTrueEnsuresConstraints(test);
constraintList_free(temp2);
}
break;
case XPR_IF:
- DPRINTF(( "IF:") );
- DPRINTF ((exprNode_unparse(e) ) );
+ DPRINTF(("IF:"));
+ DPRINTF ((exprNode_unparse(e)));
e1 = exprData_getPairA (data);
e2 = exprData_getPairB (data);
case XPR_IFELSE:
DPRINTF(("Starting IFELSE"));
p = exprData_getTriplePred (data);
+
trueBranch = exprData_getTripleTrue (data);
falseBranch = exprData_getTripleFalse (data);
exprNode_generateConstraints (trueBranch);
exprNode_generateConstraints (falseBranch);
+ llassert (exprNode_isDefined (p));
temp = p->ensuresConstraints;
- p->ensuresConstraints = exprNode_traversEnsuresConstraints (p);
+ p->ensuresConstraints = exprNode_traverseEnsuresConstraints (p);
constraintList_free(temp);
temp = p->requiresConstraints;
- p->requiresConstraints = exprNode_traversRequiresConstraints (p);
+ p->requiresConstraints = exprNode_traverseRequiresConstraints (p);
constraintList_free(temp);
temp = p->trueEnsuresConstraints;
- p->trueEnsuresConstraints = exprNode_traversTrueEnsuresConstraints(p);
+ p->trueEnsuresConstraints = exprNode_traverseTrueEnsuresConstraints(p);
constraintList_free(temp);
+
+
+ DPRINTF((message("p->trueEnsuresConstraints before substitue %s", constraintList_unparse(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_unparse(p->trueEnsuresConstraints) )
+ ));
+
temp = p->falseEnsuresConstraints;
- p->falseEnsuresConstraints = exprNode_traversFalseEnsuresConstraints(p);
+ p->falseEnsuresConstraints = exprNode_traverseFalseEnsuresConstraints(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_unparse(e->requiresConstraints))));
break;
case XPR_BLOCK:
- 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 );
+ {
+ exprNode tempExpr;
+
+ tempExpr = exprData_getSingle (data);
+
+ exprNode_generateConstraints (tempExpr);
+
+ if (exprNode_isDefined(tempExpr) )
+ {
+ constraintList_free(e->requiresConstraints);
+ e->requiresConstraints = constraintList_copy (tempExpr->requiresConstraints);
+ constraintList_free(e->ensuresConstraints);
+ e->ensuresConstraints = constraintList_copy (tempExpr->ensuresConstraints);
+ }
+ else
+ {
+ llassert(FALSE);
+ }
+ }
break;
case XPR_SWITCH:
I don't want to violate the abstraction
maybe this should go in lltok.c */
- if (lltok_isEq_Op (tok) )
+ if (lltok_isEqOp (tok))
{
return TRUE;
}
- if (lltok_isAnd_Op (tok) )
+ if (lltok_isAndOp (tok))
{
return TRUE;
}
- if (lltok_isOr_Op (tok) )
+ if (lltok_isOrOp (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;
}
exprData data;
lltok tok;
constraintList tempList, temp;
+
+ if (exprNode_isUndefined(e) )
+ {
+ llassert (exprNode_isDefined(e) );
+ return;
+ }
+
data = e->edata;
tok = exprData_getOpTok (data);
t1 = exprData_getOpA (data);
t2 = exprData_getOpB (data);
+
+ /* drl 3/2/2003 we know this because of the type of expression*/
+ llassert( exprNode_isDefined(t1) && exprNode_isDefined(t2) );
+
tempList = constraintList_undefined;
/* arithmetic tests */
- if (lltok_isEq_Op (tok) )
+ if (lltok_isEqOp (tok))
{
cons = constraint_makeEnsureEqual (t1, t2, sequencePoint);
e->trueEnsuresConstraints = constraintList_add(e->trueEnsuresConstraints, cons);
}
- if (lltok_isLt_Op (tok) )
+ if (lltok_isLt_Op (tok))
{
cons = constraint_makeEnsureLessThan (t1, t2, sequencePoint);
e->trueEnsuresConstraints = constraintList_add(e->trueEnsuresConstraints, cons);
e->falseEnsuresConstraints = constraintList_add(e->falseEnsuresConstraints, cons);
}
- if (lltok_isGe_Op (tok) )
+ if (lltok_isGe_Op (tok))
{
cons = constraint_makeEnsureGreaterThanEqual (t1, t2, sequencePoint);
e->trueEnsuresConstraints = constraintList_add(e->trueEnsuresConstraints, cons);
e->falseEnsuresConstraints = constraintList_add(e->falseEnsuresConstraints, cons);
}
- if (lltok_isGt_Op (tok) )
+ if (lltok_isGt_Op (tok))
{
cons = constraint_makeEnsureGreaterThan (t1, t2, sequencePoint);
e->trueEnsuresConstraints = constraintList_add(e->trueEnsuresConstraints, cons);
e->falseEnsuresConstraints = constraintList_add(e->falseEnsuresConstraints, cons);
}
- if (lltok_isLe_Op (tok) )
+ if (lltok_isLe_Op (tok))
{
cons = constraint_makeEnsureLessThanEqual (t1, t2, sequencePoint);
e->trueEnsuresConstraints = constraintList_add(e->trueEnsuresConstraints, cons);
/* Logical operations */
- if (lltok_isAnd_Op (tok) )
+ if (lltok_isAndOp (tok))
{
/* true ensures */
tempList = constraintList_copy (t1->trueEnsuresConstraints);
/* evans - was constraintList_addList - memory leak detected by splint */
e->falseEnsuresConstraints = constraintList_addListFree (e->falseEnsuresConstraints, tempList);
}
- else if (lltok_isOr_Op (tok) )
+ else if (lltok_isOrOp (tok))
{
/* false ensures */
tempList = constraintList_copy (t1->falseEnsuresConstraints);
}
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)
+void exprNode_exprTraverse (/*@dependent@*/ exprNode e,
+ bool definatelv, bool definaterv,
+ /*@observer@*/ /*@temp@*/ fileloc sequencePoint)
{
exprNode t1, t2, fcn;
lltok tok;
- bool handledExprNode;
exprData data;
constraint cons;
-
constraintList temp;
- if (exprNode_isError(e) )
+ if (exprNode_isError(e))
{
return;
}
- DPRINTF((message ("exprNode_exprTraverset Analysising %s %s at", exprNode_unparse( e),
- fileloc_unparse(exprNode_getfileloc(e) ) ) ) );
-
- /*e->requiresConstraints = constraintList_makeNew();
- e->ensuresConstraints = constraintList_makeNew();
- e->trueEnsuresConstraints = constraintList_makeNew();;
- e->falseEnsuresConstraints = constraintList_makeNew();;
- */
-
- if (exprNode_isUnhandled (e) )
- {
- return;
- }
+ DPRINTF (("exprNode_exprTraverse analyzing %s at %s",
+ exprNode_unparse (e),
+ fileloc_unparse (exprNode_loc (e))));
- handledExprNode = TRUE;
+ if (exprNode_isUnhandled (e))
+ {
+ return;
+ }
data = e->edata;
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);
exprNode_exprTraverse (exprData_getPairA (data), FALSE, TRUE, sequencePoint);
exprNode_exprTraverse (exprData_getPairB (data), FALSE, TRUE, sequencePoint);
- /*@i325 Should check which is array/index. */
break;
case XPR_PARENS:
break;
case XPR_INIT:
{
- /*
- idDecl t;
-
- uentry ue;
- exprNode lhs;
-
- t = exprData_getInitId (data);
- ue = usymtab_lookup (idDecl_observeId (t));
- lhs = exprNode_createId (ue);
- */
t2 = exprData_getInitNode (data);
-
- /* DPRINTF(((message("initialization: %s = %s",
- exprNode_unparse(lhs),
- exprNode_unparse(t2)
- )
- ) )); */
- exprNode_exprTraverse (t2, definatelv, TRUE, sequencePoint );
+ DPRINTF (("initialization ==> %s",exprNode_unparse (t2)));
- /* this test is nessecary because some expressions generate a null expression node. function pointer do that -- drl */
- if ((!exprNode_isError (e)) && (!exprNode_isError(t2)) )
+ exprNode_exprTraverse (t2, definatelv, TRUE, sequencePoint);
+
+ /* This test is nessecary because some expressions generate a null expression node.
+ function pointer do that -- drl */
+
+ if (!exprNode_isError (e) && !exprNode_isError (t2))
{
cons = constraint_makeEnsureEqual (e, t2, sequencePoint);
e->ensuresConstraints = constraintList_add(e->ensuresConstraints, cons);
case XPR_ASSIGN:
t1 = exprData_getOpA (data);
t2 = exprData_getOpB (data);
- 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)) )
+ DPRINTF (("Assignment constraints t1: %s", constraintList_unparse (t1->ensuresConstraints)));
+ DPRINTF (("Assignment constraints t2: %s", constraintList_unparse (t2->ensuresConstraints)));
+ exprNode_exprTraverse (t1, TRUE, definaterv, sequencePoint);
+ DPRINTF (("Assignment constraints t1: %s", constraintList_unparse (t1->ensuresConstraints)));
+ DPRINTF (("Assignment constraints t2: %s", constraintList_unparse (t2->ensuresConstraints)));
+ exprNode_exprTraverse (t2, definatelv, TRUE, sequencePoint);
+ DPRINTF (("Assignment constraints t1: %s", constraintList_unparse (t1->ensuresConstraints)));
+ DPRINTF (("Assignment constraints t2: %s", constraintList_unparse (t2->ensuresConstraints)));
+
+ /* this test is nessecary because some expressions generate a null expression node.
+ function pointer do that -- drl */
+
+ if ((!exprNode_isError (t1)) && (!exprNode_isError(t2)))
{
- cons = constraint_makeEnsureEqual (t1, t2, sequencePoint);
- e->ensuresConstraints = constraintList_add(e->ensuresConstraints, cons);
+ cons = constraint_makeEnsureEqual (t1, t2, sequencePoint);
+ DPRINTF (("Ensure equal constraint: %s", constraint_unparse (cons)));
+ e->ensuresConstraints = constraintList_add (e->ensuresConstraints, cons);
+ DPRINTF (("Assignment constraints: %s", constraintList_unparse (e->ensuresConstraints)));
}
break;
case XPR_OP:
t1 = exprData_getOpA (data);
t2 = exprData_getOpB (data);
- tok = exprData_getOpTok (data);
-
+ tok = exprData_getOpTok (data);
- if (tok.tok == ADD_ASSIGN)
+ if (lltok_getTok (tok) == ADD_ASSIGN)
{
- exprNode_exprTraverse (t1, TRUE, definaterv, sequencePoint );
- exprNode_exprTraverse (t2, definatelv, TRUE, sequencePoint );
+ exprNode_exprTraverse (t1, TRUE, definaterv, sequencePoint);
+ exprNode_exprTraverse (t2, definatelv, TRUE, sequencePoint);
- cons = constraint_makeAddAssign (t1, t2, sequencePoint );
+ cons = constraint_makeAddAssign (t1, t2, sequencePoint);
e->ensuresConstraints = constraintList_add(e->ensuresConstraints, cons);
}
- else if (tok.tok == SUB_ASSIGN)
+ else if (lltok_getTok (tok) == SUB_ASSIGN)
{
- exprNode_exprTraverse (t1, TRUE, definaterv, sequencePoint );
- exprNode_exprTraverse (t2, definatelv, TRUE, sequencePoint );
+ exprNode_exprTraverse (t1, TRUE, definaterv, sequencePoint);
+ exprNode_exprTraverse (t2, definatelv, TRUE, sequencePoint);
- cons = constraint_makeSubtractAssign (t1, t2, sequencePoint );
+ cons = constraint_makeSubtractAssign (t1, t2, sequencePoint);
e->ensuresConstraints = constraintList_add(e->ensuresConstraints, cons);
}
else
{
- exprNode_exprTraverse (t1, definatelv, definaterv, sequencePoint );
- exprNode_exprTraverse (t2, definatelv, definaterv, sequencePoint );
+ exprNode_exprTraverse (t1, definatelv, definaterv, sequencePoint);
+ exprNode_exprTraverse (t2, definatelv, definaterv, sequencePoint);
}
- if (lltok_isBoolean_Op (tok) )
+ if (lltok_isBoolean_Op (tok))
exprNode_booleanTraverse (e, definatelv, definaterv, sequencePoint);
break;
case XPR_SIZEOFT:
- /*@i43 drl possible problem : warning make sure the case can be ignored.. */
+ /*drl 4-11-03 I think this is the same as the next case...*/
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 (("Got call that %s (%s)",
+ exprNode_unparse(fcn), exprNodeList_unparse (exprData_getArgs (data))));
- fcn->requiresConstraints = constraintList_addListFree (fcn->requiresConstraints,
- checkCall (fcn, exprData_getArgs (data) ) );
-
- fcn->ensuresConstraints = constraintList_addListFree (fcn->ensuresConstraints,
- exprNode_getPostConditions(fcn, exprData_getArgs (data),e ) );
-
- t1 = exprNode_createNew (exprNode_getType (e) );
+ llassert( exprNode_isDefined(fcn) );
+
+ fcn->requiresConstraints =
+ constraintList_addListFree (fcn->requiresConstraints,
+ checkCall (fcn, exprData_getArgs (data)));
+
+ fcn->ensuresConstraints =
+ constraintList_addListFree (fcn->ensuresConstraints,
+ exprNode_getPostConditions(fcn, exprData_getArgs (data),e ));
+
+ t1 = exprNode_createNew (exprNode_getType (e));
checkArgumentList (t1, exprData_getArgs(data), sequencePoint);
exprNode_mergeResolve (e, t1, fcn);
exprNode_free(t1);
break;
case XPR_RETURN:
- exprNode_exprTraverse (exprData_getSingle (data), definatelv, definaterv, sequencePoint );
+ exprNode_exprTraverse (exprData_getSingle (data), definatelv, definaterv, sequencePoint);
break;
case XPR_NULLRETURN:
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:
case XPR_PREOP:
t1 = exprData_getUopNode(data);
+
+
+ /* drl 3/2/2003 we know this because of the type of expression*/
+ llassert( exprNode_isDefined(t1) );
+
+
tok = (exprData_getUopTok (data));
- exprNode_exprTraverse (t1, definatelv, definaterv, sequencePoint );
+ exprNode_exprTraverse (t1, definatelv, definaterv, sequencePoint);
/*handle * pointer access */
- if (lltok_isInc_Op (tok) )
+ if (lltok_isIncOp (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_isDecOp (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)
{
}
e->requiresConstraints = constraintList_add(e->requiresConstraints, cons);
}
- else if (lltok_isNot_Op (tok) )
+ else if (lltok_isNotOp (tok))
/* ! expr */
{
constraintList_free(e->trueEnsuresConstraints);
e->falseEnsuresConstraints = constraintList_copy (t1->trueEnsuresConstraints);
}
- else if (lltok_isAmpersand_Op (tok) )
+ else if (lltok_isAmpersand_Op (tok))
{
break;
}
- else if (lltok_isMinus_Op (tok) )
+ else if (lltok_isMinus_Op (tok))
{
break;
}
- else if ( lltok_isExcl_Op (tok) )
+ else if (lltok_isExcl_Op (tok))
{
break;
}
- else if (lltok_isTilde_Op (tok) )
+ else if (lltok_isTilde_Op (tok))
{
break;
}
else
{
- llcontbug((message("Unsupported preop in %s", exprNode_unparse(e) ) ));
+ llcontbug (message("Unsupported preop in %s", exprNode_unparse(e)));
BADEXIT;
}
break;
case XPR_POSTOP:
+ exprNode_exprTraverse (exprData_getUopNode (data), TRUE,
+ definaterv, sequencePoint);
- exprNode_exprTraverse (exprData_getUopNode (data), TRUE, definaterv, sequencePoint );
-
- if (lltok_isInc_Op (exprData_getUopTok (data) ) )
+ if (lltok_isIncOp (exprData_getUopTok (data)))
{
DPRINTF(("doing ++"));
t1 = exprData_getUopNode (data);
- cons = constraint_makeMaxSetSideEffectPostIncrement (t1, sequencePoint );
+ cons = constraint_makeMaxSetSideEffectPostIncrement (t1, sequencePoint);
e->ensuresConstraints = constraintList_add (e->ensuresConstraints, cons);
}
- if (lltok_isDec_Op (exprData_getUopTok (data) ) )
+ if (lltok_isDecOp (exprData_getUopTok (data)))
{
DPRINTF(("doing --"));
t1 = exprData_getUopNode (data);
- cons = constraint_makeMaxSetSideEffectPostDecrement (t1, sequencePoint );
+ cons = constraint_makeMaxSetSideEffectPostDecrement (t1, sequencePoint);
e->ensuresConstraints = constraintList_add (e->ensuresConstraints, cons);
}
break;
case XPR_CAST:
{
t2 = exprData_getCastNode (data);
- DPRINTF (( message ("Examining cast (%q)%s",
+ DPRINTF ((message ("Examining cast (%q)%s",
qtype_unparse (exprData_getCastType (data)),
- exprNode_unparse (t2) )
- ));
- exprNode_exprTraverse (t2, definatelv, definaterv, sequencePoint );
+ exprNode_unparse (t2))
+ ));
+ exprNode_exprTraverse (t2, definatelv, definaterv, sequencePoint);
}
break;
case XPR_COND:
{
exprNode pred, trueBranch, falseBranch;
- llassert(FALSE);
- pred = exprData_getTriplePred (data);
- trueBranch = exprData_getTripleTrue (data);
- falseBranch = exprData_getTripleFalse (data);
-
- exprNode_exprTraverse (pred, FALSE, TRUE, sequencePoint );
-
- temp = pred->ensuresConstraints;
- pred->ensuresConstraints = exprNode_traversEnsuresConstraints(pred);
- constraintList_free(temp);
-
- temp = pred->requiresConstraints;
- pred->requiresConstraints = exprNode_traversRequiresConstraints(pred);
- constraintList_free(temp);
-
- temp = pred->trueEnsuresConstraints;
- pred->trueEnsuresConstraints = exprNode_traversTrueEnsuresConstraints(pred);
- constraintList_free(temp);
-
- temp = pred->falseEnsuresConstraints;
- pred->falseEnsuresConstraints = exprNode_traversFalseEnsuresConstraints(pred);
- constraintList_free(temp);
-
-
- exprNode_exprTraverse (trueBranch, FALSE, TRUE, sequencePoint );
-
- temp = trueBranch->ensuresConstraints;
- trueBranch->ensuresConstraints = exprNode_traversEnsuresConstraints(trueBranch);
- constraintList_free(temp);
-
-
- temp = trueBranch->requiresConstraints;
- trueBranch->requiresConstraints = exprNode_traversRequiresConstraints(trueBranch);
- constraintList_free(temp);
-
-
- temp = trueBranch->trueEnsuresConstraints;
- trueBranch->trueEnsuresConstraints = exprNode_traversTrueEnsuresConstraints(trueBranch);
- constraintList_free(temp);
-
- temp = trueBranch->falseEnsuresConstraints;
- trueBranch->falseEnsuresConstraints = exprNode_traversFalseEnsuresConstraints(trueBranch);
- constraintList_free(temp);
-
- exprNode_exprTraverse (falseBranch, FALSE, TRUE, sequencePoint );
-
- temp = falseBranch->ensuresConstraints;
- falseBranch->ensuresConstraints = exprNode_traversEnsuresConstraints(falseBranch);
- constraintList_free(temp);
-
-
- temp = falseBranch->requiresConstraints;
- falseBranch->requiresConstraints = exprNode_traversRequiresConstraints(falseBranch);
- constraintList_free(temp);
-
-
- temp = falseBranch->trueEnsuresConstraints;
- falseBranch->trueEnsuresConstraints = exprNode_traversTrueEnsuresConstraints(falseBranch);
- constraintList_free(temp);
-
- temp = falseBranch->falseEnsuresConstraints;
- falseBranch->falseEnsuresConstraints = exprNode_traversFalseEnsuresConstraints(falseBranch);
- constraintList_free(temp);
-
- /* if pred is true e equals true otherwise pred equals false */
-
- cons = constraint_makeEnsureEqual (e, trueBranch, sequencePoint);
- trueBranch->ensuresConstraints = constraintList_add(trueBranch->ensuresConstraints, cons);
-
- cons = constraint_makeEnsureEqual (e, trueBranch, sequencePoint);
- falseBranch->ensuresConstraints = constraintList_add(falseBranch->ensuresConstraints, cons);
+ llassert(FALSE);
+ pred = exprData_getTriplePred (data);
+ trueBranch = exprData_getTripleTrue (data);
+ falseBranch = exprData_getTripleFalse (data);
+
+ llassert (exprNode_isDefined (pred));
+ llassert (exprNode_isDefined (trueBranch));
+ llassert (exprNode_isDefined (falseBranch));
- e = doIfElse (e, pred, trueBranch, falseBranch);
-
+ exprNode_exprTraverse (pred, FALSE, TRUE, sequencePoint);
+
+ temp = pred->ensuresConstraints;
+ pred->ensuresConstraints = exprNode_traverseEnsuresConstraints(pred);
+ constraintList_free(temp);
+
+ temp = pred->requiresConstraints;
+ pred->requiresConstraints = exprNode_traverseRequiresConstraints(pred);
+ constraintList_free(temp);
+
+ temp = pred->trueEnsuresConstraints;
+ pred->trueEnsuresConstraints = exprNode_traverseTrueEnsuresConstraints(pred);
+ constraintList_free(temp);
+
+ temp = pred->falseEnsuresConstraints;
+ pred->falseEnsuresConstraints = exprNode_traverseFalseEnsuresConstraints(pred);
+ constraintList_free(temp);
+
+ exprNode_exprTraverse (trueBranch, FALSE, TRUE, sequencePoint);
+
+ temp = trueBranch->ensuresConstraints;
+ trueBranch->ensuresConstraints = exprNode_traverseEnsuresConstraints(trueBranch);
+ constraintList_free(temp);
+
+ temp = trueBranch->requiresConstraints;
+ trueBranch->requiresConstraints = exprNode_traverseRequiresConstraints(trueBranch);
+ constraintList_free(temp);
+
+ temp = trueBranch->trueEnsuresConstraints;
+ trueBranch->trueEnsuresConstraints = exprNode_traverseTrueEnsuresConstraints(trueBranch);
+ constraintList_free(temp);
+
+ temp = trueBranch->falseEnsuresConstraints;
+ trueBranch->falseEnsuresConstraints = exprNode_traverseFalseEnsuresConstraints(trueBranch);
+ constraintList_free(temp);
+
+ exprNode_exprTraverse (falseBranch, FALSE, TRUE, sequencePoint);
+
+ temp = falseBranch->ensuresConstraints;
+ falseBranch->ensuresConstraints = exprNode_traverseEnsuresConstraints(falseBranch);
+ constraintList_free(temp);
+
+
+ temp = falseBranch->requiresConstraints;
+ falseBranch->requiresConstraints = exprNode_traverseRequiresConstraints(falseBranch);
+ constraintList_free(temp);
+
+ temp = falseBranch->trueEnsuresConstraints;
+ falseBranch->trueEnsuresConstraints = exprNode_traverseTrueEnsuresConstraints(falseBranch);
+ constraintList_free(temp);
+
+ temp = falseBranch->falseEnsuresConstraints;
+ falseBranch->falseEnsuresConstraints = exprNode_traverseFalseEnsuresConstraints(falseBranch);
+ constraintList_free(temp);
+
+ /* if pred is true e equals true otherwise pred equals false */
+
+ cons = constraint_makeEnsureEqual (e, trueBranch, sequencePoint);
+ trueBranch->ensuresConstraints = constraintList_add(trueBranch->ensuresConstraints, cons);
+
+ cons = constraint_makeEnsureEqual (e, trueBranch, sequencePoint);
+ falseBranch->ensuresConstraints = constraintList_add(falseBranch->ensuresConstraints, cons);
+
+ e = doIfElse (e, pred, trueBranch, falseBranch);
}
break;
case XPR_COMMA:
llassert(FALSE);
t1 = exprData_getPairA (data);
t2 = exprData_getPairB (data);
- /* we essiantially treat this like expr1; expr2
- of course sequencePoint isn't adjusted so this isn't completely accurate
- problems../ */
- exprNode_exprTraverse (t1, FALSE, FALSE, sequencePoint );
- exprNode_exprTraverse (t2, definatelv, definaterv, sequencePoint );
+ /* we essiantially treat this like expr1; expr2
+ of course sequencePoint isn't adjusted so this isn't completely accurate
+ problems...
+ */
+ exprNode_exprTraverse (t1, FALSE, FALSE, sequencePoint);
+ exprNode_exprTraverse (t2, definatelv, definaterv, sequencePoint);
exprNode_mergeResolve (e, t1, t2);
break;
default:
- handledExprNode = FALSE;
+ break;
}
- 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->requiresConstraints = constraintList_removeSurpressed( e->requiresConstraints);
+ 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->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 (("ensures constraints for %s are %s",
+ exprNode_unparse(e), constraintList_unparseDetailed (e->ensuresConstraints)));
- DPRINTF((message ("trueEnsures constraints for %s are %s", exprNode_unparse(e), constraintList_printDetailed(e->trueEnsuresConstraints) ) ));
-
- DPRINTF((message ("falseEnsures constraints for %s are %s", exprNode_unparse(e), constraintList_printDetailed(e->falseEnsuresConstraints) ) ));
+ DPRINTF (("Requires constraints for %s are %s", exprNode_unparse(e),
+ constraintList_unparseDetailed(e->ensuresConstraints)));
+ DPRINTF (("trueEnsures constraints for %s are %s", exprNode_unparse(e),
+ constraintList_unparseDetailed(e->trueEnsuresConstraints)));
+
+ DPRINTF (("falseEnsures constraints for %s are %s", exprNode_unparse(e),
+ constraintList_unparseDetailed(e->falseEnsuresConstraints)));
return;
}
-constraintList exprNode_traversTrueEnsuresConstraints (exprNode e)
+constraintList exprNode_traverseTrueEnsuresConstraints (exprNode e)
{
exprNode t1;
ret = constraintList_makeNew();
return ret;
}
- ret = constraintList_copy (e->trueEnsuresConstraints );
+
+ ret = constraintList_copy (e->trueEnsuresConstraints);
handledExprNode = TRUE;
{
case XPR_WHILEPRED:
t1 = exprData_getSingle (data);
- ret = constraintList_addListFree ( ret, exprNode_traversTrueEnsuresConstraints (t1) );
+ ret = constraintList_addListFree (ret, exprNode_traverseTrueEnsuresConstraints (t1));
break;
case XPR_FETCH:
ret = constraintList_addListFree (ret,
- exprNode_traversTrueEnsuresConstraints
- (exprData_getPairA (data) ) );
+ exprNode_traverseTrueEnsuresConstraints
+ (exprData_getPairA (data)));
ret = constraintList_addListFree (ret,
- exprNode_traversTrueEnsuresConstraints
- (exprData_getPairB (data) ) );
+ exprNode_traverseTrueEnsuresConstraints
+ (exprData_getPairB (data)));
break;
case XPR_PREOP:
ret = constraintList_addListFree (ret,
- exprNode_traversTrueEnsuresConstraints
- (exprData_getUopNode (data) ) );
+ exprNode_traverseTrueEnsuresConstraints
+ (exprData_getUopNode (data)));
break;
case XPR_PARENS:
- ret = constraintList_addListFree (ret, exprNode_traversTrueEnsuresConstraints
- (exprData_getUopNode (data) ) );
+ ret = constraintList_addListFree (ret, exprNode_traverseTrueEnsuresConstraints
+ (exprData_getUopNode (data)));
break;
case XPR_INIT:
ret = constraintList_addListFree (ret,
- exprNode_traversTrueEnsuresConstraints
- (exprData_getInitNode (data) ) );
+ exprNode_traverseTrueEnsuresConstraints
+ (exprData_getInitNode (data)));
break;
case XPR_ASSIGN:
ret = constraintList_addListFree (ret,
- exprNode_traversTrueEnsuresConstraints
- (exprData_getOpA (data) ) );
+ exprNode_traverseTrueEnsuresConstraints
+ (exprData_getOpA (data)));
ret = constraintList_addListFree (ret,
- exprNode_traversTrueEnsuresConstraints
- (exprData_getOpB (data) ) );
+ exprNode_traverseTrueEnsuresConstraints
+ (exprData_getOpB (data)));
break;
case XPR_OP:
ret = constraintList_addListFree (ret,
- exprNode_traversTrueEnsuresConstraints
- (exprData_getOpA (data) ) );
+ exprNode_traverseTrueEnsuresConstraints
+ (exprData_getOpA (data)));
ret = constraintList_addListFree (ret,
- exprNode_traversTrueEnsuresConstraints
- (exprData_getOpB (data) ) );
+ exprNode_traverseTrueEnsuresConstraints
+ (exprData_getOpB (data)));
break;
case XPR_SIZEOFT:
break;
case XPR_SIZEOF:
ret = constraintList_addListFree (ret,
- exprNode_traversTrueEnsuresConstraints
- (exprData_getSingle (data) ) );
+ exprNode_traverseTrueEnsuresConstraints
+ (exprData_getSingle (data)));
break;
case XPR_CALL:
ret = constraintList_addListFree (ret,
- exprNode_traversTrueEnsuresConstraints
- (exprData_getFcn (data) ) );
- /*@i11*/ /* exprNodeList_unparse (exprData_getArgs (data) ); */
+ exprNode_traverseTrueEnsuresConstraints
+ (exprData_getFcn (data)));
break;
case XPR_RETURN:
ret = constraintList_addListFree (ret,
- exprNode_traversTrueEnsuresConstraints
- (exprData_getSingle (data) ) );
+ exprNode_traverseTrueEnsuresConstraints
+ (exprData_getSingle (data)));
break;
case XPR_NULLRETURN:
case XPR_FACCESS:
ret = constraintList_addListFree (ret,
- exprNode_traversTrueEnsuresConstraints
- (exprData_getFieldNode (data) ) );
+ exprNode_traverseTrueEnsuresConstraints
+ (exprData_getFieldNode (data)));
break;
case XPR_ARROW:
ret = constraintList_addListFree (ret,
- exprNode_traversTrueEnsuresConstraints
- (exprData_getFieldNode (data) ) );
+ exprNode_traverseTrueEnsuresConstraints
+ (exprData_getFieldNode (data)));
break;
case XPR_STRINGLITERAL:
case XPR_POSTOP:
ret = constraintList_addListFree (ret,
- exprNode_traversTrueEnsuresConstraints
- (exprData_getUopNode (data) ) );
+ exprNode_traverseTrueEnsuresConstraints
+ (exprData_getUopNode (data)));
break;
case XPR_CAST:
ret = constraintList_addListFree (ret,
- exprNode_traversTrueEnsuresConstraints
- (exprData_getCastNode (data) ) );
+ exprNode_traverseTrueEnsuresConstraints
+ (exprData_getCastNode (data)));
break;
default:
return ret;
}
-constraintList exprNode_traversFalseEnsuresConstraints (exprNode e)
+constraintList exprNode_traverseFalseEnsuresConstraints (exprNode e)
{
exprNode t1;
bool handledExprNode;
exprData data;
constraintList ret;
-
- if (exprNode_handleError (e))
- {
- ret = constraintList_makeNew();
- return ret;
- }
-
- ret = constraintList_copy (e->falseEnsuresConstraints );
-
- handledExprNode = TRUE;
-
+
+ if (exprNode_handleError (e))
+ {
+ ret = constraintList_makeNew();
+ return ret;
+ }
+
+ ret = constraintList_copy (e->falseEnsuresConstraints);
+ handledExprNode = TRUE;
data = e->edata;
switch (e->kind)
{
case XPR_WHILEPRED:
t1 = exprData_getSingle (data);
- ret = constraintList_addListFree ( ret,exprNode_traversFalseEnsuresConstraints (t1) );
+ ret = constraintList_addListFree (ret,exprNode_traverseFalseEnsuresConstraints (t1));
break;
case XPR_FETCH:
ret = constraintList_addListFree (ret,
- exprNode_traversFalseEnsuresConstraints
- (exprData_getPairA (data) ) );
+ exprNode_traverseFalseEnsuresConstraints
+ (exprData_getPairA (data)));
ret = constraintList_addListFree (ret,
- exprNode_traversFalseEnsuresConstraints
- (exprData_getPairB (data) ) );
+ exprNode_traverseFalseEnsuresConstraints
+ (exprData_getPairB (data)));
break;
case XPR_PREOP:
ret = constraintList_addListFree (ret,
- exprNode_traversFalseEnsuresConstraints
- (exprData_getUopNode (data) ) );
+ exprNode_traverseFalseEnsuresConstraints
+ (exprData_getUopNode (data)));
break;
case XPR_PARENS:
- ret = constraintList_addListFree (ret, exprNode_traversFalseEnsuresConstraints
- (exprData_getUopNode (data) ) );
+ ret = constraintList_addListFree (ret, exprNode_traverseFalseEnsuresConstraints
+ (exprData_getUopNode (data)));
break;
case XPR_INIT:
ret = constraintList_addListFree (ret,
- exprNode_traversFalseEnsuresConstraints
- ( exprData_getInitNode (data) ) );
+ exprNode_traverseFalseEnsuresConstraints
+ ( exprData_getInitNode (data)));
break;
case XPR_ASSIGN:
ret = constraintList_addListFree (ret,
- exprNode_traversFalseEnsuresConstraints
- (exprData_getOpA (data) ) );
+ exprNode_traverseFalseEnsuresConstraints
+ (exprData_getOpA (data)));
ret = constraintList_addListFree (ret,
- exprNode_traversFalseEnsuresConstraints
- (exprData_getOpB (data) ) );
+ exprNode_traverseFalseEnsuresConstraints
+ (exprData_getOpB (data)));
break;
case XPR_OP:
ret = constraintList_addListFree (ret,
- exprNode_traversFalseEnsuresConstraints
- (exprData_getOpA (data) ) );
+ exprNode_traverseFalseEnsuresConstraints
+ (exprData_getOpA (data)));
ret = constraintList_addListFree (ret,
- exprNode_traversFalseEnsuresConstraints
- (exprData_getOpB (data) ) );
+ exprNode_traverseFalseEnsuresConstraints
+ (exprData_getOpB (data)));
break;
case XPR_SIZEOFT:
break;
case XPR_SIZEOF:
ret = constraintList_addListFree (ret,
- exprNode_traversFalseEnsuresConstraints
- (exprData_getSingle (data) ) );
+ exprNode_traverseFalseEnsuresConstraints
+ (exprData_getSingle (data)));
break;
case XPR_CALL:
ret = constraintList_addListFree (ret,
- exprNode_traversFalseEnsuresConstraints
- (exprData_getFcn (data) ) );
- /*@i11*/ /* exprNodeList_unparse (exprData_getArgs (data) ); */
+ exprNode_traverseFalseEnsuresConstraints
+ (exprData_getFcn (data)));
break;
case XPR_RETURN:
ret = constraintList_addListFree (ret,
- exprNode_traversFalseEnsuresConstraints
- (exprData_getSingle (data) ) );
+ exprNode_traverseFalseEnsuresConstraints
+ (exprData_getSingle (data)));
break;
case XPR_NULLRETURN:
case XPR_FACCESS:
ret = constraintList_addListFree (ret,
- exprNode_traversFalseEnsuresConstraints
- (exprData_getFieldNode (data) ) );
+ exprNode_traverseFalseEnsuresConstraints
+ (exprData_getFieldNode (data)));
break;
case XPR_ARROW:
ret = constraintList_addListFree (ret,
- exprNode_traversFalseEnsuresConstraints
- (exprData_getFieldNode (data) ) );
+ exprNode_traverseFalseEnsuresConstraints
+ (exprData_getFieldNode (data)));
break;
case XPR_STRINGLITERAL:
case XPR_POSTOP:
ret = constraintList_addListFree (ret,
- exprNode_traversFalseEnsuresConstraints
- (exprData_getUopNode (data) ) );
+ exprNode_traverseFalseEnsuresConstraints
+ (exprData_getUopNode (data)));
break;
case XPR_CAST:
ret = constraintList_addListFree (ret,
- exprNode_traversFalseEnsuresConstraints
- (exprData_getCastNode (data) ) );
+ exprNode_traverseFalseEnsuresConstraints
+ (exprData_getCastNode (data)));
break;
default:
/* walk down the tree and get all requires Constraints in each subexpression*/
-/*@only@*/ constraintList exprNode_traversRequiresConstraints (exprNode e)
+/*@only@*/ constraintList exprNode_traverseRequiresConstraints (exprNode e)
{
exprNode t1;
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_traverseRequiresConstraints (t1));
break;
case XPR_FETCH:
ret = constraintList_addListFree (ret,
- exprNode_traversRequiresConstraints
- (exprData_getPairA (data) ) );
+ exprNode_traverseRequiresConstraints
+ (exprData_getPairA (data)));
ret = constraintList_addListFree (ret,
- exprNode_traversRequiresConstraints
- (exprData_getPairB (data) ) );
+ exprNode_traverseRequiresConstraints
+ (exprData_getPairB (data)));
break;
case XPR_PREOP:
ret = constraintList_addListFree (ret,
- exprNode_traversRequiresConstraints
- (exprData_getUopNode (data) ) );
+ exprNode_traverseRequiresConstraints
+ (exprData_getUopNode (data)));
break;
case XPR_PARENS:
- ret = constraintList_addListFree (ret, exprNode_traversRequiresConstraints
- (exprData_getUopNode (data) ) );
+ ret = constraintList_addListFree (ret, exprNode_traverseRequiresConstraints
+ (exprData_getUopNode (data)));
break;
case XPR_INIT:
ret = constraintList_addListFree (ret,
- exprNode_traversRequiresConstraints
- (exprData_getInitNode (data) ) );
+ exprNode_traverseRequiresConstraints
+ (exprData_getInitNode (data)));
break;
case XPR_ASSIGN:
ret = constraintList_addListFree (ret,
- exprNode_traversRequiresConstraints
- (exprData_getOpA (data) ) );
+ exprNode_traverseRequiresConstraints
+ (exprData_getOpA (data)));
ret = constraintList_addListFree (ret,
- exprNode_traversRequiresConstraints
- (exprData_getOpB (data) ) );
+ exprNode_traverseRequiresConstraints
+ (exprData_getOpB (data)));
break;
case XPR_OP:
ret = constraintList_addListFree (ret,
- exprNode_traversRequiresConstraints
- (exprData_getOpA (data) ) );
+ exprNode_traverseRequiresConstraints
+ (exprData_getOpA (data)));
ret = constraintList_addListFree (ret,
- exprNode_traversRequiresConstraints
- (exprData_getOpB (data) ) );
+ exprNode_traverseRequiresConstraints
+ (exprData_getOpB (data)));
break;
case XPR_SIZEOFT:
break;
case XPR_SIZEOF:
ret = constraintList_addListFree (ret,
- exprNode_traversRequiresConstraints
- (exprData_getSingle (data) ) );
+ exprNode_traverseRequiresConstraints
+ (exprData_getSingle (data)));
break;
case XPR_CALL:
ret = constraintList_addListFree (ret,
- exprNode_traversRequiresConstraints
- (exprData_getFcn (data) ) );
- /*@i11*/ /* exprNodeList_unparse (exprData_getArgs (data) ); */
+ exprNode_traverseRequiresConstraints
+ (exprData_getFcn (data)));
break;
case XPR_RETURN:
ret = constraintList_addListFree (ret,
- exprNode_traversRequiresConstraints
- (exprData_getSingle (data) ) );
+ exprNode_traverseRequiresConstraints
+ (exprData_getSingle (data)));
break;
case XPR_NULLRETURN:
case XPR_FACCESS:
ret = constraintList_addListFree (ret,
- exprNode_traversRequiresConstraints
- (exprData_getFieldNode (data) ) );
+ exprNode_traverseRequiresConstraints
+ (exprData_getFieldNode (data)));
break;
case XPR_ARROW:
ret = constraintList_addListFree (ret,
- exprNode_traversRequiresConstraints
- (exprData_getFieldNode (data) ) );
+ exprNode_traverseRequiresConstraints
+ (exprData_getFieldNode (data)));
break;
case XPR_STRINGLITERAL:
case XPR_POSTOP:
ret = constraintList_addListFree (ret,
- exprNode_traversRequiresConstraints
- (exprData_getUopNode (data) ) );
+ exprNode_traverseRequiresConstraints
+ (exprData_getUopNode (data)));
break;
case XPR_CAST:
ret = constraintList_addListFree (ret,
- exprNode_traversRequiresConstraints
- (exprData_getCastNode (data) ) );
+ exprNode_traverseRequiresConstraints
+ (exprData_getCastNode (data)));
break;
default:
/* walk down the tree and get all Ensures Constraints in each subexpression*/
-/*@only@*/ constraintList exprNode_traversEnsuresConstraints (exprNode e)
+/*@only@*/ constraintList exprNode_traverseEnsuresConstraints (exprNode e)
{
exprNode t1;
exprData data;
constraintList ret;
-
- if (exprNode_handleError (e))
- {
- ret = constraintList_makeNew();
- return ret;
- }
-
- ret = constraintList_copy (e->ensuresConstraints );
- handledExprNode = TRUE;
-
+ if (exprNode_handleError (e))
+ {
+ ret = constraintList_makeNew();
+ return ret;
+ }
+
+ ret = constraintList_copy (e->ensuresConstraints);
+ handledExprNode = TRUE;
+
data = e->edata;
-
- DPRINTF((message (
- "exprnode_traversEnsuresConstraints call for %s with constraintList of %s",
+
+ DPRINTF ((message ("exprnode_traversEnsuresConstraints call for %s with "
+ "constraintList of %s",
exprNode_unparse (e),
- constraintList_print(e->ensuresConstraints)
+ constraintList_unparse(e->ensuresConstraints)
)
));
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_traverseEnsuresConstraints (t1));
break;
case XPR_FETCH:
-
ret = constraintList_addListFree (ret,
- exprNode_traversEnsuresConstraints
- (exprData_getPairA (data) ) );
-
+ exprNode_traverseEnsuresConstraints
+ (exprData_getPairA (data)));
+
ret = constraintList_addListFree (ret,
- exprNode_traversEnsuresConstraints
- (exprData_getPairB (data) ) );
+ exprNode_traverseEnsuresConstraints
+ (exprData_getPairB (data)));
break;
case XPR_PREOP:
-
ret = constraintList_addListFree (ret,
- exprNode_traversEnsuresConstraints
- (exprData_getUopNode (data) ) );
+ exprNode_traverseEnsuresConstraints
+ (exprData_getUopNode (data)));
break;
case XPR_PARENS:
- ret = constraintList_addListFree (ret, exprNode_traversEnsuresConstraints
- (exprData_getUopNode (data) ) );
+ ret = constraintList_addListFree (ret, exprNode_traverseEnsuresConstraints
+ (exprData_getUopNode (data)));
break;
case XPR_INIT:
ret = constraintList_addListFree (ret,
- exprNode_traversEnsuresConstraints
- (exprData_getInitNode (data) ) );
- break;
-
-
+ exprNode_traverseEnsuresConstraints
+ (exprData_getInitNode (data)));
+ break;
+
+
case XPR_ASSIGN:
- ret = constraintList_addListFree (ret,
- exprNode_traversEnsuresConstraints
- (exprData_getOpA (data) ) );
-
- ret = constraintList_addListFree (ret,
- exprNode_traversEnsuresConstraints
- (exprData_getOpB (data) ) );
- break;
+ ret = constraintList_addListFree (ret,
+ exprNode_traverseEnsuresConstraints
+ (exprData_getOpA (data)));
+
+ ret = constraintList_addListFree (ret,
+ exprNode_traverseEnsuresConstraints
+ (exprData_getOpB (data)));
+ break;
case XPR_OP:
- ret = constraintList_addListFree (ret,
- exprNode_traversEnsuresConstraints
- (exprData_getOpA (data) ) );
-
- ret = constraintList_addListFree (ret,
- exprNode_traversEnsuresConstraints
- (exprData_getOpB (data) ) );
- break;
+ ret = constraintList_addListFree (ret,
+ exprNode_traverseEnsuresConstraints
+ (exprData_getOpA (data)));
+
+ ret = constraintList_addListFree (ret,
+ exprNode_traverseEnsuresConstraints
+ (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_traverseEnsuresConstraints
+ (exprData_getSingle (data)));
+ break;
case XPR_CALL:
ret = constraintList_addListFree (ret,
- exprNode_traversEnsuresConstraints
- (exprData_getFcn (data) ) );
- /*@i11*/ /* exprNodeList_unparse (exprData_getArgs (data) ); */
+ exprNode_traverseEnsuresConstraints
+ (exprData_getFcn (data)));
break;
-
case XPR_RETURN:
ret = constraintList_addListFree (ret,
- exprNode_traversEnsuresConstraints
- (exprData_getSingle (data) ) );
+ exprNode_traverseEnsuresConstraints
+ (exprData_getSingle (data)));
break;
-
case XPR_NULLRETURN:
break;
-
case XPR_FACCESS:
ret = constraintList_addListFree (ret,
- exprNode_traversEnsuresConstraints
- (exprData_getFieldNode (data) ) );
+ exprNode_traverseEnsuresConstraints
+ (exprData_getFieldNode (data)));
break;
-
case XPR_ARROW:
ret = constraintList_addListFree (ret,
- exprNode_traversEnsuresConstraints
- (exprData_getFieldNode (data) ) );
+ exprNode_traverseEnsuresConstraints
+ (exprData_getFieldNode (data)));
break;
-
case XPR_STRINGLITERAL:
break;
-
case XPR_NUMLIT:
break;
case XPR_POSTOP:
-
- ret = constraintList_addListFree (ret,
- exprNode_traversEnsuresConstraints
- (exprData_getUopNode (data) ) );
- break;
+ ret = constraintList_addListFree (ret,
+ exprNode_traverseEnsuresConstraints
+ (exprData_getUopNode (data)));
+ break;
case XPR_CAST:
-
ret = constraintList_addListFree (ret,
- exprNode_traversEnsuresConstraints
- (exprData_getCastNode (data) ) );
+ exprNode_traverseEnsuresConstraints
+ (exprData_getCastNode (data)));
break;
-
default:
break;
}
-
- DPRINTF((message (
- "exprnode_traversEnsuresConstraints call for %s with constraintList of is returning %s",
- exprNode_unparse (e),
- constraintList_print(ret))));
+
+ DPRINTF((message ("exprnode_traversEnsuresConstraints call for %s with "
+ "constraintList of is returning %s",
+ exprNode_unparse (e),
+ constraintList_unparse(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)
{
+
+ llassert(temp != NULL );
+
temp->requiresConstraints = constraintList_makeNew();
temp->ensuresConstraints = constraintList_makeNew();
temp->trueEnsuresConstraints = constraintList_makeNew();
exprNodeList_elements (arglist, el)
{
constraintList temp2;
+
+ llassert(exprNode_isDefined(el) );
+
exprNode_exprTraverse (el, FALSE, FALSE, sequencePoint);
temp2 = el->requiresConstraints;
- el->requiresConstraints = exprNode_traversRequiresConstraints(el);
+ el->requiresConstraints = exprNode_traverseRequiresConstraints(el);
constraintList_free(temp2);
temp2 = el->ensuresConstraints;
- el->ensuresConstraints = exprNode_traversEnsuresConstraints(el);
+ el->ensuresConstraints = exprNode_traverseEnsuresConstraints(el);
constraintList_free(temp2);
temp->requiresConstraints = constraintList_addList(temp->requiresConstraints,
{
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);
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))
+ DPRINTF((message("Found structure %s", exprNode_unparse(expr))
+ ));
+ if (hasInvariants(ct))
+ {
+ constraintList invars;
+
+ invars = getInvariants(ct);
+
+
+ DPRINTF((message ("findStructs has invariants %s ", constraintList_unparse (invars))
+ ));
+
+ invars = constraintList_doSRefFixStructConstraint(invars, exprNode_getSref(expr), ct);
+
+
+ DPRINTF((message ("findStructs finded invariants to be %s ", constraintList_unparse (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);
}
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) ) ));
+
+ if (context_getFlag (FLG_IMPBOUNDSCONSTRAINTS))
+ {
+
+ /*
+ uentryList_elements (arglist, el)
+ {
+ sRef s;
+ DPRINTF((message("setImplicitfcnConstraints 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_unparseDetailed(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;
}
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)
+void exprNode_findValue(exprNode e)
{
exprData data;
exprNode t1, t2;
lltok tok;
+ llassert(exprNode_isDefined(e) );
+
data = e->edata;
- if (exprNode_hasValue(e) )
+ if (exprNode_hasValue(e))
return;
if (e->kind == XPR_OP)
exprNode_findValue(t1);
exprNode_findValue(t2);
- if (!(exprNode_knownIntValue(t1) && (exprNode_knownIntValue(t2) ) ) )
+ if (!(exprNode_knownIntValue(t1) && (exprNode_knownIntValue(t2))))
return;
- if (lltok_isPlus_Op (tok) )
+ if (lltok_isPlus_Op (tok))
{
long v1, v2;
v1 = exprNode_getLongValue(t1);
v2 = exprNode_getLongValue(t2);
- if (multiVal_isDefined(e->val) )
+ if (multiVal_isDefined(e->val))
multiVal_free (e->val);
e->val = multiVal_makeInt (v1 + v2);
}
- if ( lltok_isMinus_Op (tok) )
+ if (lltok_isMinus_Op (tok))
{
long v1, v2;
v1 = exprNode_getLongValue(t1);
v2 = exprNode_getLongValue(t2);
- if (multiVal_isDefined(e->val) )
- multiVal_free (e->val);
+ if (multiVal_isDefined(e->val))
+ {
+ multiVal_free (e->val);
+ }
e->val = multiVal_makeInt (v1 - v2);
}
andersk / splint.git / blobdiff