# include "exprChecks.h"
# include "exprNodeSList.h"
-/*@access exprNode @*/
-
+/*@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! */
static /*@truewhennull@*/ bool exprNode_handleError (/*@temp@*/ exprNode p_e);
{
if (sRef_isFixedArray(el))
{
- long int size;
+ size_t size;
DPRINTF((message("%s is a fixed array",
sRef_unparse(el))));
size = sRef_getArraySize(el);
static /*@dependent@*/ exprNode exprNode_makeDependent(/*@returned@*/ exprNode e)
{
- /*@-temptrans@*/
+ /* !!! DRL - this is ridiculous! Read the manual on memory annotations please! */
return e;
- /*@=temptrans@*/
}
static void
p->trueEnsuresConstraints = exprNode_traversTrueEnsuresConstraints(p);
constraintList_free(temp);
+
+
+ DPRINTF((message("p->trueEnsuresConstraints before substitue %s", constraintList_print(p->trueEnsuresConstraints) )
+ ));
+
+ /*drl 10/10/2002 this is a bit of a hack but the reason why we do this is so that any function post conditions or similar things get applied correctly to each branch. e.g. in strlen(s) < 5 we want the trueEnsures to be maxRead(s) < 5*/
+
+ p->trueEnsuresConstraints = constraintList_substituteFreeTarget (p->trueEnsuresConstraints,
+ p->ensuresConstraints);
+
+ DPRINTF(( message ("p->trueEnsuresConstraints after substitue %s", constraintList_print(p->trueEnsuresConstraints) )
+ ));
+
temp = p->falseEnsuresConstraints;
p->falseEnsuresConstraints = exprNode_traversFalseEnsuresConstraints(p);
constraintList_free(temp);
+ /*See comment on trueEnsures*/
+ p->falseEnsuresConstraints = constraintList_substituteFreeTarget (p->falseEnsuresConstraints,
+ p->ensuresConstraints);
+
e = doIfElse (e, p, trueBranch, falseBranch);
DPRINTF(("Done IFELSE"));
break;
-
+
case XPR_DOWHILE:
e2 = (exprData_getPairB (data));
t2 = exprData_getOpB (data);
tok = exprData_getOpTok (data);
- if (tok.tok == ADD_ASSIGN)
+ if (lltok_getTok (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)
+ else if (lltok_getTok (tok) == SUB_ASSIGN)
{
exprNode_exprTraverse (t1, TRUE, definaterv, sequencePoint);
exprNode_exprTraverse (t2, definatelv, TRUE, sequencePoint);
if (constraintList_isUndefined(preconditions))
preconditions = constraintList_makeNew();
}
+
+ // drl remember to remove this code before you make a pslint release.
+ /*
+ if (context_getFlag (FLG_IMPLICTCONSTRAINT) )
+ {
+
+ uentryList_elements (params, el)
+ {
+ DPRINTF((message("setImplictfcnConstraints doing: %s", uentry_unparse(el) ) ));
+
+ s = uentry_getSref(el);
+ if (sRef_isReference (s) )
+ {
+ DPRINTF((message ("%s is a pointer", sRef_unparse(s) ) ));
+ }
+ else
+ {
+ DPRINTF((message ("%s is NOT a pointer", sRef_unparse(s) ) ));
+ }
+ //drl 4/26/01
+ //chagned this from MaxSet(s) == 0 to MaxSet(s) >= 0
+ c = constraint_makeSRefWriteSafeInt (s, 0);
+
+ implicitFcnConstraints = constraintList_add(implicitFcnConstraints , c);
+
+ //drl 10/23/2002 added support for out
+ 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))));