+ exprNode_generateConstraints (exprData_getTripleInc (data));
+ break;
+
+ case XPR_WHILE:
+ e1 = exprData_getPairA (data);
+ e2 = exprData_getPairB (data);
+
+ exprNode_exprTraverse (e1,
+ FALSE, FALSE, exprNode_loc(e1));
+
+ exprNode_generateConstraints (e2);
+
+ e = doWhile (e, e1, e2);
+
+ break;
+
+ case XPR_IF:
+ DPRINTF(("IF:"));
+ DPRINTF ((exprNode_unparse(e)));
+ e1 = exprData_getPairA (data);
+ e2 = exprData_getPairB (data);
+
+ exprNode_exprTraverse (e1, FALSE, FALSE, exprNode_loc(e1));
+
+ exprNode_generateConstraints (e2);
+ e = doIf (e, e1, e2);
+ break;
+
+ case XPR_IFELSE:
+ DPRINTF(("Starting IFELSE"));
+ p = exprData_getTriplePred (data);
+
+ trueBranch = exprData_getTripleTrue (data);
+ falseBranch = exprData_getTripleFalse (data);
+
+ exprNode_exprTraverse (p,
+ FALSE, FALSE, exprNode_loc(p));
+ exprNode_generateConstraints (trueBranch);
+ exprNode_generateConstraints (falseBranch);
+
+ llassert (exprNode_isDefined (p));
+ temp = p->ensuresConstraints;
+ p->ensuresConstraints = exprNode_traversEnsuresConstraints (p);
+ constraintList_free(temp);
+
+ temp = p->requiresConstraints;
+ p->requiresConstraints = exprNode_traversRequiresConstraints (p);
+ constraintList_free(temp);
+
+ temp = p->trueEnsuresConstraints;
+ p->trueEnsuresConstraints = exprNode_traversTrueEnsuresConstraints(p);
+ constraintList_free(temp);
+
+
+
+ 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);
+ constraintList_free(temp);
+
+ /*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))));
+ exprNode_generateConstraints (e2);
+ exprNode_generateConstraints (e1);
+ e = exprNode_copyConstraints (e, e2);
+ DPRINTF ((message ("e = %s ", constraintList_unparse(e->requiresConstraints))));
+
+ break;
+
+ case XPR_BLOCK:
+ {
+ 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:
+ e = doSwitch (e);
+ break;
+ case XPR_STMT:
+ case XPR_STMTLIST:
+ exprNode_stmtList (e);
+ return ;
+ /*@notreached@*/
+ break;
+ default:
+ ret=FALSE;
+ }
+ return;
+}
+
+static bool lltok_isBoolean_Op (lltok tok)
+{
+ /*this should really be a switch statement but
+ I don't want to violate the abstraction
+ maybe this should go in lltok.c */
+
+ if (lltok_isEqOp (tok))
+ {
+ return TRUE;
+ }
+ if (lltok_isAndOp (tok))
+
+ {
+
+ return TRUE;
+ }
+ if (lltok_isOrOp (tok))
+ {
+ return TRUE;
+ }
+
+ if (lltok_isGt_Op (tok))
+ {
+ return TRUE;
+ }
+ if (lltok_isLt_Op (tok))
+ {
+ return TRUE;
+ }
+
+ if (lltok_isLe_Op (tok))
+ {
+ return TRUE;
+ }
+
+ if (lltok_isGe_Op (tok))
+ {
+ return TRUE;
+ }
+
+ return FALSE;
+
+}
+
+
+static void exprNode_booleanTraverse (/*@dependent@*/ exprNode e, /*@unused@*/ bool definatelv, /*@unused@*/ bool definaterv, fileloc sequencePoint)
+{
+ constraint cons;
+ exprNode t1, t2;
+ exprData data;
+ lltok tok;
+ constraintList tempList, temp;
+
+ 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_isEqOp (tok))
+ {
+ cons = constraint_makeEnsureEqual (t1, t2, sequencePoint);
+ e->trueEnsuresConstraints = constraintList_add(e->trueEnsuresConstraints, cons);
+ }
+
+
+ if (lltok_isLt_Op (tok))
+ {
+ cons = constraint_makeEnsureLessThan (t1, t2, sequencePoint);
+ e->trueEnsuresConstraints = constraintList_add(e->trueEnsuresConstraints, cons);
+ cons = constraint_makeEnsureGreaterThanEqual (t1, t2, sequencePoint);
+ e->falseEnsuresConstraints = constraintList_add(e->falseEnsuresConstraints, cons);
+ }
+
+ if (lltok_isGe_Op (tok))
+ {
+ cons = constraint_makeEnsureGreaterThanEqual (t1, t2, sequencePoint);
+ e->trueEnsuresConstraints = constraintList_add(e->trueEnsuresConstraints, cons);
+
+ cons = constraint_makeEnsureLessThan (t1, t2, sequencePoint);
+ e->falseEnsuresConstraints = constraintList_add(e->falseEnsuresConstraints, cons);
+ }
+
+ if (lltok_isGt_Op (tok))
+ {
+ cons = constraint_makeEnsureGreaterThan (t1, t2, sequencePoint);
+ e->trueEnsuresConstraints = constraintList_add(e->trueEnsuresConstraints, cons);
+ cons = constraint_makeEnsureLessThanEqual (t1, t2, sequencePoint);
+ e->falseEnsuresConstraints = constraintList_add(e->falseEnsuresConstraints, cons);
+ }
+
+ if (lltok_isLe_Op (tok))
+ {
+ cons = constraint_makeEnsureLessThanEqual (t1, t2, sequencePoint);
+ e->trueEnsuresConstraints = constraintList_add(e->trueEnsuresConstraints, cons);
+
+ cons = constraint_makeEnsureGreaterThan (t1, t2, sequencePoint);
+ e->falseEnsuresConstraints = constraintList_add(e->falseEnsuresConstraints, cons);
+ }
+
+ /* Logical operations */
+
+ if (lltok_isAndOp (tok))
+ {
+ /* true ensures */
+ tempList = constraintList_copy (t1->trueEnsuresConstraints);
+ tempList = constraintList_addList (tempList, t2->trueEnsuresConstraints);
+ e->trueEnsuresConstraints = constraintList_addListFree(e->trueEnsuresConstraints, tempList);
+
+ /* false ensures: fens t1 or tens t1 and fens t2 */
+ tempList = constraintList_copy (t1->trueEnsuresConstraints);
+ tempList = constraintList_addList (tempList, t2->falseEnsuresConstraints);
+ temp = tempList;
+ tempList = constraintList_logicalOr (tempList, t1->falseEnsuresConstraints);
+ constraintList_free (temp);
+
+ /* evans - was constraintList_addList - memory leak detected by splint */
+ e->falseEnsuresConstraints = constraintList_addListFree (e->falseEnsuresConstraints, tempList);
+ }
+ else if (lltok_isOrOp (tok))
+ {
+ /* false ensures */
+ tempList = constraintList_copy (t1->falseEnsuresConstraints);
+ tempList = constraintList_addList (tempList, t2->falseEnsuresConstraints);
+ e->falseEnsuresConstraints = constraintList_addListFree(e->falseEnsuresConstraints, tempList);
+
+ /* true ensures: tens t1 or fens t1 and tens t2 */
+ tempList = constraintList_copy (t1->falseEnsuresConstraints);
+ tempList = constraintList_addList (tempList, t2->trueEnsuresConstraints);
+
+ temp = tempList;
+ tempList = constraintList_logicalOr (tempList, t1->trueEnsuresConstraints);
+ constraintList_free(temp);
+
+ e->trueEnsuresConstraints = constraintList_addListFree(e->trueEnsuresConstraints, tempList);
+ tempList = constraintList_undefined;
+ }
+ else
+ {
+ DPRINTF((message("%s is not a boolean operation", lltok_unparse(tok))));
+ }
+}
+
+void exprNode_exprTraverse (/*@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)))));
+
+ /*e->requiresConstraints = constraintList_makeNew();
+ e->ensuresConstraints = constraintList_makeNew();
+ e->trueEnsuresConstraints = constraintList_makeNew();;
+ e->falseEnsuresConstraints = constraintList_makeNew();;
+ */
+
+ if (exprNode_isUnhandled (e))
+ {
+ return;
+ }
+
+ handledExprNode = TRUE;
+
+ data = e->edata;
+
+ switch (e->kind)
+ {