+ constraintList temp;
+ constraint con;
+
+ DPRINTF ((message("Got case marker")));
+
+ if (constraintList_isUndefined(*savedEnsures) &&
+ 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")));
+ 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));
+
+
+ constraintList_free(*currentEnsures);
+ *currentEnsures = constraintList_makeNew();
+ *currentEnsures = constraintList_add(*currentEnsures, con);
+
+ constraintList_free(*currentRequires);
+ *currentRequires = constraintList_makeNew();
+ DPRINTF((message("exprNode_doGenerateConstraintSwitch: (switch %s) %s savedRequires:"
+ "%s savedEnsures:%s",
+ exprNode_unparse(switchExpr), exprNode_unparse(body),
+ constraintList_print(*savedRequires), constraintList_print(*savedEnsures)
+ )));
+
+ }
+
+ else if (exprNode_isCaseMarker(stmt))
+ /* prior case has no break. */
+ {
+ /*
+ We don't do anything to the sved constraints because the case hasn't ended
+ The new ensures constraints for the case will be:
+ the constraint for the case statement (CASE_LABEL == SWITCH_EXPR) logicalOr currentEnsures
+ */
+
+ constraintList 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();
+
+ ensuresTemp = constraintList_add (ensuresTemp, con);
+
+ if (exprNode_isError(stmtList))
+ {
+ constraintList_free(*currentEnsures);
+
+ *currentEnsures = constraintList_copy(ensuresTemp);
+ constraintList_free(ensuresTemp);
+
+ }
+ else
+ {
+
+ temp = constraintList_logicalOr (*currentEnsures, ensuresTemp);
+
+ constraintList_free(*currentEnsures);
+ constraintList_free(ensuresTemp);
+
+ *currentEnsures = temp;
+ }
+ constraintList_free(*currentRequires);
+
+ *currentRequires = constraintList_makeNew();
+ }
+ else
+ {
+ /*
+ we handle the case of ! exprNode_isCaseMarker above
+ the else if clause should always be true.
+ */
+ BADEXIT;
+ }
+
+ DPRINTF((message("returning from exprNode_doGenerateConstraintSwitch: (switch %s) %s currentRequires:"
+ "%s currentEnsures:%s",
+ exprNode_unparse(switchExpr), exprNode_unparse(body),
+ constraintList_print(*currentRequires), constraintList_print(*currentEnsures)
+ )));
+ /*@-onlytrans@*/
+ return;
+ /*@=onlytrans@*/
+}
+
+
+static void exprNode_generateConstraintSwitch (/*@notnull@*/ exprNode switchStmt)
+{
+ constraintList constraintsRequires;
+ constraintList constraintsEnsures;
+ constraintList lastRequires;
+ constraintList lastEnsures;
+
+ exprNode body;
+ exprNode switchExpr;
+
+ switchExpr = exprData_getPairA (switchStmt->edata);
+ body = exprData_getPairB (switchStmt->edata);
+
+ if (!exprNode_isDefined (body))
+ {
+ return;
+ }
+
+ /*@i22*/
+ DPRINTF((message("")));
+
+ if (body->kind == XPR_BLOCK)
+ body = exprData_getSingle(body->edata);
+
+ /*
+ constraintsRequires = constraintList_undefined;
+ constraintsEnsures = constraintList_undefined;
+
+ lastRequires = constraintList_makeNew();
+ lastEnsures = constraintList_makeNew();
+ */
+
+ /*@-mustfree@*/
+ /*@i6534 - evans 2002-01-01: spurious warnings for these becuase of stack allocated storage */
+ exprNode_doGenerateConstraintSwitch (switchExpr, body, &lastRequires,
+ &lastEnsures, &constraintsRequires, &constraintsEnsures);
+ /*@=mustfree@*/
+
+ /*
+ merge current and saved constraint with Logical Or...
+ make a constraint for ensures
+ */
+
+ constraintList_free(switchStmt->requiresConstraints);
+ constraintList_free(switchStmt->ensuresConstraints);
+
+ if (constraintList_isDefined(constraintsEnsures) && constraintList_isDefined(constraintsRequires))
+ {
+ switchStmt->ensuresConstraints = constraintList_logicalOr(constraintsEnsures, lastEnsures);
+ switchStmt->requiresConstraints = constraintList_mergeRequires(constraintsRequires, lastRequires);
+ constraintList_free (constraintsRequires);
+ constraintList_free (constraintsEnsures);
+ }
+ else
+ {
+ switchStmt->ensuresConstraints = constraintList_copy(lastEnsures);
+ switchStmt->requiresConstraints = constraintList_copy(lastRequires);
+ }
+
+ constraintList_free (lastRequires);
+ constraintList_free (lastEnsures);
+
+ DPRINTF(((message(" exprNode_generateConstraintSwitch returning requires: %s and ensures %s",
+ constraintList_print(switchStmt->requiresConstraints),
+ constraintList_print(switchStmt->ensuresConstraints)
+ )
+ )));
+}
+
+static exprNode doSwitch (/*@returned@*/ /*@notnull@*/ exprNode e)
+{
+ exprNode body;
+ exprData data;
+
+ data = e->edata;
+ DPRINTF ((message ("doSwitch for: switch (%s) %s",
+ exprNode_unparse (exprData_getPairA (data)),
+ exprNode_unparse (exprData_getPairB (data)))));
+
+ body = exprData_getPairB (data);
+ exprNode_generateConstraintSwitch (e);
+ return e;
+}
+
+void exprNode_multiStatement (/*@dependent@*/ exprNode e)
+{
+
+ bool ret;
+ exprData data;
+ exprNode e1, e2;
+ exprNode p, trueBranch, falseBranch;
+ exprNode forPred, forBody;
+ exprNode test;
+
+ constraintList temp;
+
+ DPRINTF((message ("exprNode_multistatement Analysising %s %s at", exprNode_unparse(e),
+ fileloc_unparse(exprNode_getfileloc(e)))));
+
+ if (exprNode_handleError (e))
+ {
+ return;
+ }
+
+ data = e->edata;
+
+ ret = TRUE;
+
+ switch (e->kind)
+ {
+
+ case XPR_FOR:
+ forPred = exprData_getPairA (data);
+ forBody = exprData_getPairB (data);
+
+ /* First generate the constraints */
+ exprNode_generateConstraints (forPred);
+ exprNode_generateConstraints (forBody);
+
+
+ doFor (e, forPred, forBody);
+
+ break;
+
+ case XPR_FORPRED:
+ exprNode_generateConstraints (exprData_getTripleInit (data));
+ test = exprData_getTripleTest (data);
+ exprNode_exprTraverse (test,FALSE, FALSE, exprNode_loc(e));
+ exprNode_generateConstraints (exprData_getTripleInc (data));
+
+ if (!exprNode_isError(test))
+ {
+ constraintList temp2;
+ temp2 = test->trueEnsuresConstraints;
+ test->trueEnsuresConstraints = exprNode_traversTrueEnsuresConstraints(test);
+ constraintList_free(temp2);
+ }
+
+ exprNode_generateConstraints (exprData_getTripleInc (data));
+ break;
+
+ case XPR_WHILE:
+ e1 = exprData_getPairA (data);
+ e2 = exprData_getPairB (data);
+
+ exprNode_exprTraverse (e1,
+ FALSE, FALSE, exprNode_loc(e1));
+
+ exprNode_generateConstraints (e2);
+
+ e = doWhile (e, e1, e2);
+
+ break;
+
+ case XPR_IF:
+ DPRINTF(("IF:"));
+ DPRINTF ((exprNode_unparse(e)));
+ 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_print(p->trueEnsuresConstraints) )
+ ));
+
+ /*drl 10/10/2002 this is a bit of a hack but the reason why we do this is so that any function post conditions or similar things get applied correctly to each branch. e.g. in strlen(s) < 5 we want the trueEnsures to be maxRead(s) < 5*/
+
+ p->trueEnsuresConstraints = constraintList_substituteFreeTarget (p->trueEnsuresConstraints,
+ p->ensuresConstraints);
+
+ DPRINTF(( message ("p->trueEnsuresConstraints after substitue %s", constraintList_print(p->trueEnsuresConstraints) )
+ ));
+
+ temp = p->falseEnsuresConstraints;
+ p->falseEnsuresConstraints = exprNode_traversFalseEnsuresConstraints(p);
+ constraintList_free(temp);
+
+ /*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_print(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);
+ 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_isEq_Op (tok))
+ {
+ return TRUE;
+ }
+ if (lltok_isAnd_Op (tok))
+
+ {
+
+ return TRUE;
+ }
+ if (lltok_isOr_Op (tok))
+ {
+ return TRUE;
+ }
+
+ if (lltok_isGt_Op (tok))
+ {
+ return TRUE;
+ }
+ if (lltok_isLt_Op (tok))
+ {
+ return TRUE;
+ }
+
+ if (lltok_isLe_Op (tok))
+ {
+ return TRUE;
+ }
+
+ if (lltok_isGe_Op (tok))
+ {
+ return TRUE;
+ }
+
+ return FALSE;
+
+}
+
+
+static void exprNode_booleanTraverse (/*@dependent@*/ exprNode e, /*@unused@*/ bool definatelv, /*@unused@*/ bool definaterv, fileloc sequencePoint)
+{
+ constraint cons;
+ exprNode t1, t2;
+ exprData data;
+ lltok tok;
+ constraintList tempList, temp;
+ data = e->edata;
+
+ tok = exprData_getOpTok (data);
+ t1 = exprData_getOpA (data);
+ t2 = exprData_getOpB (data);
+
+ tempList = constraintList_undefined;
+
+ /* arithmetic tests */
+
+ if (lltok_isEq_Op (tok))
+ {
+ cons = constraint_makeEnsureEqual (t1, t2, sequencePoint);
+ e->trueEnsuresConstraints = constraintList_add(e->trueEnsuresConstraints, cons);
+ }
+
+
+ if (lltok_isLt_Op (tok))
+ {
+ cons = constraint_makeEnsureLessThan (t1, t2, sequencePoint);
+ e->trueEnsuresConstraints = constraintList_add(e->trueEnsuresConstraints, cons);
+ cons = constraint_makeEnsureGreaterThanEqual (t1, t2, sequencePoint);
+ e->falseEnsuresConstraints = constraintList_add(e->falseEnsuresConstraints, cons);
+ }
+
+ if (lltok_isGe_Op (tok))
+ {
+ cons = constraint_makeEnsureGreaterThanEqual (t1, t2, sequencePoint);
+ e->trueEnsuresConstraints = constraintList_add(e->trueEnsuresConstraints, cons);
+
+ cons = constraint_makeEnsureLessThan (t1, t2, sequencePoint);
+ e->falseEnsuresConstraints = constraintList_add(e->falseEnsuresConstraints, cons);
+ }
+
+ if (lltok_isGt_Op (tok))
+ {
+ cons = constraint_makeEnsureGreaterThan (t1, t2, sequencePoint);
+ e->trueEnsuresConstraints = constraintList_add(e->trueEnsuresConstraints, cons);
+ cons = constraint_makeEnsureLessThanEqual (t1, t2, sequencePoint);
+ e->falseEnsuresConstraints = constraintList_add(e->falseEnsuresConstraints, cons);
+ }
+
+ if (lltok_isLe_Op (tok))
+ {
+ cons = constraint_makeEnsureLessThanEqual (t1, t2, sequencePoint);
+ e->trueEnsuresConstraints = constraintList_add(e->trueEnsuresConstraints, cons);
+
+ cons = constraint_makeEnsureGreaterThan (t1, t2, sequencePoint);
+ e->falseEnsuresConstraints = constraintList_add(e->falseEnsuresConstraints, cons);
+ }
+
+ /* Logical operations */
+
+ if (lltok_isAnd_Op (tok))
+ {
+ /* true ensures */
+ tempList = constraintList_copy (t1->trueEnsuresConstraints);
+ tempList = constraintList_addList (tempList, t2->trueEnsuresConstraints);
+ e->trueEnsuresConstraints = constraintList_addListFree(e->trueEnsuresConstraints, tempList);
+
+ /* false ensures: fens t1 or tens t1 and fens t2 */
+ tempList = constraintList_copy (t1->trueEnsuresConstraints);
+ tempList = constraintList_addList (tempList, t2->falseEnsuresConstraints);
+ temp = tempList;
+ tempList = constraintList_logicalOr (tempList, t1->falseEnsuresConstraints);
+ constraintList_free (temp);
+
+ /* evans - was constraintList_addList - memory leak detected by splint */
+ e->falseEnsuresConstraints = constraintList_addListFree (e->falseEnsuresConstraints, tempList);
+ }
+ else if (lltok_isOr_Op (tok))
+ {
+ /* false ensures */
+ tempList = constraintList_copy (t1->falseEnsuresConstraints);
+ tempList = constraintList_addList (tempList, t2->falseEnsuresConstraints);
+ e->falseEnsuresConstraints = constraintList_addListFree(e->falseEnsuresConstraints, tempList);
+
+ /* true ensures: tens t1 or fens t1 and tens t2 */
+ tempList = constraintList_copy (t1->falseEnsuresConstraints);
+ tempList = constraintList_addList (tempList, t2->trueEnsuresConstraints);