/*
** Splint - annotation-assisted static program checker
-** Copyright (C) 1994-2002 University of Virginia,
+** Copyright (C) 1994-2003 University of Virginia,
** Massachusetts Institute of Technology
**
** This program is free software; you can redistribute it and/or modify it
# include "exprChecks.h"
# include "exprNodeSList.h"
-/*@access exprNode@*/ /* NO! Don't do this recklessly! */
-/*@-nullderef@*/ /* DRL needs to fix this code! */
-/*@-nullpass@*/ /* DRL needs to fix this code! */
-/*@-temptrans@*/ /* DRL needs to fix this code! */
+/*drl We need to access the internal representation of exprNode
+ because these functions walk down the parse tree and need a richer
+information than is accessible through the exprNode interface.*/
+
+/*@access exprNode@*/
-static /*@truewhennull@*/ bool exprNode_handleError (/*@temp@*/ exprNode p_e);
+static /*@nullwhentrue@*/ bool exprNode_handleError (/*@temp@*/ exprNode p_e);
static void exprNode_stmt (/*@temp@*/ /*@temp@*/ exprNode p_e);
static void exprNode_multiStatement (/*@temp@*/ exprNode p_e);
return FALSE;
}
-bool exprNode_handleError (exprNode e)
+/*@nullwhentrue@*/ bool exprNode_handleError (exprNode e)
{
if (exprNode_isError (e) || exprNode_isUnhandled (e))
{
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;
DPRINTF((message("exprNode_doGenerateConstraintSwitch: (switch %s) %s savedRequires:"
"%s savedEnsures:%s",
exprNode_unparse(switchExpr), exprNode_unparse(body),
- constraintList_print(*savedRequires), constraintList_print(*savedEnsures)
+ constraintList_unparse(*savedRequires), constraintList_unparse(*savedEnsures)
)));
}
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;
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 */
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;
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);
+ {
+ exprNode tempExpr;
+
+ tempExpr = exprData_getSingle (data);
+
+ exprNode_generateConstraints (tempExpr);
+
+ if (exprNode_isDefined(tempExpr) )
+ {
+ constraintList_free(e->requiresConstraints);
+ e->requiresConstraints = constraintList_copy (tempExpr->requiresConstraints);
+ constraintList_free(e->ensuresConstraints);
+ e->ensuresConstraints = constraintList_copy (tempExpr->ensuresConstraints);
+ }
+ else
+ {
+ llassert(FALSE);
+ }
+ }
break;
case XPR_SWITCH:
I don't want to violate the abstraction
maybe this should go in lltok.c */
- if (lltok_isEq_Op (tok))
+ if (lltok_isEqOp (tok))
{
return TRUE;
}
- if (lltok_isAnd_Op (tok))
+ if (lltok_isAndOp (tok))
{
return TRUE;
}
- if (lltok_isOr_Op (tok))
+ if (lltok_isOrOp (tok))
{
return TRUE;
}
exprData data;
lltok tok;
constraintList tempList, temp;
+
+ if (exprNode_isUndefined(e) )
+ {
+ llassert (exprNode_isDefined(e) );
+ return;
+ }
+
data = e->edata;
tok = exprData_getOpTok (data);
t1 = exprData_getOpA (data);
t2 = exprData_getOpB (data);
+
+ /* drl 3/2/2003 we know this because of the type of expression*/
+ llassert( exprNode_isDefined(t1) && exprNode_isDefined(t2) );
+
tempList = constraintList_undefined;
/* arithmetic tests */
- if (lltok_isEq_Op (tok))
+ if (lltok_isEqOp (tok))
{
cons = constraint_makeEnsureEqual (t1, t2, sequencePoint);
e->trueEnsuresConstraints = constraintList_add(e->trueEnsuresConstraints, cons);
/* Logical operations */
- if (lltok_isAnd_Op (tok))
+ if (lltok_isAndOp (tok))
{
/* true ensures */
tempList = constraintList_copy (t1->trueEnsuresConstraints);
/* evans - was constraintList_addList - memory leak detected by splint */
e->falseEnsuresConstraints = constraintList_addListFree (e->falseEnsuresConstraints, tempList);
}
- else if (lltok_isOr_Op (tok))
+ else if (lltok_isOrOp (tok))
{
/* false ensures */
tempList = constraintList_copy (t1->falseEnsuresConstraints);
}
}
-void exprNode_exprTraverse (exprNode e, bool definatelv, bool definaterv, /*@observer@*/ /*@temp@*/ fileloc sequencePoint)
+void exprNode_exprTraverse (/*@dependent@*/ exprNode e, bool definatelv, bool definaterv, /*@observer@*/ /*@temp@*/ fileloc sequencePoint)
{
exprNode t1, t2, fcn;
lltok tok;
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;
exprNode_exprTraverse (fcn, definatelv, definaterv, sequencePoint);
DPRINTF ((message ("Got call that %s (%s) ", exprNode_unparse(fcn), exprNodeList_unparse (exprData_getArgs (data)))));
+ llassert( exprNode_isDefined(fcn) );
+
fcn->requiresConstraints = constraintList_addListFree (fcn->requiresConstraints,
checkCall (fcn, exprData_getArgs (data) ));
case XPR_PREOP:
t1 = exprData_getUopNode(data);
+
+
+ /* drl 3/2/2003 we know this because of the type of expression*/
+ llassert( exprNode_isDefined(t1) );
+
+
tok = (exprData_getUopTok (data));
exprNode_exprTraverse (t1, definatelv, definaterv, sequencePoint);
/*handle * pointer access */
- if (lltok_isInc_Op (tok))
+ if (lltok_isIncOp (tok))
{
DPRINTF(("doing ++(var)"));
t1 = exprData_getUopNode (data);
cons = constraint_makeMaxSetSideEffectPostIncrement (t1, sequencePoint);
e->ensuresConstraints = constraintList_add (e->ensuresConstraints, cons);
}
- else if (lltok_isDec_Op (tok))
+ else if (lltok_isDecOp (tok))
{
DPRINTF(("doing --(var)"));
t1 = exprData_getUopNode (data);
}
e->requiresConstraints = constraintList_add(e->requiresConstraints, cons);
}
- else if (lltok_isNot_Op (tok))
+ else if (lltok_isNotOp (tok))
/* ! expr */
{
constraintList_free(e->trueEnsuresConstraints);
exprNode_exprTraverse (exprData_getUopNode (data), TRUE,
definaterv, sequencePoint);
- if (lltok_isInc_Op (exprData_getUopTok (data)))
+ if (lltok_isIncOp (exprData_getUopTok (data)))
{
DPRINTF(("doing ++"));
t1 = exprData_getUopNode (data);
cons = constraint_makeMaxSetSideEffectPostIncrement (t1, sequencePoint);
e->ensuresConstraints = constraintList_add (e->ensuresConstraints, cons);
}
- if (lltok_isDec_Op (exprData_getUopTok (data)))
+ if (lltok_isDecOp (exprData_getUopTok (data)))
{
DPRINTF(("doing --"));
t1 = exprData_getUopNode (data);
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;
}
void checkArgumentList (/*@out@*/ exprNode temp, exprNodeList arglist,
fileloc sequencePoint)
{
+
+ llassert(temp != NULL );
+
temp->requiresConstraints = constraintList_makeNew();
temp->ensuresConstraints = constraintList_makeNew();
temp->trueEnsuresConstraints = constraintList_makeNew();
exprNodeList_elements (arglist, el)
{
constraintList temp2;
+
+ llassert(exprNode_isDefined(el) );
+
exprNode_exprTraverse (el, FALSE, FALSE, sequencePoint);
temp2 = el->requiresConstraints;
el->requiresConstraints = exprNode_traversRequiresConstraints(el);
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))
));
}
}
preconditions = constraintList_makeNew();
}
- /*@i523@ drl remember to remove this code before you make a splint release. */
- /*
if (context_getFlag (FLG_IMPLICTCONSTRAINT) )
{
-
- uentryList_elements (params, el)
+
+ /*
+ uentryList_elements (arglist, el)
{
- DPRINTF((message("setImplictfcnConstraints doing: %s", uentry_unparse(el) ) ));
+ sRef s;
+ TPRINTF((message("setImplictfcnConstraints doing: %s", uentry_unparse(el) ) ));
s = uentry_getSref(el);
if (sRef_isReference (s) )
{
- DPRINTF((message ("%s is a pointer", sRef_unparse(s) ) ));
+ TPRINTF((message ("%s is a pointer", sRef_unparse(s) ) ));
}
else
{
- DPRINTF((message ("%s is NOT a pointer", sRef_unparse(s) ) ));
+ TPRINTF((message ("%s is NOT a pointer", sRef_unparse(s) ) ));
}
//drl 4/26/01
//chagned this from MaxSet(s) == 0 to MaxSet(s) >= 0
if (!uentry_isOut(el) )
{
c = constraint_makeSRefReadSafeInt (s, 0);
-
implicitFcnConstraints = constraintList_add(implicitFcnConstraints , c);
}
-
+
}
-
+ */
}
- */
+
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;
exprNode t1, t2;
lltok tok;
+ llassert(exprNode_isDefined(e) );
+
data = e->edata;
if (exprNode_hasValue(e))
andersk / splint.git / blobdiff