# include <ctype.h> /* for isdigit */
# include "lclintMacros.nf"
# include "basic.h"
-# include "cgrammar.h"
+
# include "cgrammar_tokens.h"
# include "exprChecks.h"
-# include "aliasChecks.h"
# include "exprNodeSList.h"
-# include "exprData.i"
-# include "exprDataQuite.i"
+//# include "exprDataQuite.i"
/*@access exprNode @*/
-extern void forLoopHeuristics( exprNode e, exprNode forPred, exprNode forBody);
-bool /*@alt void@*/ exprNode_generateConstraints (/*@temp@*/ exprNode e);
-static bool exprNode_handleError( exprNode p_e);
+static bool exprNode_handleError(/*@dependent@*/ exprNode p_e);
//static cstring exprNode_findConstraints ( exprNode p_e);
-static bool exprNode_isMultiStatement(exprNode p_e);
-static void exprNode_multiStatement (exprNode p_e);
+static bool exprNode_isMultiStatement(/*@dependent@*/ exprNode p_e);
+static void exprNode_multiStatement (/*@dependent@*/ exprNode p_e);
//static void exprNode_constraintPropagateUp (exprNode p_e);
-static constraintList exprNode_traversTrueEnsuresConstraints (exprNode e);
-static constraintList exprNode_traversFalseEnsuresConstraints (exprNode e);
+static constraintList exprNode_traversTrueEnsuresConstraints (/*@dependent@*/ exprNode p_e);
+static constraintList exprNode_traversFalseEnsuresConstraints (/*@dependent@*/ exprNode p_e);
+
+static exprNode makeDataTypeConstraints (/*@returned@*/ exprNode p_e);
-/*@unused@*/ exprNode makeDataTypeConstraints (exprNode e);
-constraintList constraintList_makeFixedArrayConstraints (sRefSet s);
+static void checkArgumentList (/*@out@*/ exprNode p_temp, exprNodeList p_arglist, fileloc p_sequencePoint) /*@modifies p_temp @*/;
+static constraintList checkCall (/*@dependent@*/ exprNode p_fcn, exprNodeList p_arglist);
+
+//constraintList constraintList_makeFixedArrayConstraints (sRefSet s);
//bool exprNode_testd()
//{
*/
//}
-static bool exprNode_isUnhandled (exprNode e)
+static bool exprNode_isUnhandled (/*@dependent@*/ /*@obsever@*/ exprNode e)
{
llassert( exprNode_isDefined(e) );
switch (e->kind)
case XPR_VAARG:
case XPR_ITERCALL:
case XPR_ITER:
- case XPR_CAST:
case XPR_GOTO:
case XPR_CONTINUE:
case XPR_BREAK:
case XPR_TOK:
case XPR_FTDEFAULT:
case XPR_DEFAULT:
- case XPR_SWITCH:
+ // case XPR_SWITCH:
case XPR_FTCASE:
case XPR_CASE:
// case XPR_INIT:
return FALSE;
}
-bool /*@alt void@*/ exprNode_generateConstraints (/*@temp@*/ exprNode e)
+bool /*@alt void@*/ exprNode_generateConstraints (/*@dependent@*/ exprNode e)
{
if (exprNode_isError (e) )
return FALSE;
constraintList c;
c = constraintList_makeFixedArrayConstraints (e->uses);
- e->requiresConstraints = reflectChangesFreePre (e->requiresConstraints, c);
+ e->requiresConstraints = constraintList_reflectChangesFreePre (e->requiresConstraints, c);
// e->ensuresConstraints = constraintList_mergeEnsures(c, e->ensuresConstraints);
case XPR_BLOCK:
case XPR_STMT:
case XPR_STMTLIST:
+ case XPR_SWITCH:
return TRUE;
default:
return FALSE;
}
-static void exprNode_stmt (exprNode e)
+static void exprNode_stmt ( /*@dependent@*/ exprNode e)
{
exprNode snode;
fileloc loc;
}
-static void exprNode_stmtList (exprNode e)
+static void exprNode_stmtList (/*@dependent@*/ exprNode e)
{
exprNode stmt1, stmt2;
if (exprNode_isError (e) )
DPRINTF(("\nstmt after stmtList call " ));
exprNode_stmt (stmt2);
- mergeResolve (e, stmt1, stmt2 );
+ exprNode_mergeResolve (e, stmt1, stmt2 );
DPRINTF ( (message ("smtlist constraints are: pre: %s \n and \t post %s\n",
constraintList_print(e->requiresConstraints),
return; // TRUE;
}
-static exprNode doIf (exprNode e, exprNode test, exprNode body)
+static exprNode doIf (/*@returned@*/ exprNode e, /*@dependent@*/ exprNode test, /*@dependent@*/ exprNode body)
{
constraintList temp;
DPRINTF ((message ("doIf: test true ensures %s ", constraintList_print(test->trueEnsuresConstraints) ) ) );
constraintList_free(e->requiresConstraints);
- e->requiresConstraints = reflectChanges (body->requiresConstraints, test->trueEnsuresConstraints);
+ e->requiresConstraints = constraintList_reflectChanges(body->requiresConstraints, test->trueEnsuresConstraints);
- e->requiresConstraints = reflectChangesFreePre (e->requiresConstraints,
+ e->requiresConstraints = constraintList_reflectChangesFreePre (e->requiresConstraints,
test->ensuresConstraints);
temp = e->requiresConstraints;
e->requiresConstraints = constraintList_mergeRequires (e->requiresConstraints, test->requiresConstraints);
constraintList_free(temp);
-#warning bad
+//drl possible problem : warning bad
constraintList_free(e->ensuresConstraints);
e->ensuresConstraints = constraintList_copy (test->ensuresConstraints);
*/
-static exprNode doIfElse (/*@returned@*/ exprNode e, exprNode p, exprNode trueBranch, exprNode falseBranch)
+static exprNode doIfElse (/*@returned@*/ exprNode e, /*@dependent@*/ exprNode p, /*@dependent@*/ exprNode trueBranch, /*@dependent@*/ exprNode falseBranch)
{
constraintList c1, cons, t, t2, f, f2;
// do requires clauses
c1 = constraintList_copy (p->ensuresConstraints);
- t = reflectChanges (trueBranch->requiresConstraints, p->trueEnsuresConstraints);
- t = reflectChangesFreePre (t, p->ensuresConstraints);
+ t = constraintList_reflectChanges(trueBranch->requiresConstraints, p->trueEnsuresConstraints);
+ t = constraintList_reflectChangesFreePre (t, p->ensuresConstraints);
- cons = reflectChanges (falseBranch->requiresConstraints, p->falseEnsuresConstraints);
- cons = reflectChangesFreePre (cons, c1);
+ cons = constraintList_reflectChanges(falseBranch->requiresConstraints, p->falseEnsuresConstraints);
+ cons = constraintList_reflectChangesFreePre (cons, c1);
constraintList_free(e->requiresConstraints);
e->requiresConstraints = constraintList_mergeRequiresFreeFirst (t, cons);
return e;
}
-static exprNode doWhile (exprNode e, exprNode test, exprNode body)
+static exprNode doWhile (/*@returned@*/ exprNode e, /*@dependent@*/ exprNode test, /*@dependent@*/ exprNode body)
{
DPRINTF ((message ("doWhile: %s ", exprNode_unparse(e) ) ) );
return doIf (e, test, body);
}
-constraintList constraintList_makeFixedArrayConstraints (sRefSet s)
+/*@only@*/ constraintList constraintList_makeFixedArrayConstraints (/*@observer@*/ sRefSet s)
{
constraintList ret;
constraint con;
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;
}
-static void doFor (exprNode e, exprNode forPred, exprNode forBody)
+static void doFor (/*@dependent@*/ exprNode e, /*@dependent@*/ exprNode forPred, /*@dependent@*/ exprNode forBody)
{
exprNode init, test, inc;
//merge the constraints: modle as if statement
return;
}
- forLoopHeuristics(e, forPred, forBody);
+ exprNode_forLoopHeuristics(e, forPred, forBody);
constraintList_free(e->requiresConstraints);
- e->requiresConstraints = reflectChanges (forBody->requiresConstraints, test->ensuresConstraints);
- e->requiresConstraints = reflectChangesFreePre (e->requiresConstraints, test->trueEnsuresConstraints);
- e->requiresConstraints = reflectChangesFreePre (e->requiresConstraints, forPred->ensuresConstraints);
+ e->requiresConstraints = constraintList_reflectChanges(forBody->requiresConstraints, test->ensuresConstraints);
+ e->requiresConstraints = constraintList_reflectChangesFreePre (e->requiresConstraints, test->trueEnsuresConstraints);
+ e->requiresConstraints = constraintList_reflectChangesFreePre (e->requiresConstraints, forPred->ensuresConstraints);
if (!forBody->canBreak)
{
- e->ensuresConstraints = constraintList_addList(e->ensuresConstraints, constraintList_copy(forPred->ensuresConstraints) );
- e->ensuresConstraints = constraintList_addList(e->ensuresConstraints,constraintList_copy( 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;
}
exprData data;
data = e->edata;
- llassert(FALSE);
- //DPRINTF (( message ("doSwitch for: switch (%s) %s",
- // exprNode_unparse (exprData_getPairA (data)),
- // exprNode_unparse (exprData_getPairB (data))) ));
-
+ // llassert(FALSE);
+ DPRINTF (( message ("doSwitch for: switch (%s) %s",
+ exprNode_unparse (exprData_getPairA (data)),
+ exprNode_unparse (exprData_getPairB (data))) ));
+
body = exprData_getPairB (data);
- // exprNode_generateConstraints(body);
+ exprNode_generateConstraints(body);
- // e->requiresConstraints = constraintList_copy ( body->requiresConstraints );
- //e->ensuresConstraints = constraintList_copy ( body->ensuresConstraints );
+ constraintList_free(e->requiresConstraints);
+ constraintList_free(e->ensuresConstraints);
+
+ e->requiresConstraints = NULL;
+ e->ensuresConstraints = NULL;
+
+ e->requiresConstraints = constraintList_copy ( body->requiresConstraints );
+ e->ensuresConstraints = constraintList_copy ( body->ensuresConstraints );
return e;
}
-void exprNode_multiStatement (exprNode e)
+void exprNode_multiStatement (/*@dependent@*/ exprNode e)
{
bool ret;
}
-static void exprNode_booleanTraverse (exprNode e, /*@unused@*/ bool definatelv, /*@unused@*/ bool definaterv, fileloc sequencePoint)
+static void exprNode_booleanTraverse (/*@dependent@*/ exprNode e, /*@unused@*/ bool definatelv, /*@unused@*/ bool definaterv, fileloc sequencePoint)
{
constraint cons;
exprNode t1, t2;
t2 = exprData_getOpB (data);
+ tempList = constraintList_undefined;
+
/* arithmetic tests */
if (lltok_isEq_Op (tok) )
/*Logical operations */
+
if (lltok_isAnd_Op (tok) )
{
//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);
//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);
constraintList_free(temp);
- e->trueEnsuresConstraints =constraintList_addList(e->trueEnsuresConstraints, tempList);
+ e->trueEnsuresConstraints =constraintList_addListFree(e->trueEnsuresConstraints, tempList);
+ tempList = constraintList_undefined;
+
}
else
}
-void exprNode_exprTraverse (exprNode e, bool definatelv, bool definaterv, /*@observer@*/ fileloc sequencePoint)
+void exprNode_exprTraverse (exprNode e, bool definatelv, bool definaterv, /*@observer@*/ /*@temp@*/ fileloc sequencePoint)
{
exprNode t1, t2, fcn;
lltok tok;
switch (e->kind)
{
-
-
case XPR_WHILEPRED:
t1 = exprData_getSingle (data);
exprNode_exprTraverse (t1, definatelv, definaterv, sequencePoint);
// e->constraints = constraintList_exprNodemerge (exprData_getUopNode (e->edata), exprNode_undefined);
break;
case XPR_INIT:
- /* //t1 = exprData_getInitId (data); */
- t2 = exprData_getInitNode (data);
- //exprNode_exprTraverse (t1, TRUE, FALSE, sequencePoint );
-
- exprNode_exprTraverse (t2, definatelv, TRUE, sequencePoint );
-
- /* this test is nessecary because some expressions generate a null expression node. function pointer do that -- drl */
+ {
+ /*
+ 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)
+ )
+ ) )); */
+
+ //exprNode_exprTraverse (t1, TRUE, FALSE, sequencePoint );
+
+ 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)) )
- {
- cons = constraint_makeEnsureEqual (e, t2, sequencePoint);
- e->ensuresConstraints = constraintList_add(e->ensuresConstraints, cons);
- }
+ {
+ cons = constraint_makeEnsureEqual (e, t2, sequencePoint);
+ e->ensuresConstraints = constraintList_add(e->ensuresConstraints, cons);
+ }
+ }
break;
case XPR_ASSIGN:
t2 = exprData_getOpB (data);
exprNode_exprTraverse (t1, TRUE, definaterv, sequencePoint );
//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 */
case XPR_OP:
t1 = exprData_getOpA (data);
t2 = exprData_getOpB (data);
-
- exprNode_exprTraverse (t1, definatelv, definaterv, sequencePoint );
tok = exprData_getOpTok (data);
- exprNode_exprTraverse (t2, definatelv, definaterv, sequencePoint );
+
+
+ if (tok.tok == ADD_ASSIGN)
+ {
+ exprNode_exprTraverse (t1, TRUE, definaterv, sequencePoint );
+ exprNode_exprTraverse (t2, definatelv, TRUE, sequencePoint );
+ cons = constraint_makeAddAssign (t1, t2, sequencePoint );
+ e->ensuresConstraints = constraintList_add(e->ensuresConstraints, cons);
+ }
+ else if (tok.tok == SUB_ASSIGN)
+ {
+ exprNode_exprTraverse (t1, TRUE, definaterv, sequencePoint );
+ exprNode_exprTraverse (t2, definatelv, TRUE, sequencePoint );
+
+ cons = constraint_makeSubtractAssign (t1, t2, sequencePoint );
+ e->ensuresConstraints = constraintList_add(e->ensuresConstraints, cons);
+ }
+ else
+ {
+ exprNode_exprTraverse (t1, definatelv, definaterv, sequencePoint );
+ exprNode_exprTraverse (t2, definatelv, definaterv, sequencePoint );
+ }
+
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:
- #warning make sure the case can be ignored..
+ //drl possible problem : warning make sure the case can be ignored..
break;
exprNode_exprTraverse (fcn, definatelv, definaterv, sequencePoint );
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,
- getPostConditions(fcn, exprData_getArgs (data),e ) );
+ 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);
- mergeResolve (e, t1, fcn);
+ exprNode_mergeResolve (e, t1, fcn);
+
+ exprNode_free(t1);
// e->constraints = constraintList_add (e->constraints, constraint_create (e,exprNode_undefined, GT, CALLSAFE ) );
+
break;
case XPR_RETURN:
{
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) ) ));
}
break;
case XPR_CAST:
- llassert(FALSE);
- exprNode_exprTraverse (exprData_getCastNode (data), definatelv, definaterv, sequencePoint );
+ {
+ t2 = exprData_getCastNode (data);
+ DPRINTF (( message ("Examining cast (%q)%s",
+ qtype_unparse (exprData_getCastType (data)),
+ exprNode_unparse (t2) )
+ ));
+ exprNode_exprTraverse (t2, definatelv, definaterv, sequencePoint );
+ }
break;
+
case XPR_COND:
{
- exprNode pred, true, false;
+ exprNode pred, trueBranch, falseBranch;
llassert(FALSE);
pred = exprData_getTriplePred (data);
- true = exprData_getTripleTrue (data);
- false = exprData_getTripleFalse (data);
+ trueBranch = exprData_getTripleTrue (data);
+ falseBranch = exprData_getTripleFalse (data);
exprNode_exprTraverse (pred, FALSE, TRUE, sequencePoint );
constraintList_free(temp);
- exprNode_exprTraverse (true, FALSE, TRUE, sequencePoint );
+ exprNode_exprTraverse (trueBranch, FALSE, TRUE, sequencePoint );
- temp = true->ensuresConstraints;
- true->ensuresConstraints = exprNode_traversEnsuresConstraints(true);
+ temp = trueBranch->ensuresConstraints;
+ trueBranch->ensuresConstraints = exprNode_traversEnsuresConstraints(trueBranch);
constraintList_free(temp);
- temp = true->requiresConstraints;
- true->requiresConstraints = exprNode_traversRequiresConstraints(true);
+ temp = trueBranch->requiresConstraints;
+ trueBranch->requiresConstraints = exprNode_traversRequiresConstraints(trueBranch);
constraintList_free(temp);
- temp = true->trueEnsuresConstraints;
- true->trueEnsuresConstraints = exprNode_traversTrueEnsuresConstraints(true);
+ temp = trueBranch->trueEnsuresConstraints;
+ trueBranch->trueEnsuresConstraints = exprNode_traversTrueEnsuresConstraints(trueBranch);
constraintList_free(temp);
- temp = true->falseEnsuresConstraints;
- true->falseEnsuresConstraints = exprNode_traversFalseEnsuresConstraints(true);
+ temp = trueBranch->falseEnsuresConstraints;
+ trueBranch->falseEnsuresConstraints = exprNode_traversFalseEnsuresConstraints(trueBranch);
constraintList_free(temp);
//dfdf
- exprNode_exprTraverse (false, FALSE, TRUE, sequencePoint );
+ exprNode_exprTraverse (falseBranch, FALSE, TRUE, sequencePoint );
- temp = false->ensuresConstraints;
- false->ensuresConstraints = exprNode_traversEnsuresConstraints(false);
+ temp = falseBranch->ensuresConstraints;
+ falseBranch->ensuresConstraints = exprNode_traversEnsuresConstraints(falseBranch);
constraintList_free(temp);
- temp = false->requiresConstraints;
- false->requiresConstraints = exprNode_traversRequiresConstraints(false);
+ temp = falseBranch->requiresConstraints;
+ falseBranch->requiresConstraints = exprNode_traversRequiresConstraints(falseBranch);
constraintList_free(temp);
- temp = false->trueEnsuresConstraints;
- false->trueEnsuresConstraints = exprNode_traversTrueEnsuresConstraints(false);
+ temp = falseBranch->trueEnsuresConstraints;
+ falseBranch->trueEnsuresConstraints = exprNode_traversTrueEnsuresConstraints(falseBranch);
constraintList_free(temp);
- temp = false->falseEnsuresConstraints;
- false->falseEnsuresConstraints = exprNode_traversFalseEnsuresConstraints(false);
+ temp = falseBranch->falseEnsuresConstraints;
+ falseBranch->falseEnsuresConstraints = exprNode_traversFalseEnsuresConstraints(falseBranch);
constraintList_free(temp);
/* if pred is true e equals true otherwise pred equals false */
- cons = constraint_makeEnsureEqual (e, true, sequencePoint);
- true->ensuresConstraints = constraintList_add(true->ensuresConstraints, cons);
+ cons = constraint_makeEnsureEqual (e, trueBranch, sequencePoint);
+ trueBranch->ensuresConstraints = constraintList_add(trueBranch->ensuresConstraints, cons);
- cons = constraint_makeEnsureEqual (e, true, sequencePoint);
- false->ensuresConstraints = constraintList_add(false->ensuresConstraints, cons);
+ cons = constraint_makeEnsureEqual (e, trueBranch, sequencePoint);
+ falseBranch->ensuresConstraints = constraintList_add(falseBranch->ensuresConstraints, cons);
- e = doIfElse (e, pred, true, false);
+ e = doIfElse (e, pred, trueBranch, falseBranch);
}
break;
problems../ */
exprNode_exprTraverse (t1, FALSE, FALSE, sequencePoint );
exprNode_exprTraverse (t2, definatelv, definaterv, sequencePoint );
- mergeResolve (e, t1, t2);
+ exprNode_mergeResolve (e, t1, t2);
break;
-
+
default:
handledExprNode = FALSE;
}
exprData data;
constraintList ret;
- if (exprNode_handleError (e))
- {
- ret = constraintList_makeNew();
- return ret;
- }
+ if (exprNode_handleError (e))
+ {
+ ret = constraintList_makeNew();
+ return ret;
+ }
ret = constraintList_copy (e->trueEnsuresConstraints );
- handledExprNode = TRUE;
+ handledExprNode = TRUE;
data = e->edata;
{
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_INIT:
+ ret = constraintList_addListFree (ret,
+ exprNode_traversTrueEnsuresConstraints
+ (exprData_getInitNode (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;
{
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_INIT:
+ ret = constraintList_addListFree (ret,
+ exprNode_traversFalseEnsuresConstraints
+ ( exprData_getInitNode (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;
{
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_INIT:
+ ret = constraintList_addListFree (ret,
+ exprNode_traversRequiresConstraints
+ (exprData_getInitNode (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;
{
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_INIT:
+ ret = constraintList_addListFree (ret,
+ exprNode_traversEnsuresConstraints
+ (exprData_getInitNode (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;
return ret;
}
+/*drl moved out of constraintResolve.c 07-02-001 */
+void checkArgumentList (/*@out@*/ exprNode temp, exprNodeList arglist, fileloc sequencePoint)
+{
+ temp->requiresConstraints = constraintList_makeNew();
+ temp->ensuresConstraints = constraintList_makeNew();
+ temp->trueEnsuresConstraints = constraintList_makeNew();
+ temp->falseEnsuresConstraints = constraintList_makeNew();
+
+ exprNodeList_elements (arglist, el)
+ {
+ constraintList temp2;
+ exprNode_exprTraverse (el, FALSE, FALSE, sequencePoint);
+ temp2 = el->requiresConstraints;
+ el->requiresConstraints = exprNode_traversRequiresConstraints(el);
+ constraintList_free(temp2);
+
+ temp2 = el->ensuresConstraints;
+ el->ensuresConstraints = exprNode_traversEnsuresConstraints(el);
+ constraintList_free(temp2);
+
+ temp->requiresConstraints = constraintList_addList(temp->requiresConstraints,
+ el->requiresConstraints);
+
+ temp->ensuresConstraints = constraintList_addList(temp->ensuresConstraints,
+ el->ensuresConstraints);
+ }
+ end_exprNodeList_elements;
+
+}
+
+/*drl moved out of constraintResolve.c 07-03-001 */
+constraintList exprNode_getPostConditions (exprNode fcn, exprNodeList arglist, exprNode fcnCall)
+{
+ constraintList postconditions;
+ uentry temp;
+ DPRINTF( (message ("Got call that %s ( %s) ", exprNode_unparse(fcn), exprNodeList_unparse (arglist ) ) ) );
+
+ temp = exprNode_getUentry (fcn);
+
+ postconditions = uentry_getFcnPostconditions (temp);
+
+ if (constraintList_isDefined(postconditions) )
+ {
+ postconditions = constraintList_doSRefFixConstraintParam (postconditions, arglist);
+ postconditions = constraintList_doFixResult (postconditions, fcnCall);
+ }
+ else
+ {
+ postconditions = constraintList_makeNew();
+ }
+
+ return postconditions;
+}
+
+
+/*drl moved out of constraintResolve.c 07-02-001 */
+constraintList checkCall (/*@dependent@*/ exprNode fcn, exprNodeList arglist)
+{
+ constraintList preconditions;
+ uentry temp;
+ DPRINTF( (message ("Got call that %s ( %s) ", exprNode_unparse(fcn), exprNodeList_unparse (arglist ) ) ) );
+
+ temp = exprNode_getUentry (fcn);
+
+ preconditions = uentry_getFcnPreconditions (temp);
+
+ if (constraintList_isDefined(preconditions) )
+ {
+ preconditions = constraintList_togglePost (preconditions);
+ preconditions = constraintList_preserveCallInfo(preconditions, fcn);
+ preconditions = constraintList_doSRefFixConstraintParam (preconditions, arglist);
+ }
+ else
+ {
+ if (constraintList_isUndefined(preconditions) )
+ preconditions = constraintList_makeNew();
+ }
+ DPRINTF (( message("Done checkCall\n") ));
+ DPRINTF (( message("Returning list %q ", constraintList_printDetailed(preconditions) ) ));
+ return preconditions;
+}
andersk / splint.git / blobdiff