constraintList_free(c);
}
- DPRINTF ((message ("e->requiresConstraints %s", constraintList_printDetailed (e->requiresConstraints))));
+ DPRINTF ((message ("e->requiresConstraints %s", constraintList_unparseDetailed (e->requiresConstraints))));
return FALSE;
}
e->ensuresConstraints = exprNode_traversEnsuresConstraints(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;
}
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))));
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;
}
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)
)
)));
}
- 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;
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;
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_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;
e->requiresConstraints = constraintList_removeSurpressed(e->requiresConstraints);
- 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))));
return;
}
ret = constraintList_addListFree (ret,
exprNode_traversTrueEnsuresConstraints
(exprData_getFcn (data)));
- /*@i11*/ /* exprNodeList_unparse (exprData_getArgs (data)); */
break;
case XPR_RETURN:
ret = constraintList_addListFree (ret,
exprNode_traversFalseEnsuresConstraints
(exprData_getFcn (data)));
- /*@i11*/ /* exprNodeList_unparse (exprData_getArgs (data)); */
break;
case XPR_RETURN:
ret = constraintList_addListFree (ret,
exprNode_traversRequiresConstraints
(exprData_getFcn (data)));
- /*@i11*/ /* exprNodeList_unparse (exprData_getArgs (data)); */
break;
case XPR_RETURN:
DPRINTF ((message ("exprnode_traversEnsuresConstraints call for %s with "
"constraintList of %s",
exprNode_unparse (e),
- constraintList_print(e->ensuresConstraints)
+ constraintList_unparse(e->ensuresConstraints)
)
));
ret = constraintList_addListFree (ret,
exprNode_traversEnsuresConstraints
(exprData_getFcn (data)));
- /*@i11*/ /* exprNodeList_unparse (exprData_getArgs (data)); */
break;
case XPR_RETURN:
ret = constraintList_addListFree (ret,
DPRINTF((message ("exprnode_traversEnsuresConstraints call for %s with "
"constraintList of is returning %s",
exprNode_unparse (e),
- constraintList_print(ret))));
+ constraintList_unparse(ret))));
return ret;
}
invars = getInvariants(ct);
- TPRINTF((message ("findStructs has invariants %s ", constraintList_print (invars))
+ TPRINTF((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))
+ TPRINTF((message ("findStructs finded invariants to be %s ", constraintList_unparse (invars))
));
}
}
}
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;
andersk / splint.git / blobdiff