# include "aliasChecks.h"
# include "exprNodeSList.h"
-# include "exprData.i"
# include "exprDataQuite.i"
+/*@access exprNode @*/
+
extern void forLoopHeuristics( exprNode e, exprNode forPred, exprNode forBody);
bool /*@alt void@*/ exprNode_generateConstraints (/*@temp@*/ exprNode e);
//static cstring exprNode_findConstraints ( exprNode p_e);
static bool exprNode_isMultiStatement(exprNode p_e);
-static bool exprNode_multiStatement (exprNode p_e);
-bool exprNode_exprTraverse (exprNode e, bool definatelv, bool definaterv, fileloc sequencePoint);
+static void exprNode_multiStatement (exprNode p_e);
+
//static void exprNode_constraintPropagateUp (exprNode p_e);
-constraintList exprNode_traversRequiresConstraints (exprNode e);
-constraintList exprNode_traversEnsuresConstraints (exprNode e);
-constraintList exprNode_traversTrueEnsuresConstraints (exprNode e);
-constraintList exprNode_traversFalseEnsuresConstraints (exprNode e);
+static constraintList exprNode_traversTrueEnsuresConstraints (exprNode e);
+static constraintList exprNode_traversFalseEnsuresConstraints (exprNode e);
-extern constraintList reflectChanges (constraintList pre2, constraintList post1);
+exprNode makeDataTypeConstraints (/*@returned@*/ exprNode e);
-void mergeResolve (exprNode parent, exprNode child1, exprNode child2);
-exprNode makeDataTypeConstraints (exprNode e);
constraintList constraintList_makeFixedArrayConstraints (sRefSet s);
-constraintList checkCall (exprNode fcn, exprNodeList arglist);
-
-void checkArgumentList (exprNode temp, exprNodeList arglist, fileloc sequencePoint);
//bool exprNode_testd()
//{
*/
//}
-bool exprNode_isUnhandled (exprNode e)
+static bool exprNode_isUnhandled (exprNode e)
{
llassert( exprNode_isDefined(e) );
switch (e->kind)
{
if (exprNode_isError (e) )
return FALSE;
-
- e->requiresConstraints = constraintList_new();
- e->ensuresConstraints = constraintList_new();
- e->trueEnsuresConstraints = constraintList_new();
- e->falseEnsuresConstraints = constraintList_new();
+ /*
+ e->requiresConstraints = constraintList_makeNew();
+ e->ensuresConstraints = constraintList_makeNew();
+ e->trueEnsuresConstraints = constraintList_makeNew();
+ e->falseEnsuresConstraints = constraintList_makeNew();
+ */
if (exprNode_isUnhandled (e) )
{
loc = exprNode_getNextSequencePoint(e);
exprNode_exprTraverse(e, FALSE, FALSE, loc);
- // llassert(FALSE);
+ fileloc_free(loc);
return FALSE;
}
constraintList c;
c = constraintList_makeFixedArrayConstraints (e->uses);
- e->requiresConstraints = reflectChanges (e->requiresConstraints, c);
+ e->requiresConstraints = reflectChangesFreePre (e->requiresConstraints, c);
// e->ensuresConstraints = constraintList_mergeEnsures(c, e->ensuresConstraints);
+ constraintList_free(c);
}
- /* printf ("%s", (message ("%s", constraintList_printDetailed (e->requiresConstraints) ) ) );
- printf ("%s", (message ("%s", constraintList_printDetailed (e->ensuresConstraints) ) ) ); */
+ DPRINTF ( (message ("e->requiresConstraints %s", constraintList_printDetailed (e->requiresConstraints) ) ) );
return FALSE;
}
}
-bool exprNode_stmt (exprNode e)
+static void exprNode_stmt (exprNode e)
{
exprNode snode;
fileloc loc;
- bool notError;
- char * s;
+ cstring s;
if (exprNode_isError(e) )
{
- return FALSE;
+ return; // FALSE;
}
- e->requiresConstraints = constraintList_new();
- e->ensuresConstraints = constraintList_new();
+ /*e->requiresConstraints = constraintList_makeNew();
+ e->ensuresConstraints = constraintList_makeNew(); */
// e = makeDataTypeConstraints(e);
if (e->kind == XPR_INIT)
{
+ constraintList tempList;
DPRINTF (("Init") );
DPRINTF ( (message ("%s ", exprNode_unparse (e)) ) );
loc = exprNode_getNextSequencePoint(e); /* reduces to an expression */
- notError = exprNode_exprTraverse (e, FALSE, FALSE, loc);
+ exprNode_exprTraverse (e, FALSE, FALSE, loc);
+ fileloc_free(loc);
+
+ tempList = e->requiresConstraints;
e->requiresConstraints = exprNode_traversRequiresConstraints(e);
+ constraintList_free(tempList);
+
+ tempList = e->ensuresConstraints;
e->ensuresConstraints = exprNode_traversEnsuresConstraints(e);
- return notError;
+ constraintList_free(tempList);
+ return; // notError;
}
if (e->kind != XPR_STMT)
{
return exprNode_multiStatement (e );
}
- BPRINTF( (message ("Ignoring non-statement %s", exprNode_unparse(e) ) ) );
- return TRUE;
+ DPRINTF( (message ("Ignoring non-statement %s", exprNode_unparse(e) ) ) );
+ return; //TRUE;
// llassert(FALSE);
}
if (exprNode_isMultiStatement (snode))
{
- bool temp;
-
- temp = exprNode_multiStatement (snode);
- exprNode_copyConstraints (e, snode);
- return temp;
+ exprNode_multiStatement (snode);
+ (void) exprNode_copyConstraints (e, snode);
+ return;
}
loc = exprNode_getNextSequencePoint(e); /* reduces to an expression */
- notError = exprNode_exprTraverse (snode, FALSE, FALSE, loc);
+ //notError =
+ exprNode_exprTraverse (snode, FALSE, FALSE, loc);
+
+ fileloc_free(loc);
+
+ constraintList_free (e->requiresConstraints);
e->requiresConstraints = exprNode_traversRequiresConstraints(snode);
// printf ("For: %s \n", exprNode_unparse (e) );
// printf ("%s\n", constraintList_print(e->requiresConstraints) );
+
+ constraintList_free (e->ensuresConstraints);
e->ensuresConstraints = exprNode_traversEnsuresConstraints(snode);
// printf ("Ensures that:\n %s\n", constraintList_print(e->ensuresConstraints) );
// llassert(notError);
- return notError;
+
+ DPRINTF ( (message ("smtlist constraints are: pre: %s \n and \t post %s\n",
+ constraintList_print(e->requiresConstraints),
+ constraintList_print(e->ensuresConstraints) ) ) );
+
+ return; // notError;
}
-bool exprNode_stmtList (exprNode e)
+static void exprNode_stmtList (exprNode e)
{
exprNode stmt1, stmt2;
if (exprNode_isError (e) )
{
- return FALSE;
+ return; // FALSE;
}
- e->requiresConstraints = constraintList_new();
- e->ensuresConstraints = constraintList_new();
+ /*
+ e->requiresConstraints = constraintList_makeNew();
+ e->ensuresConstraints = constraintList_makeNew();
+ */
// e = makeDataTypeConstraints(e);
/*Handle case of stmtList with only one statement:
The parse tree stores this as stmt instead of stmtList*/
if (e->kind != XPR_STMTLIST)
{
- return exprNode_stmt(e);
+ exprNode_stmt(e);
+ return;
}
llassert (e->kind == XPR_STMTLIST);
DPRINTF(( "STMTLIST:") );
DPRINTF ( (message ("smtlist constraints are: pre: %s \n and \t post %s\n",
constraintList_print(e->requiresConstraints),
constraintList_print(e->ensuresConstraints) ) ) );
- return TRUE;
+ return; // TRUE;
}
-exprNode doIf (exprNode e, exprNode test, exprNode body)
+static exprNode doIf (/*@returned@*/ exprNode e, exprNode test, exprNode body)
{
+ constraintList temp;
+
DPRINTF ((message ("doIf: %s ", exprNode_unparse(e) ) ) );
- llassert(test);
- llassert(e);
- llassert(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 ("Requires constraints for %s are %s", exprNode_unparse(e), constraintList_printDetailed(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((message ("ensures constraints for %s are %s", exprNode_unparse(test), constraintList_printDetailed(test->ensuresConstraints) ) ));
+
+ DPRINTF((message ("Requires constraints for %s are %s", exprNode_unparse(test), constraintList_printDetailed(test->ensuresConstraints) ) ));
+
+ DPRINTF((message ("trueEnsures constraints for %s are %s", exprNode_unparse(test), constraintList_printDetailed(test->trueEnsuresConstraints) ) ));
+
+ DPRINTF((message ("falseEnsures constraints for %s are %s", exprNode_unparse(test), constraintList_printDetailed(test->falseEnsuresConstraints) ) ));
+
+
+
+ temp = test->trueEnsuresConstraints;
+ test->trueEnsuresConstraints = exprNode_traversTrueEnsuresConstraints(test);
+ constraintList_free(temp);
+
+ temp = test->ensuresConstraints;
test->ensuresConstraints = exprNode_traversEnsuresConstraints (test);
+ constraintList_free(temp);
+
+ temp = test->requiresConstraints;
test->requiresConstraints = exprNode_traversRequiresConstraints (test);
-
- test->trueEnsuresConstraints = exprNode_traversTrueEnsuresConstraints(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 true ensures %s ", constraintList_print(test->trueEnsuresConstraints) ) ) );
+
+ constraintList_free(e->requiresConstraints);
e->requiresConstraints = reflectChanges (body->requiresConstraints, test->trueEnsuresConstraints);
- e->requiresConstraints = reflectChanges (e->requiresConstraints,
+
+ e->requiresConstraints = reflectChangesFreePre (e->requiresConstraints,
test->ensuresConstraints);
+ temp = e->requiresConstraints;
e->requiresConstraints = constraintList_mergeRequires (e->requiresConstraints, test->requiresConstraints);
-
+ constraintList_free(temp);
+
+
#warning bad
+ constraintList_free(e->ensuresConstraints);
e->ensuresConstraints = constraintList_copy (test->ensuresConstraints);
- /*
- if (!exprNode_mayEscape (body) )
- e->ensuresConstraints = constraintList_mergeEnsures (e->ensuresConstraints,
+
+ if (exprNode_mayEscape (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) ) ) );
return e;
*/
-exprNode doIfElse (/*@returned@*/ exprNode e, exprNode p, exprNode trueBranch, exprNode falseBranch)
+static exprNode doIfElse (/*@returned@*/ exprNode e, exprNode p, exprNode trueBranch, exprNode falseBranch)
{
- constraintList c1, cons, t, f;
+ constraintList c1, cons, t, t2, f, f2;
+
+ DPRINTF ((message ("doIfElse: %s ", exprNode_unparse(e) ) ) );
// do requires clauses
c1 = constraintList_copy (p->ensuresConstraints);
t = reflectChanges (trueBranch->requiresConstraints, p->trueEnsuresConstraints);
- t = reflectChanges (t, p->ensuresConstraints);
+ t = reflectChangesFreePre (t, p->ensuresConstraints);
- // e->requiresConstraints = constraintList_copy (cons);
-
cons = reflectChanges (falseBranch->requiresConstraints, p->falseEnsuresConstraints);
- cons = reflectChanges (cons, c1);
+ cons = reflectChangesFreePre (cons, c1);
- e->requiresConstraints = constraintList_mergeRequires (t, cons);
- e->requiresConstraints = constraintList_mergeRequires (e->requiresConstraints, p->requiresConstraints);
+ constraintList_free(e->requiresConstraints);
+ e->requiresConstraints = constraintList_mergeRequiresFreeFirst (t, cons);
+ e->requiresConstraints = constraintList_mergeRequiresFreeFirst (e->requiresConstraints, p->requiresConstraints);
// do ensures clauses
// find the the ensures lists for each subbranch
t = constraintList_mergeEnsures (p->trueEnsuresConstraints, trueBranch->ensuresConstraints);
+ t2 = t;
t = constraintList_mergeEnsures (p->ensuresConstraints, t);
-
+ constraintList_free(t2);
+
f = constraintList_mergeEnsures (p->falseEnsuresConstraints, falseBranch->ensuresConstraints);
+ f2 = f;
f = constraintList_mergeEnsures (p->ensuresConstraints, f);
+ constraintList_free(f2);
// find ensures for whole if/else statement
+ constraintList_free(e->ensuresConstraints);
+
e->ensuresConstraints = constraintList_logicalOr (t, f);
+ constraintList_free(t);
+ constraintList_free(f);
+ 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) ) ) );
+
return e;
}
-exprNode doWhile (exprNode e, exprNode test, exprNode body)
+static exprNode doWhile (/*@returned@*/ exprNode e, exprNode test, exprNode body)
{
DPRINTF ((message ("doWhile: %s ", exprNode_unparse(e) ) ) );
return doIf (e, test, body);
{
constraintList ret;
constraint con;
- ret = constraintList_new();
+ ret = constraintList_makeNew();
sRefSet_elements (s, el)
{
// llassert (el);
if (sRef_isFixedArray(el) )
{
- int s;
+ long int size;
DPRINTF( (message("%s is a fixed array",
sRef_unparse(el)) ) );
//if (el->kind == SK_DERIVED)
// break; //hack until I find the real problem
- s = sRef_getArraySize(el);
+ size = sRef_getArraySize(el);
DPRINTF( (message("%s is a fixed array with size %d",
- sRef_unparse(el), s) ) );
- con = constraint_makeSRefSetBufferSize (el, (s - 1));
- //con = constraint_makeSRefWriteSafeInt (el, (s - 1));
+ sRef_unparse(el), (int)size) ) );
+ con = constraint_makeSRefSetBufferSize (el, (size - 1));
+ //con = constraint_makeSRefWriteSafeInt (el, (size - 1));
ret = constraintList_add(ret, con);
}
else
return ret;
}
-exprNode makeDataTypeConstraints (exprNode e)
+exprNode makeDataTypeConstraints (/*@returned@*/ exprNode e)
{
constraintList c;
DPRINTF(("makeDataTypeConstraints"));
c = constraintList_makeFixedArrayConstraints (e->uses);
- e->ensuresConstraints = constraintList_addList (e->ensuresConstraints, c);
+ e->ensuresConstraints = constraintList_addListFree (e->ensuresConstraints, c);
return e;
}
-void doFor (exprNode e, exprNode forPred, exprNode forBody)
+static void doFor (exprNode e, exprNode forPred, exprNode forBody)
{
exprNode init, test, inc;
//merge the constraints: modle as if statement
forLoopHeuristics(e, forPred, forBody);
+ constraintList_free(e->requiresConstraints);
e->requiresConstraints = reflectChanges (forBody->requiresConstraints, test->ensuresConstraints);
- e->requiresConstraints = reflectChanges (e->requiresConstraints, test->trueEnsuresConstraints);
- e->requiresConstraints = reflectChanges (e->requiresConstraints, forPred->ensuresConstraints);
+ e->requiresConstraints = reflectChangesFreePre (e->requiresConstraints, test->trueEnsuresConstraints);
+ e->requiresConstraints = reflectChangesFreePre (e->requiresConstraints, forPred->ensuresConstraints);
if (!forBody->canBreak)
{
- e->ensuresConstraints = constraintList_addList(e->ensuresConstraints, forPred->ensuresConstraints);
- e->ensuresConstraints = constraintList_addList(e->ensuresConstraints, test->falseEnsuresConstraints);
+ e->ensuresConstraints = constraintList_addListFree(e->ensuresConstraints, constraintList_copy(forPred->ensuresConstraints) );
+ e->ensuresConstraints = constraintList_addListFree(e->ensuresConstraints,constraintList_copy( test->falseEnsuresConstraints));
+ // forPred->ensuresConstraints = constraintList_undefined;
+ // test->falseEnsuresConstraints = constraintList_undefined;
}
else
{
}
-exprNode doSwitch (/*@returned@*/ exprNode e)
+static exprNode doSwitch (/*@returned@*/ exprNode e)
{
exprNode body;
exprData data;
data = e->edata;
llassert(FALSE);
- //TPRINTF (( message ("doSwitch for: switch (%s) %s",
+ //DPRINTF (( message ("doSwitch for: switch (%s) %s",
// exprNode_unparse (exprData_getPairA (data)),
// exprNode_unparse (exprData_getPairB (data))) ));
}
-bool exprNode_multiStatement (exprNode e)
+void exprNode_multiStatement (exprNode e)
{
bool ret;
exprNode p, trueBranch, falseBranch;
exprNode forPred, forBody;
exprNode test;
- // constraintList t, f;
- e->requiresConstraints = constraintList_new();
- e->ensuresConstraints = constraintList_new();
- e->trueEnsuresConstraints = constraintList_new();
- e->falseEnsuresConstraints = constraintList_new();
+ constraintList temp;
+
+ // constraintList t, f;
+ /*e->requiresConstraints = constraintList_makeNew();
+ e->ensuresConstraints = constraintList_makeNew();
+ e->trueEnsuresConstraints = constraintList_makeNew();
+ e->falseEnsuresConstraints = constraintList_makeNew();
+ */
// e = makeDataTypeConstraints(e);
DPRINTF((message ("exprNode_multistatement Analysising %s %s at", exprNode_unparse( e),
if (exprNode_handleError (e))
{
- return FALSE;
+ return; // FALSE;
}
data = e->edata;
exprNode_generateConstraints (exprData_getTripleInc (data) );
if (!exprNode_isError(test) )
- test->trueEnsuresConstraints = exprNode_traversTrueEnsuresConstraints(test);
-
+ {
+ constraintList temp2;
+ temp2 = test->trueEnsuresConstraints;
+ test->trueEnsuresConstraints = exprNode_traversTrueEnsuresConstraints(test);
+ constraintList_free(temp2);
+ }
+
exprNode_generateConstraints (exprData_getTripleInc (data));
break;
FALSE, FALSE, exprNode_loc(e1));
exprNode_generateConstraints (e2);
-
e = doIf (e, e1, e2);
exprNode_generateConstraints (trueBranch);
exprNode_generateConstraints (falseBranch);
+ 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);
+
+ temp = p->falseEnsuresConstraints;
p->falseEnsuresConstraints = exprNode_traversFalseEnsuresConstraints(p);
+ constraintList_free(temp);
e = doIfElse (e, p, trueBranch, falseBranch);
DPRINTF( ("Done IFELSE") );
case XPR_BLOCK:
// ret = message ("{ %s }",
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 );
// e->constraints = (exprData_getSingle (data))->constraints;
break;
break;
case XPR_STMT:
case XPR_STMTLIST:
- return exprNode_stmtList (e);
+ exprNode_stmtList (e);
+ return ;
/*@notreached@*/
break;
default:
ret=FALSE;
}
- return ret;
+ return; // ret;
}
-bool lltok_isBoolean_Op (lltok tok)
+static bool lltok_isBoolean_Op (lltok tok)
{
/*this should really be a switch statement but
I don't want to violate the abstraction
}
-void exprNode_booleanTraverse (exprNode e, bool definatelv, bool definaterv, fileloc sequencePoint)
+static void exprNode_booleanTraverse (exprNode e, /*@unused@*/ bool definatelv, /*@unused@*/ bool definaterv, fileloc sequencePoint)
{
constraint cons;
exprNode t1, t2;
exprData data;
lltok tok;
-constraintList tempList;
+constraintList tempList, temp;
data = e->edata;
tok = exprData_getOpTok (data);
//true ensures
tempList = constraintList_copy (t1->trueEnsuresConstraints);
tempList = constraintList_addList (tempList, t2->trueEnsuresConstraints);
- e->trueEnsuresConstraints = constraintList_addList(e->trueEnsuresConstraints, tempList);
+ 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);
+
e->falseEnsuresConstraints =constraintList_addList(e->falseEnsuresConstraints, tempList);
}
-
- if (lltok_isOr_Op (tok) )
- {
+ else if (lltok_isOr_Op (tok) )
+ {
//false ensures
tempList = constraintList_copy (t1->falseEnsuresConstraints);
tempList = constraintList_addList (tempList, t2->falseEnsuresConstraints);
- e->falseEnsuresConstraints = constraintList_addList(e->falseEnsuresConstraints, tempList);
+ 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);
- e->trueEnsuresConstraints =constraintList_addList(e->trueEnsuresConstraints, tempList);
+ constraintList_free(temp);
+
+
+ e->trueEnsuresConstraints =constraintList_addListFree(e->trueEnsuresConstraints, tempList);
}
+ else
+ {
+ DPRINTF((message("%s is not a boolean operation", lltok_unparse(tok) ) ));
+ }
}
-bool exprNode_exprTraverse (exprNode e, bool definatelv, bool definaterv, fileloc sequencePoint)
+void exprNode_exprTraverse (exprNode e, bool definatelv, bool definaterv, /*@observer@*/ fileloc sequencePoint)
{
exprNode t1, t2, fcn;
lltok tok;
exprData data;
constraint cons;
+ constraintList temp;
+
if (exprNode_isError(e) )
{
- return FALSE;
+ return; // FALSE;
}
DPRINTF((message ("exprNode_exprTraverset Analysising %s %s at", exprNode_unparse( e),
fileloc_unparse(exprNode_getfileloc(e) ) ) ) );
- e->requiresConstraints = constraintList_new();
- e->ensuresConstraints = constraintList_new();
- e->trueEnsuresConstraints = constraintList_new();;
- e->falseEnsuresConstraints = constraintList_new();;
-
+ /*e->requiresConstraints = constraintList_makeNew();
+ e->ensuresConstraints = constraintList_makeNew();
+ e->trueEnsuresConstraints = constraintList_makeNew();;
+ e->falseEnsuresConstraints = constraintList_makeNew();;
+ */
if (exprNode_isUnhandled (e) )
{
- return FALSE;
+ return; // FALSE;
}
// e = makeDataTypeConstraints (e);
// cons = constraint_makeEnsureMinReadAtMost (t1, t2, sequencePoint);
// e->ensuresConstraints = constraintList_add(e->ensuresConstraints, cons);
-
+
exprNode_exprTraverse (exprData_getPairA (data), FALSE, TRUE, sequencePoint);
exprNode_exprTraverse (exprData_getPairB (data), FALSE, TRUE, sequencePoint);
t1 = exprData_getOpA (data);
t2 = exprData_getOpB (data);
exprNode_exprTraverse (t1, TRUE, definaterv, sequencePoint );
- lltok_unparse (exprData_getOpTok (data));
+ //lltok_unparse (exprData_getOpTok (data));
+ #warning check this for += -= etc
exprNode_exprTraverse (t2, definatelv, TRUE, sequencePoint );
/* this test is nessecary because some expressions generate a null expression node. function pointer do that -- drl */
tok = exprData_getOpTok (data);
exprNode_exprTraverse (t2, definatelv, definaterv, sequencePoint );
+ #warning fix definatelv and definaterv
+
+ if (tok.tok == ADD_ASSIGN)
+ {
+ cons = constraint_makeAddAssign (t1, t2, sequencePoint );
+ e->ensuresConstraints = constraintList_add(e->ensuresConstraints, cons);
+ }
+
+ if (tok.tok == SUB_ASSIGN)
+ {
+ cons = constraint_makeSubtractAssign (t1, t2, sequencePoint );
+ e->ensuresConstraints = constraintList_add(e->ensuresConstraints, cons);
+ }
+
+
+
if (lltok_isBoolean_Op (tok) )
exprNode_booleanTraverse (e, definatelv, definaterv, sequencePoint);
// e->constraints = constraintList_exprNodemerge (exprData_getOpA (data), exprData_getOpB (data));
break;
case XPR_SIZEOFT:
- ctype_unparse (qtype_getType (exprData_getType (data) ) );
+ #warning make sure the case can be ignored..
break;
fcn = exprData_getFcn(data);
exprNode_exprTraverse (fcn, definatelv, definaterv, sequencePoint );
- exprNodeList_unparse (exprData_getArgs (data) );
DPRINTF ( (message ("Got call that %s ( %s) ", exprNode_unparse(fcn), exprNodeList_unparse (exprData_getArgs (data) ) ) ) );
- fcn->requiresConstraints = constraintList_addList (fcn->requiresConstraints,
+ fcn->requiresConstraints = constraintList_addListFree (fcn->requiresConstraints,
checkCall (fcn, exprData_getArgs (data) ) );
- fcn->ensuresConstraints = constraintList_addList (fcn->ensuresConstraints,
+ fcn->ensuresConstraints = constraintList_addListFree (fcn->ensuresConstraints,
getPostConditions(fcn, exprData_getArgs (data),e ) );
t1 = exprNode_createNew (exprNode_getType (e) );
break;
case XPR_NULLRETURN:
- cstring_makeLiteral ("return");;
+
break;
case XPR_FACCESS:
exprNode_exprTraverse (exprData_getFieldNode (data), definatelv, definaterv, sequencePoint );
- exprData_getFieldName (data) ;
break;
case XPR_ARROW:
exprNode_exprTraverse (exprData_getFieldNode (data), definatelv, definaterv, sequencePoint );
- exprData_getFieldName (data);
break;
case XPR_STRINGLITERAL:
- cstring_copy (exprData_getLiteral (data));
+
break;
case XPR_NUMLIT:
- cstring_copy (exprData_getLiteral (data));
+
break;
case XPR_PREOP:
cons = constraint_makeMaxSetSideEffectPostDecrement (t1, sequencePoint );
e->ensuresConstraints = constraintList_add (e->ensuresConstraints, cons);
}
-
- if (lltok_isMult( exprData_getUopTok (data) ) )
+ else if (lltok_isMult( tok ) )
{
if (definatelv)
{
}
e->requiresConstraints = constraintList_add(e->requiresConstraints, cons);
}
-
- /* ! expr */
- if (lltok_isNot_Op (exprData_getUopTok (data) ) )
+ else if (lltok_isNot_Op (tok) )
+ /* ! expr */
{
+ constraintList_free(e->trueEnsuresConstraints);
+
e->trueEnsuresConstraints = constraintList_copy (t1->falseEnsuresConstraints);
+ constraintList_free(e->falseEnsuresConstraints);
e->falseEnsuresConstraints = constraintList_copy (t1->trueEnsuresConstraints);
}
+
+ else if (lltok_isAmpersand_Op (tok) )
+ {
+ break;
+ }
+ else if (lltok_isMinus_Op (tok) )
+ {
+ break;
+ }
+ else if ( lltok_isExcl_Op (tok) )
+ {
+ break;
+ }
+ else if (lltok_isTilde_Op (tok) )
+ {
+ break;
+ }
+ else
+ {
+ llcontbug((message("Unsupported preop in %s", exprNode_unparse(e) ) ));
+ BADEXIT;
+ }
break;
case XPR_POSTOP:
exprNode_exprTraverse (exprData_getUopNode (data), TRUE, definaterv, sequencePoint );
- lltok_unparse (exprData_getUopTok (data));
+
if (lltok_isInc_Op (exprData_getUopTok (data) ) )
{
DPRINTF(("doing ++"));
false = 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 (true, FALSE, TRUE, sequencePoint );
+
+ temp = true->ensuresConstraints;
true->ensuresConstraints = exprNode_traversEnsuresConstraints(true);
+ constraintList_free(temp);
+
+
+ temp = true->requiresConstraints;
true->requiresConstraints = exprNode_traversRequiresConstraints(true);
+ constraintList_free(temp);
+
+ temp = true->trueEnsuresConstraints;
true->trueEnsuresConstraints = exprNode_traversTrueEnsuresConstraints(true);
+ constraintList_free(temp);
+
+ temp = true->falseEnsuresConstraints;
true->falseEnsuresConstraints = exprNode_traversFalseEnsuresConstraints(true);
+ constraintList_free(temp);
+ //dfdf
exprNode_exprTraverse (false, FALSE, TRUE, sequencePoint );
+
+ temp = false->ensuresConstraints;
false->ensuresConstraints = exprNode_traversEnsuresConstraints(false);
+ constraintList_free(temp);
+
+
+ temp = false->requiresConstraints;
false->requiresConstraints = exprNode_traversRequiresConstraints(false);
+ constraintList_free(temp);
+
+ temp = false->trueEnsuresConstraints;
false->trueEnsuresConstraints = exprNode_traversTrueEnsuresConstraints(false);
- false->falseEnsuresConstraints = exprNode_traversFalseEnsuresConstraints(false);
+ constraintList_free(temp);
+ temp = false->falseEnsuresConstraints;
+ false->falseEnsuresConstraints = exprNode_traversFalseEnsuresConstraints(false);
+ constraintList_free(temp);
/* if pred is true e equals true otherwise pred equals false */
e->ensuresConstraints = constraintList_addGeneratingExpr ( e->ensuresConstraints, e);
- DPRINTF((message ("ensures constraint for %s are %s", exprNode_unparse(e), constraintList_printDetailed(e->ensuresConstraints) ) ));
+ 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) ) ));
- return handledExprNode;
+ 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) ) ));
+
+ return; // handledExprNode;
}
if (exprNode_handleError (e))
{
- ret = constraintList_new();
+ ret = constraintList_makeNew();
return ret;
}
ret = constraintList_copy (e->trueEnsuresConstraints );
{
case XPR_WHILEPRED:
t1 = exprData_getSingle (data);
- ret = constraintList_addList ( ret,exprNode_traversTrueEnsuresConstraints (t1) );
+ ret = constraintList_addListFree ( ret, exprNode_traversTrueEnsuresConstraints (t1) );
break;
case XPR_FETCH:
- ret = constraintList_addList (ret,
+ ret = constraintList_addListFree (ret,
exprNode_traversTrueEnsuresConstraints
(exprData_getPairA (data) ) );
- ret = constraintList_addList (ret,
+ ret = constraintList_addListFree (ret,
exprNode_traversTrueEnsuresConstraints
(exprData_getPairB (data) ) );
break;
case XPR_PREOP:
- ret = constraintList_addList (ret,
+ ret = constraintList_addListFree (ret,
exprNode_traversTrueEnsuresConstraints
(exprData_getUopNode (data) ) );
break;
case XPR_PARENS:
- ret = constraintList_addList (ret, exprNode_traversTrueEnsuresConstraints
+ ret = constraintList_addListFree (ret, exprNode_traversTrueEnsuresConstraints
(exprData_getUopNode (data) ) );
break;
case XPR_ASSIGN:
- ret = constraintList_addList (ret,
+ ret = constraintList_addListFree (ret,
exprNode_traversTrueEnsuresConstraints
(exprData_getOpA (data) ) );
- ret = constraintList_addList (ret,
+ ret = constraintList_addListFree (ret,
exprNode_traversTrueEnsuresConstraints
(exprData_getOpB (data) ) );
break;
case XPR_OP:
- ret = constraintList_addList (ret,
+ ret = constraintList_addListFree (ret,
exprNode_traversTrueEnsuresConstraints
(exprData_getOpA (data) ) );
- ret = constraintList_addList (ret,
+ ret = constraintList_addListFree (ret,
exprNode_traversTrueEnsuresConstraints
(exprData_getOpB (data) ) );
break;
case XPR_SIZEOF:
- ret = constraintList_addList (ret,
- exprNode_traversTrueEnsuresConstraints
- (exprData_getSingle (data) ) );
+ ret = constraintList_addListFree (ret,
+ exprNode_traversTrueEnsuresConstraints
+ (exprData_getSingle (data) ) );
break;
case XPR_CALL:
- ret = constraintList_addList (ret,
+ ret = constraintList_addListFree (ret,
exprNode_traversTrueEnsuresConstraints
(exprData_getFcn (data) ) );
/*@i11*/ // exprNodeList_unparse (exprData_getArgs (data) );
break;
case XPR_RETURN:
- ret = constraintList_addList (ret,
+ ret = constraintList_addListFree (ret,
exprNode_traversTrueEnsuresConstraints
(exprData_getSingle (data) ) );
break;
break;
case XPR_FACCESS:
- ret = constraintList_addList (ret,
+ ret = constraintList_addListFree (ret,
exprNode_traversTrueEnsuresConstraints
(exprData_getFieldNode (data) ) );
//exprData_getFieldName (data) ;
break;
case XPR_ARROW:
- ret = constraintList_addList (ret,
+ ret = constraintList_addListFree (ret,
exprNode_traversTrueEnsuresConstraints
(exprData_getFieldNode (data) ) );
// exprData_getFieldName (data);
break;
case XPR_POSTOP:
- ret = constraintList_addList (ret,
+ ret = constraintList_addListFree (ret,
exprNode_traversTrueEnsuresConstraints
(exprData_getUopNode (data) ) );
break;
case XPR_CAST:
- ret = constraintList_addList (ret,
+ ret = constraintList_addListFree (ret,
exprNode_traversTrueEnsuresConstraints
(exprData_getCastNode (data) ) );
- break;
-
break;
+
default:
break;
}
if (exprNode_handleError (e))
{
- ret = constraintList_new();
+ ret = constraintList_makeNew();
return ret;
}
ret = constraintList_copy (e->falseEnsuresConstraints );
{
case XPR_WHILEPRED:
t1 = exprData_getSingle (data);
- ret = constraintList_addList ( ret,exprNode_traversFalseEnsuresConstraints (t1) );
+ ret = constraintList_addListFree ( ret,exprNode_traversFalseEnsuresConstraints (t1) );
break;
case XPR_FETCH:
- ret = constraintList_addList (ret,
+ ret = constraintList_addListFree (ret,
exprNode_traversFalseEnsuresConstraints
(exprData_getPairA (data) ) );
- ret = constraintList_addList (ret,
+ ret = constraintList_addListFree (ret,
exprNode_traversFalseEnsuresConstraints
(exprData_getPairB (data) ) );
break;
case XPR_PREOP:
- ret = constraintList_addList (ret,
+ ret = constraintList_addListFree (ret,
exprNode_traversFalseEnsuresConstraints
(exprData_getUopNode (data) ) );
break;
case XPR_PARENS:
- ret = constraintList_addList (ret, exprNode_traversFalseEnsuresConstraints
+ ret = constraintList_addListFree (ret, exprNode_traversFalseEnsuresConstraints
(exprData_getUopNode (data) ) );
break;
case XPR_ASSIGN:
- ret = constraintList_addList (ret,
+ ret = constraintList_addListFree (ret,
exprNode_traversFalseEnsuresConstraints
(exprData_getOpA (data) ) );
- ret = constraintList_addList (ret,
+ ret = constraintList_addListFree (ret,
exprNode_traversFalseEnsuresConstraints
(exprData_getOpB (data) ) );
break;
case XPR_OP:
- ret = constraintList_addList (ret,
+ ret = constraintList_addListFree (ret,
exprNode_traversFalseEnsuresConstraints
(exprData_getOpA (data) ) );
- ret = constraintList_addList (ret,
+ ret = constraintList_addListFree (ret,
exprNode_traversFalseEnsuresConstraints
(exprData_getOpB (data) ) );
break;
case XPR_SIZEOF:
- ret = constraintList_addList (ret,
+ ret = constraintList_addListFree (ret,
exprNode_traversFalseEnsuresConstraints
(exprData_getSingle (data) ) );
break;
case XPR_CALL:
- ret = constraintList_addList (ret,
+ ret = constraintList_addListFree (ret,
exprNode_traversFalseEnsuresConstraints
(exprData_getFcn (data) ) );
/*@i11*/ // exprNodeList_unparse (exprData_getArgs (data) );
break;
case XPR_RETURN:
- ret = constraintList_addList (ret,
+ ret = constraintList_addListFree (ret,
exprNode_traversFalseEnsuresConstraints
(exprData_getSingle (data) ) );
break;
break;
case XPR_FACCESS:
- ret = constraintList_addList (ret,
+ ret = constraintList_addListFree (ret,
exprNode_traversFalseEnsuresConstraints
(exprData_getFieldNode (data) ) );
//exprData_getFieldName (data) ;
break;
case XPR_ARROW:
- ret = constraintList_addList (ret,
+ ret = constraintList_addListFree (ret,
exprNode_traversFalseEnsuresConstraints
(exprData_getFieldNode (data) ) );
// exprData_getFieldName (data);
break;
case XPR_POSTOP:
- ret = constraintList_addList (ret,
+ ret = constraintList_addListFree (ret,
exprNode_traversFalseEnsuresConstraints
(exprData_getUopNode (data) ) );
break;
case XPR_CAST:
- ret = constraintList_addList (ret,
+ ret = constraintList_addListFree (ret,
exprNode_traversFalseEnsuresConstraints
(exprData_getCastNode (data) ) );
break;
/* walk down the tree and get all requires Constraints in each subexpression*/
-constraintList exprNode_traversRequiresConstraints (exprNode e)
+/*@only@*/ constraintList exprNode_traversRequiresConstraints (exprNode e)
{
exprNode t1;
if (exprNode_handleError (e))
{
- ret = constraintList_new();
+ ret = constraintList_makeNew();
return ret;
}
ret = constraintList_copy (e->requiresConstraints );
{
case XPR_WHILEPRED:
t1 = exprData_getSingle (data);
- ret = constraintList_addList ( ret,exprNode_traversRequiresConstraints (t1) );
+ ret = constraintList_addListFree ( ret, exprNode_traversRequiresConstraints (t1) );
break;
case XPR_FETCH:
- ret = constraintList_addList (ret,
+ ret = constraintList_addListFree (ret,
exprNode_traversRequiresConstraints
(exprData_getPairA (data) ) );
- ret = constraintList_addList (ret,
+ ret = constraintList_addListFree (ret,
exprNode_traversRequiresConstraints
(exprData_getPairB (data) ) );
break;
case XPR_PREOP:
- ret = constraintList_addList (ret,
+ ret = constraintList_addListFree (ret,
exprNode_traversRequiresConstraints
(exprData_getUopNode (data) ) );
break;
case XPR_PARENS:
- ret = constraintList_addList (ret, exprNode_traversRequiresConstraints
+ ret = constraintList_addListFree (ret, exprNode_traversRequiresConstraints
(exprData_getUopNode (data) ) );
break;
case XPR_ASSIGN:
- ret = constraintList_addList (ret,
+ ret = constraintList_addListFree (ret,
exprNode_traversRequiresConstraints
(exprData_getOpA (data) ) );
- ret = constraintList_addList (ret,
+ ret = constraintList_addListFree (ret,
exprNode_traversRequiresConstraints
(exprData_getOpB (data) ) );
break;
case XPR_OP:
- ret = constraintList_addList (ret,
+ ret = constraintList_addListFree (ret,
exprNode_traversRequiresConstraints
(exprData_getOpA (data) ) );
- ret = constraintList_addList (ret,
+ ret = constraintList_addListFree (ret,
exprNode_traversRequiresConstraints
(exprData_getOpB (data) ) );
break;
case XPR_SIZEOF:
- ret = constraintList_addList (ret,
+ ret = constraintList_addListFree (ret,
exprNode_traversRequiresConstraints
(exprData_getSingle (data) ) );
break;
case XPR_CALL:
- ret = constraintList_addList (ret,
+ ret = constraintList_addListFree (ret,
exprNode_traversRequiresConstraints
(exprData_getFcn (data) ) );
/*@i11*/ // exprNodeList_unparse (exprData_getArgs (data) );
break;
case XPR_RETURN:
- ret = constraintList_addList (ret,
+ ret = constraintList_addListFree (ret,
exprNode_traversRequiresConstraints
(exprData_getSingle (data) ) );
break;
break;
case XPR_FACCESS:
- ret = constraintList_addList (ret,
+ ret = constraintList_addListFree (ret,
exprNode_traversRequiresConstraints
(exprData_getFieldNode (data) ) );
//exprData_getFieldName (data) ;
break;
case XPR_ARROW:
- ret = constraintList_addList (ret,
+ ret = constraintList_addListFree (ret,
exprNode_traversRequiresConstraints
(exprData_getFieldNode (data) ) );
// exprData_getFieldName (data);
break;
case XPR_POSTOP:
- ret = constraintList_addList (ret,
+ ret = constraintList_addListFree (ret,
exprNode_traversRequiresConstraints
(exprData_getUopNode (data) ) );
break;
case XPR_CAST:
- ret = constraintList_addList (ret,
+ ret = constraintList_addListFree (ret,
exprNode_traversRequiresConstraints
(exprData_getCastNode (data) ) );
break;
/* walk down the tree and get all Ensures Constraints in each subexpression*/
-constraintList exprNode_traversEnsuresConstraints (exprNode e)
+/*@only@*/ constraintList exprNode_traversEnsuresConstraints (exprNode e)
{
exprNode t1;
if (exprNode_handleError (e))
{
- ret = constraintList_new();
+ ret = constraintList_makeNew();
return ret;
}
{
case XPR_WHILEPRED:
t1 = exprData_getSingle (data);
- ret = constraintList_addList ( ret,exprNode_traversEnsuresConstraints (t1) );
+ ret = constraintList_addListFree ( ret,exprNode_traversEnsuresConstraints (t1) );
break;
case XPR_FETCH:
- ret = constraintList_addList (ret,
+ ret = constraintList_addListFree (ret,
exprNode_traversEnsuresConstraints
(exprData_getPairA (data) ) );
- ret = constraintList_addList (ret,
+ ret = constraintList_addListFree (ret,
exprNode_traversEnsuresConstraints
(exprData_getPairB (data) ) );
break;
case XPR_PREOP:
- ret = constraintList_addList (ret,
+ ret = constraintList_addListFree (ret,
exprNode_traversEnsuresConstraints
(exprData_getUopNode (data) ) );
break;
case XPR_PARENS:
- ret = constraintList_addList (ret, exprNode_traversEnsuresConstraints
+ ret = constraintList_addListFree (ret, exprNode_traversEnsuresConstraints
(exprData_getUopNode (data) ) );
break;
case XPR_ASSIGN:
- ret = constraintList_addList (ret,
+ ret = constraintList_addListFree (ret,
exprNode_traversEnsuresConstraints
(exprData_getOpA (data) ) );
- ret = constraintList_addList (ret,
+ ret = constraintList_addListFree (ret,
exprNode_traversEnsuresConstraints
(exprData_getOpB (data) ) );
break;
case XPR_OP:
- ret = constraintList_addList (ret,
+ ret = constraintList_addListFree (ret,
exprNode_traversEnsuresConstraints
(exprData_getOpA (data) ) );
- ret = constraintList_addList (ret,
+ ret = constraintList_addListFree (ret,
exprNode_traversEnsuresConstraints
(exprData_getOpB (data) ) );
break;
case XPR_SIZEOF:
- ret = constraintList_addList (ret,
+ ret = constraintList_addListFree (ret,
exprNode_traversEnsuresConstraints
(exprData_getSingle (data) ) );
break;
case XPR_CALL:
- ret = constraintList_addList (ret,
+ ret = constraintList_addListFree (ret,
exprNode_traversEnsuresConstraints
(exprData_getFcn (data) ) );
/*@i11*/ // exprNodeList_unparse (exprData_getArgs (data) );
break;
case XPR_RETURN:
- ret = constraintList_addList (ret,
+ ret = constraintList_addListFree (ret,
exprNode_traversEnsuresConstraints
(exprData_getSingle (data) ) );
break;
break;
case XPR_FACCESS:
- ret = constraintList_addList (ret,
+ ret = constraintList_addListFree (ret,
exprNode_traversEnsuresConstraints
(exprData_getFieldNode (data) ) );
//exprData_getFieldName (data) ;
break;
case XPR_ARROW:
- ret = constraintList_addList (ret,
+ ret = constraintList_addListFree (ret,
exprNode_traversEnsuresConstraints
(exprData_getFieldNode (data) ) );
// exprData_getFieldName (data);
break;
case XPR_POSTOP:
- ret = constraintList_addList (ret,
+ ret = constraintList_addListFree (ret,
exprNode_traversEnsuresConstraints
(exprData_getUopNode (data) ) );
break;
case XPR_CAST:
- ret = constraintList_addList (ret,
+ ret = constraintList_addListFree (ret,
exprNode_traversEnsuresConstraints
(exprData_getCastNode (data) ) );
break;
andersk / splint.git / blobdiff