/*
** 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
# include "exprChecks.h"
# include "exprNodeSList.h"
-/*@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! */
+/*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 /*@truewhennull@*/ bool exprNode_handleError (/*@temp@*/ exprNode p_e);
+static /*@nullwhentrue@*/ bool exprNode_handleError (/*@temp@*/ exprNode p_e);
static void exprNode_stmt (/*@temp@*/ /*@temp@*/ exprNode p_e);
static void exprNode_multiStatement (/*@temp@*/ exprNode p_e);
-static constraintList exprNode_traversTrueEnsuresConstraints (/*@temp@*/ exprNode p_e);
-static constraintList exprNode_traversFalseEnsuresConstraints (/*@temp@*/ 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 (/*@temp@*/ exprNode p_fcn, exprNodeList p_arglist);
+static constraintList checkCall (/*@temp@*/ exprNode p_fcn, exprNodeList p_arglist);
static bool exprNode_isUnhandled (/*@temp@*/ /*@observer@*/ exprNode e)
{
return FALSE;
}
-bool exprNode_handleError (exprNode e)
+/*@nullwhentrue@*/ bool exprNode_handleError (exprNode e)
{
if (exprNode_isError (e) || exprNode_isUnhandled (e))
{
return FALSE;
}
- DPRINTF((message ("exprNode_generateConstraints Analysising %s at %s", exprNode_unparse(e),
- fileloc_unparse(exprNode_getfileloc(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))));
+
+ DPRINTF ((message ("e->requiresConstraints %s",
+ constraintList_unparseDetailed (e->requiresConstraints))));
return FALSE;
}
{
exprNode snode;
fileloc loc;
- cstring s;
+ 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;
}
fileloc_free(loc);
tempList = e->requiresConstraints;
- e->requiresConstraints = exprNode_traversRequiresConstraints(e);
+ e->requiresConstraints = exprNode_traverseRequiresConstraints(e);
constraintList_free(tempList);
}
if (e->kind != XPR_STMT)
{
-
DPRINTF (("Not Stmt"));
DPRINTF ((message ("%s ", exprNode_unparse (e))));
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;
}
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;
}
DPRINTF ((message ("doIf: %s ", exprNode_unparse(e))));
- llassert(exprNode_isDefined(test));
+ 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);
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_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;
}
end_sRefSet_elements ;
DPRINTF((message("constraintList_makeFixedArrayConstraints returning %s",
- constraintList_print(ret))));
+ constraintList_unparse(ret))));
return ret;
}
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;
*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@*/
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 */
+ /* evans 2002-01-01: spurious warnings for these becuase of stack allocated storage */
exprNode_doGenerateConstraintSwitch (switchExpr, body, &lastRequires,
&lastEnsures, &constraintsRequires, &constraintsEnsures);
/*@=mustfree@*/
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)
)
)));
}
constraintList temp;
DPRINTF((message ("exprNode_multistatement Analysising %s %s at", exprNode_unparse(e),
- fileloc_unparse(exprNode_getfileloc(e)))));
+ fileloc_unparse(exprNode_getNextSequencePoint(e)))));
if (exprNode_handleError (e))
{
{
constraintList temp2;
temp2 = test->trueEnsuresConstraints;
- test->trueEnsuresConstraints = exprNode_traversTrueEnsuresConstraints(test);
+ test->trueEnsuresConstraints = exprNode_traverseTrueEnsuresConstraints(test);
constraintList_free(temp2);
}
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_print(p->trueEnsuresConstraints) )
+ 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_print(p->trueEnsuresConstraints) )
+ 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);
/*See comment on trueEnsures*/
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:
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;
}
}
-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))
return;
}
- DPRINTF((message ("exprNode_exprTraverset Analysising %s %s at", exprNode_unparse(e),
- fileloc_unparse(exprNode_getfileloc(e)))));
+ DPRINTF (("exprNode_exprTraverse analyzing %s at %s",
+ exprNode_unparse (e),
+ fileloc_unparse (exprNode_loc (e))));
- /*e->requiresConstraints = constraintList_makeNew();
- e->ensuresConstraints = constraintList_makeNew();
- e->trueEnsuresConstraints = constraintList_makeNew();;
- e->falseEnsuresConstraints = constraintList_makeNew();;
- */
-
if (exprNode_isUnhandled (e))
- {
- return;
- }
-
- handledExprNode = TRUE;
+ {
+ return;
+ }
data = e->edata;
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)
- )
- ))); */
+
+ DPRINTF (("initialization ==> %s",exprNode_unparse (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)))
+ /* 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);
+ 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)))
+ /* 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:
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;
fcn = exprData_getFcn(data);
exprNode_exprTraverse (fcn, definatelv, definaterv, sequencePoint);
- DPRINTF ((message ("Got call that %s (%s) ", exprNode_unparse(fcn), exprNodeList_unparse (exprData_getArgs (data)))));
-
- fcn->requiresConstraints = constraintList_addListFree (fcn->requiresConstraints,
- checkCall (fcn, exprData_getArgs (data) ));
-
- fcn->ensuresConstraints = constraintList_addListFree (fcn->ensuresConstraints,
- exprNode_getPostConditions(fcn, exprData_getArgs (data),e ));
+ DPRINTF (("Got call that %s (%s)",
+ exprNode_unparse(fcn), exprNodeList_unparse (exprData_getArgs (data))));
+ 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);
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);
/*handle * pointer access */
{
break;
}
+ else if (lltok_isPlus_Op (tok))
+ {
+ break;
+ }
else if (lltok_isExcl_Op (tok))
{
break;
exprNode_exprTraverse (pred, FALSE, TRUE, sequencePoint);
temp = pred->ensuresConstraints;
- pred->ensuresConstraints = exprNode_traversEnsuresConstraints(pred);
+ pred->ensuresConstraints = exprNode_traverseEnsuresConstraints(pred);
constraintList_free(temp);
temp = pred->requiresConstraints;
- pred->requiresConstraints = exprNode_traversRequiresConstraints(pred);
+ pred->requiresConstraints = exprNode_traverseRequiresConstraints(pred);
constraintList_free(temp);
temp = pred->trueEnsuresConstraints;
- pred->trueEnsuresConstraints = exprNode_traversTrueEnsuresConstraints(pred);
+ pred->trueEnsuresConstraints = exprNode_traverseTrueEnsuresConstraints(pred);
constraintList_free(temp);
temp = pred->falseEnsuresConstraints;
- pred->falseEnsuresConstraints = exprNode_traversFalseEnsuresConstraints(pred);
+ pred->falseEnsuresConstraints = exprNode_traverseFalseEnsuresConstraints(pred);
constraintList_free(temp);
exprNode_exprTraverse (trueBranch, FALSE, TRUE, sequencePoint);
temp = trueBranch->ensuresConstraints;
- trueBranch->ensuresConstraints = exprNode_traversEnsuresConstraints(trueBranch);
+ trueBranch->ensuresConstraints = exprNode_traverseEnsuresConstraints(trueBranch);
constraintList_free(temp);
temp = trueBranch->requiresConstraints;
- trueBranch->requiresConstraints = exprNode_traversRequiresConstraints(trueBranch);
+ trueBranch->requiresConstraints = exprNode_traverseRequiresConstraints(trueBranch);
constraintList_free(temp);
-
- temp = trueBranch->trueEnsuresConstraints;
- trueBranch->trueEnsuresConstraints = exprNode_traversTrueEnsuresConstraints(trueBranch);
+ temp = trueBranch->trueEnsuresConstraints;
+ trueBranch->trueEnsuresConstraints = exprNode_traverseTrueEnsuresConstraints(trueBranch);
constraintList_free(temp);
- temp = trueBranch->falseEnsuresConstraints;
- trueBranch->falseEnsuresConstraints = exprNode_traversFalseEnsuresConstraints(trueBranch);
+ temp = trueBranch->falseEnsuresConstraints;
+ trueBranch->falseEnsuresConstraints = exprNode_traverseFalseEnsuresConstraints(trueBranch);
constraintList_free(temp);
exprNode_exprTraverse (falseBranch, FALSE, TRUE, sequencePoint);
temp = falseBranch->ensuresConstraints;
- falseBranch->ensuresConstraints = exprNode_traversEnsuresConstraints(falseBranch);
+ falseBranch->ensuresConstraints = exprNode_traverseEnsuresConstraints(falseBranch);
constraintList_free(temp);
temp = falseBranch->requiresConstraints;
- falseBranch->requiresConstraints = exprNode_traversRequiresConstraints(falseBranch);
+ falseBranch->requiresConstraints = exprNode_traverseRequiresConstraints(falseBranch);
constraintList_free(temp);
temp = falseBranch->trueEnsuresConstraints;
- falseBranch->trueEnsuresConstraints = exprNode_traversTrueEnsuresConstraints(falseBranch);
+ falseBranch->trueEnsuresConstraints = exprNode_traverseTrueEnsuresConstraints(falseBranch);
constraintList_free(temp);
temp = falseBranch->falseEnsuresConstraints;
- falseBranch->falseEnsuresConstraints = exprNode_traversFalseEnsuresConstraints(falseBranch);
+ falseBranch->falseEnsuresConstraints = exprNode_traverseFalseEnsuresConstraints(falseBranch);
constraintList_free(temp);
/* if pred is true e equals true otherwise pred equals false */
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../ */
+ /* 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_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->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;
{
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
+ exprNode_traverseTrueEnsuresConstraints
(exprData_getPairA (data)));
ret = constraintList_addListFree (ret,
- exprNode_traversTrueEnsuresConstraints
+ exprNode_traverseTrueEnsuresConstraints
(exprData_getPairB (data)));
break;
case XPR_PREOP:
ret = constraintList_addListFree (ret,
- exprNode_traversTrueEnsuresConstraints
+ exprNode_traverseTrueEnsuresConstraints
(exprData_getUopNode (data)));
break;
case XPR_PARENS:
- ret = constraintList_addListFree (ret, exprNode_traversTrueEnsuresConstraints
+ ret = constraintList_addListFree (ret, exprNode_traverseTrueEnsuresConstraints
(exprData_getUopNode (data)));
break;
case XPR_INIT:
ret = constraintList_addListFree (ret,
- exprNode_traversTrueEnsuresConstraints
+ exprNode_traverseTrueEnsuresConstraints
(exprData_getInitNode (data)));
break;
case XPR_ASSIGN:
ret = constraintList_addListFree (ret,
- exprNode_traversTrueEnsuresConstraints
+ exprNode_traverseTrueEnsuresConstraints
(exprData_getOpA (data)));
ret = constraintList_addListFree (ret,
- exprNode_traversTrueEnsuresConstraints
+ exprNode_traverseTrueEnsuresConstraints
(exprData_getOpB (data)));
break;
case XPR_OP:
ret = constraintList_addListFree (ret,
- exprNode_traversTrueEnsuresConstraints
+ exprNode_traverseTrueEnsuresConstraints
(exprData_getOpA (data)));
ret = constraintList_addListFree (ret,
- exprNode_traversTrueEnsuresConstraints
+ exprNode_traverseTrueEnsuresConstraints
(exprData_getOpB (data)));
break;
case XPR_SIZEOFT:
case XPR_SIZEOF:
ret = constraintList_addListFree (ret,
- exprNode_traversTrueEnsuresConstraints
+ exprNode_traverseTrueEnsuresConstraints
(exprData_getSingle (data)));
break;
case XPR_CALL:
ret = constraintList_addListFree (ret,
- exprNode_traversTrueEnsuresConstraints
+ exprNode_traverseTrueEnsuresConstraints
(exprData_getFcn (data)));
- /*@i11*/ /* exprNodeList_unparse (exprData_getArgs (data)); */
break;
case XPR_RETURN:
ret = constraintList_addListFree (ret,
- exprNode_traversTrueEnsuresConstraints
+ exprNode_traverseTrueEnsuresConstraints
(exprData_getSingle (data)));
break;
case XPR_FACCESS:
ret = constraintList_addListFree (ret,
- exprNode_traversTrueEnsuresConstraints
+ exprNode_traverseTrueEnsuresConstraints
(exprData_getFieldNode (data)));
break;
case XPR_ARROW:
ret = constraintList_addListFree (ret,
- exprNode_traversTrueEnsuresConstraints
+ exprNode_traverseTrueEnsuresConstraints
(exprData_getFieldNode (data)));
break;
case XPR_POSTOP:
ret = constraintList_addListFree (ret,
- exprNode_traversTrueEnsuresConstraints
+ exprNode_traverseTrueEnsuresConstraints
(exprData_getUopNode (data)));
break;
case XPR_CAST:
ret = constraintList_addListFree (ret,
- exprNode_traversTrueEnsuresConstraints
+ exprNode_traverseTrueEnsuresConstraints
(exprData_getCastNode (data)));
break;
return ret;
}
-constraintList exprNode_traversFalseEnsuresConstraints (exprNode e)
+constraintList exprNode_traverseFalseEnsuresConstraints (exprNode e)
{
exprNode t1;
bool handledExprNode;
{
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
+ exprNode_traverseFalseEnsuresConstraints
(exprData_getPairA (data)));
ret = constraintList_addListFree (ret,
- exprNode_traversFalseEnsuresConstraints
+ exprNode_traverseFalseEnsuresConstraints
(exprData_getPairB (data)));
break;
case XPR_PREOP:
ret = constraintList_addListFree (ret,
- exprNode_traversFalseEnsuresConstraints
+ exprNode_traverseFalseEnsuresConstraints
(exprData_getUopNode (data)));
break;
case XPR_PARENS:
- ret = constraintList_addListFree (ret, exprNode_traversFalseEnsuresConstraints
+ ret = constraintList_addListFree (ret, exprNode_traverseFalseEnsuresConstraints
(exprData_getUopNode (data)));
break;
case XPR_INIT:
ret = constraintList_addListFree (ret,
- exprNode_traversFalseEnsuresConstraints
+ exprNode_traverseFalseEnsuresConstraints
( exprData_getInitNode (data)));
break;
case XPR_ASSIGN:
ret = constraintList_addListFree (ret,
- exprNode_traversFalseEnsuresConstraints
+ exprNode_traverseFalseEnsuresConstraints
(exprData_getOpA (data)));
ret = constraintList_addListFree (ret,
- exprNode_traversFalseEnsuresConstraints
+ exprNode_traverseFalseEnsuresConstraints
(exprData_getOpB (data)));
break;
case XPR_OP:
ret = constraintList_addListFree (ret,
- exprNode_traversFalseEnsuresConstraints
+ exprNode_traverseFalseEnsuresConstraints
(exprData_getOpA (data)));
ret = constraintList_addListFree (ret,
- exprNode_traversFalseEnsuresConstraints
+ exprNode_traverseFalseEnsuresConstraints
(exprData_getOpB (data)));
break;
case XPR_SIZEOFT:
case XPR_SIZEOF:
ret = constraintList_addListFree (ret,
- exprNode_traversFalseEnsuresConstraints
+ exprNode_traverseFalseEnsuresConstraints
(exprData_getSingle (data)));
break;
case XPR_CALL:
ret = constraintList_addListFree (ret,
- exprNode_traversFalseEnsuresConstraints
+ exprNode_traverseFalseEnsuresConstraints
(exprData_getFcn (data)));
- /*@i11*/ /* exprNodeList_unparse (exprData_getArgs (data)); */
break;
case XPR_RETURN:
ret = constraintList_addListFree (ret,
- exprNode_traversFalseEnsuresConstraints
+ exprNode_traverseFalseEnsuresConstraints
(exprData_getSingle (data)));
break;
case XPR_FACCESS:
ret = constraintList_addListFree (ret,
- exprNode_traversFalseEnsuresConstraints
+ exprNode_traverseFalseEnsuresConstraints
(exprData_getFieldNode (data)));
break;
case XPR_ARROW:
ret = constraintList_addListFree (ret,
- exprNode_traversFalseEnsuresConstraints
+ exprNode_traverseFalseEnsuresConstraints
(exprData_getFieldNode (data)));
break;
case XPR_POSTOP:
ret = constraintList_addListFree (ret,
- exprNode_traversFalseEnsuresConstraints
+ exprNode_traverseFalseEnsuresConstraints
(exprData_getUopNode (data)));
break;
case XPR_CAST:
ret = constraintList_addListFree (ret,
- exprNode_traversFalseEnsuresConstraints
+ exprNode_traverseFalseEnsuresConstraints
(exprData_getCastNode (data)));
break;
/* 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;
{
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
+ exprNode_traverseRequiresConstraints
(exprData_getPairA (data)));
ret = constraintList_addListFree (ret,
- exprNode_traversRequiresConstraints
+ exprNode_traverseRequiresConstraints
(exprData_getPairB (data)));
break;
case XPR_PREOP:
ret = constraintList_addListFree (ret,
- exprNode_traversRequiresConstraints
+ exprNode_traverseRequiresConstraints
(exprData_getUopNode (data)));
break;
case XPR_PARENS:
- ret = constraintList_addListFree (ret, exprNode_traversRequiresConstraints
+ ret = constraintList_addListFree (ret, exprNode_traverseRequiresConstraints
(exprData_getUopNode (data)));
break;
case XPR_INIT:
ret = constraintList_addListFree (ret,
- exprNode_traversRequiresConstraints
+ exprNode_traverseRequiresConstraints
(exprData_getInitNode (data)));
break;
case XPR_ASSIGN:
ret = constraintList_addListFree (ret,
- exprNode_traversRequiresConstraints
+ exprNode_traverseRequiresConstraints
(exprData_getOpA (data)));
ret = constraintList_addListFree (ret,
- exprNode_traversRequiresConstraints
+ exprNode_traverseRequiresConstraints
(exprData_getOpB (data)));
break;
case XPR_OP:
ret = constraintList_addListFree (ret,
- exprNode_traversRequiresConstraints
+ exprNode_traverseRequiresConstraints
(exprData_getOpA (data)));
ret = constraintList_addListFree (ret,
- exprNode_traversRequiresConstraints
+ exprNode_traverseRequiresConstraints
(exprData_getOpB (data)));
break;
case XPR_SIZEOFT:
case XPR_SIZEOF:
ret = constraintList_addListFree (ret,
- exprNode_traversRequiresConstraints
+ exprNode_traverseRequiresConstraints
(exprData_getSingle (data)));
break;
case XPR_CALL:
ret = constraintList_addListFree (ret,
- exprNode_traversRequiresConstraints
+ exprNode_traverseRequiresConstraints
(exprData_getFcn (data)));
- /*@i11*/ /* exprNodeList_unparse (exprData_getArgs (data)); */
break;
case XPR_RETURN:
ret = constraintList_addListFree (ret,
- exprNode_traversRequiresConstraints
+ exprNode_traverseRequiresConstraints
(exprData_getSingle (data)));
break;
case XPR_FACCESS:
ret = constraintList_addListFree (ret,
- exprNode_traversRequiresConstraints
+ exprNode_traverseRequiresConstraints
(exprData_getFieldNode (data)));
break;
case XPR_ARROW:
ret = constraintList_addListFree (ret,
- exprNode_traversRequiresConstraints
+ exprNode_traverseRequiresConstraints
(exprData_getFieldNode (data)));
break;
case XPR_POSTOP:
ret = constraintList_addListFree (ret,
- exprNode_traversRequiresConstraints
+ exprNode_traverseRequiresConstraints
(exprData_getUopNode (data)));
break;
case XPR_CAST:
ret = constraintList_addListFree (ret,
- exprNode_traversRequiresConstraints
+ exprNode_traverseRequiresConstraints
(exprData_getCastNode (data)));
break;
/* 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;
DPRINTF ((message ("exprnode_traversEnsuresConstraints call for %s with "
"constraintList of %s",
exprNode_unparse (e),
- constraintList_print(e->ensuresConstraints)
+ constraintList_unparse(e->ensuresConstraints)
)
));
{
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
+ exprNode_traverseEnsuresConstraints
(exprData_getPairA (data)));
ret = constraintList_addListFree (ret,
- exprNode_traversEnsuresConstraints
+ exprNode_traverseEnsuresConstraints
(exprData_getPairB (data)));
break;
case XPR_PREOP:
ret = constraintList_addListFree (ret,
- exprNode_traversEnsuresConstraints
+ exprNode_traverseEnsuresConstraints
(exprData_getUopNode (data)));
break;
case XPR_PARENS:
- ret = constraintList_addListFree (ret, exprNode_traversEnsuresConstraints
+ ret = constraintList_addListFree (ret, exprNode_traverseEnsuresConstraints
(exprData_getUopNode (data)));
break;
case XPR_INIT:
ret = constraintList_addListFree (ret,
- exprNode_traversEnsuresConstraints
+ exprNode_traverseEnsuresConstraints
(exprData_getInitNode (data)));
break;
case XPR_ASSIGN:
ret = constraintList_addListFree (ret,
- exprNode_traversEnsuresConstraints
+ exprNode_traverseEnsuresConstraints
(exprData_getOpA (data)));
ret = constraintList_addListFree (ret,
- exprNode_traversEnsuresConstraints
+ exprNode_traverseEnsuresConstraints
(exprData_getOpB (data)));
break;
case XPR_OP:
ret = constraintList_addListFree (ret,
- exprNode_traversEnsuresConstraints
+ exprNode_traverseEnsuresConstraints
(exprData_getOpA (data)));
ret = constraintList_addListFree (ret,
- exprNode_traversEnsuresConstraints
+ exprNode_traverseEnsuresConstraints
(exprData_getOpB (data)));
break;
case XPR_SIZEOFT:
case XPR_SIZEOF:
ret = constraintList_addListFree (ret,
- exprNode_traversEnsuresConstraints
+ exprNode_traverseEnsuresConstraints
(exprData_getSingle (data)));
break;
case XPR_CALL:
ret = constraintList_addListFree (ret,
- exprNode_traversEnsuresConstraints
+ exprNode_traverseEnsuresConstraints
(exprData_getFcn (data)));
- /*@i11*/ /* exprNodeList_unparse (exprData_getArgs (data)); */
break;
case XPR_RETURN:
ret = constraintList_addListFree (ret,
- exprNode_traversEnsuresConstraints
+ exprNode_traverseEnsuresConstraints
(exprData_getSingle (data)));
break;
case XPR_NULLRETURN:
break;
case XPR_FACCESS:
ret = constraintList_addListFree (ret,
- exprNode_traversEnsuresConstraints
+ exprNode_traverseEnsuresConstraints
(exprData_getFieldNode (data)));
break;
case XPR_ARROW:
ret = constraintList_addListFree (ret,
- exprNode_traversEnsuresConstraints
+ exprNode_traverseEnsuresConstraints
(exprData_getFieldNode (data)));
break;
case XPR_STRINGLITERAL:
break;
case XPR_POSTOP:
ret = constraintList_addListFree (ret,
- exprNode_traversEnsuresConstraints
+ exprNode_traverseEnsuresConstraints
(exprData_getUopNode (data)));
break;
case XPR_CAST:
ret = constraintList_addListFree (ret,
- exprNode_traversEnsuresConstraints
+ exprNode_traverseEnsuresConstraints
(exprData_getCastNode (data)));
break;
default:
DPRINTF((message ("exprnode_traversEnsuresConstraints call for %s with "
"constraintList of is returning %s",
exprNode_unparse (e),
- constraintList_print(ret))));
+ constraintList_unparse(ret))));
return ret;
}
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,
rt = ctype_realType (ct);
if (ctype_isStruct (rt))
- TPRINTF((message("Found structure %s", exprNode_unparse(expr))
+ DPRINTF((message("Found structure %s", exprNode_unparse(expr))
));
if (hasInvariants(ct))
{
invars = getInvariants(ct);
- TPRINTF((message ("findStructs has invariants %s ", constraintList_print (invars))
+ DPRINTF((message ("findStructs has invariants %s ", constraintList_unparse (invars))
));
invars = constraintList_doSRefFixStructConstraint(invars, exprNode_getSref(expr), ct);
- TPRINTF((message ("findStructs finded invariants to be %s ", constraintList_print (invars))
+ DPRINTF((message ("findStructs finded invariants to be %s ", constraintList_unparse (invars))
));
}
}
preconditions = constraintList_makeNew();
}
- if (context_getFlag (FLG_IMPLICTCONSTRAINT) )
+ if (context_getFlag (FLG_IMPBOUNDSCONSTRAINTS))
{
/*
uentryList_elements (arglist, el)
{
sRef s;
- TPRINTF((message("setImplictfcnConstraints doing: %s", uentry_unparse(el) ) ));
+ DPRINTF((message("setImplicitfcnConstraints doing: %s", uentry_unparse(el) ) ));
s = uentry_getSref(el);
if (sRef_isReference (s) )
{
- TPRINTF((message ("%s is a pointer", sRef_unparse(s) ) ));
+ DPRINTF((message ("%s is a pointer", sRef_unparse(s) ) ));
}
else
{
- TPRINTF((message ("%s is NOT a pointer", sRef_unparse(s) ) ));
+ DPRINTF((message ("%s is NOT a pointer", sRef_unparse(s) ) ));
}
//drl 4/26/01
//chagned this from MaxSet(s) == 0 to MaxSet(s) >= 0
}
DPRINTF ((message("Done checkCall\n")));
- DPRINTF ((message("Returning list %q ", constraintList_printDetailed(preconditions))));
+ DPRINTF ((message("Returning list %q ", constraintList_unparseDetailed(preconditions))));
/*
drl we're going to comment this out for now
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;
+ llassert(exprNode_isDefined(e) );
+
data = e->edata;
if (exprNode_hasValue(e))
andersk / splint.git / blobdiff