# include "aliasChecks.h"
# include "exprNodeSList.h"
-# include "exprData.i"
# include "exprDataQuite.i"
+/*@access constraint, exprNode @*/
+
+/*@access constraintExpr @*/
+
+static bool isInc (/*@observer@*/ constraintExpr c) /*@*/
+{
+
+ llassert(constraintExpr_isDefined(c) );
+ if (c->kind == binaryexpr )
+ {
+ constraintExprBinaryOpKind binOP;
+ constraintExpr t1, t2;
+ t1 = constraintExprData_binaryExprGetExpr1 (c->data);
+ t2 = constraintExprData_binaryExprGetExpr2 (c->data);
+
+ binOP = constraintExprData_binaryExprGetOp (c->data);
+ if (binOP == PLUS)
+ if (constraintExpr_isLit (t2) && constraintExpr_getValue (t2) == 1 )
+ {
+ return TRUE;
+ }
+ }
+
+ return FALSE;
+}
+
+
// look for constraints like cexrp = cexrp + 1
-static bool incVar (constraint c)
+static bool incVar (/*@notnull@*/ constraint c) /*@*/
{
constraintExpr t1;
if (c->ar != EQ)
if (! isInc (c->expr ) )
return FALSE;
+ llassert (constraintExpr_isDefined(c->expr) );
llassert (c->expr->kind == binaryexpr);
+
t1 = constraintExprData_binaryExprGetExpr1 (c->expr->data);
if (constraintExpr_similar (c->lexpr, t1) )
return TRUE;
return FALSE;
}
+/*@noaccess constraintExpr @*/
-static bool increments (constraint c,
- constraintExpr var)
+static bool increments (/*@observer@*/ constraint c,
+ /*@observer@*/ constraintExpr var)
{
+ llassert(constraint_isDefined(c) );
+
+ if (constraint_isUndefined(c) )
+ {
+ return FALSE;
+ }
+
llassert (incVar (c));
if (constraintExpr_similar (c->lexpr, var) )
return TRUE;
return FALSE;
}
-static bool canGetForTimes ( exprNode forPred, exprNode forBody)
+static bool canGetForTimes (/*@notnull@*/ exprNode forPred, /*@notnull@*/ exprNode forBody)
{
exprNode init, test, inc, t1, t2;
lltok tok;
+ llassert(exprNode_isDefined (forPred) );
+ llassert(exprNode_isDefined (forBody) );
+
init = exprData_getTripleInit (forPred->edata);
test = exprData_getTripleTest (forPred->edata);
inc = exprData_getTripleInc (forPred->edata);
-
+ llassert(exprNode_isDefined(test) );
+
+ if (exprNode_isUndefined(test) )
+ {
+ return FALSE;
+ }
+
+ llassert(exprNode_isDefined(inc) );
+
+ if (exprNode_isUndefined(inc) )
+ {
+ return FALSE;
+ }
+
if (test->kind != XPR_PREOP)
return FALSE;
{
t1 = exprData_getUopNode (test->edata);
t2 = exprData_getUopNode (inc->edata);
+ llassert(exprNode_isDefined(t2) && exprNode_isDefined(t2) );
+
+ if (exprNode_isUndefined(t1) || exprNode_isUndefined(t2) )
+ {
+ return FALSE;
+ }
+
if (sRef_sameName (t1->sref, t2->sref) )
{
return TRUE;
return FALSE;
}
-static constraintList getLessThanConstraints (constraintList c)
+static /*@only@*/ constraintList getLessThanConstraints (/*@observer@*/ constraintList c)
{
constraintList ret;
- ret = constraintList_new();
+ ret = constraintList_makeNew();
constraintList_elements (c, el)
{
+ llassert(constraint_isDefined(el));
+ if ( constraint_isUndefined(el) )
+ continue;
+
if (el->ar == LT || el->ar == LTE)
{
- ret = constraintList_add (ret, el);
+ constraint temp;
+ temp = constraint_copy(el);
+
+ ret = constraintList_add (ret, temp);
}
}
end_constraintList_elements;
return ret;
}
-static constraintList getIncConstraints (constraintList c)
+static /*@only@*/ constraintList getIncConstraints (/*@observer@*/ constraintList c)
{
constraintList ret;
- ret = constraintList_new();
+ ret = constraintList_makeNew();
constraintList_elements (c, el)
{
if (incVar (el) )
{
- ret = constraintList_add (ret, el);
+ constraint temp;
+ temp = constraint_copy(el);
+ ret = constraintList_add (ret, temp);
}
}
end_constraintList_elements;
return ret;
}
-constraintExpr getForTimes ( exprNode forPred, exprNode forBody)
+static /*@only@*/ constraintExpr getForTimes (/*@notnull@*/ exprNode forPred, /*@notnull@*/ exprNode forBody)
{
exprNode init, test, inc, t1, t2;
constraintList ltCon;
constraintList incCon;
+ constraintExpr ret;
lltok tok;
test = exprData_getTripleTest (forPred->edata);
inc = exprData_getTripleInc (forPred->edata);
- llassert(test);
- llassert(inc);
+ llassert(exprNode_isDefined(test) );
+ llassert(exprNode_isDefined(inc) );
ltCon = getLessThanConstraints (test->trueEnsuresConstraints);
incCon = getIncConstraints (inc->ensuresConstraints);
if ( increments(el2, el->lexpr) )
{
DPRINTF(( message ("getForTimes: %s increments %s", constraint_print(el2), constraint_print(el) ) ));
- return constraintExpr_copy (el->expr);
+ ret = constraintExpr_copy (el->expr);
+ constraintList_free(ltCon);
+ constraintList_free(incCon);
+ return ret;
}
else
}
end_constraintList_elements;
+
+ constraintList_free(ltCon);
+ constraintList_free(incCon);
DPRINTF (( message ("getForTimes: %s %s resorting to ugly hack", exprNode_unparse(forPred), exprNode_unparse(forBody) ) ));
if (! canGetForTimes (forPred, forBody) )
BADEXIT;
}
+/*@access constraintExpr @*/
-static bool isInc (constraintExpr c)
-{
-
- if (c->kind == binaryexpr )
- {
- constraintExprBinaryOpKind binOP;
- constraintExpr t1, t2;
- t1 = constraintExprData_binaryExprGetExpr1 (c->data);
- t2 = constraintExprData_binaryExprGetExpr2 (c->data);
-
- binOP = constraintExprData_binaryExprGetOp (c->data);
- if (binOP == PLUS)
- if (constraintExpr_isLit (t2) && constraintExpr_getValue (t2) == 1 )
- {
- return TRUE;
- }
- }
-
- return FALSE;
-}
-
-constraintExpr constraintExpr_searchAndAdd (constraintExpr c, constraintExpr find, constraintExpr add)
+static /*@only@*/ constraintExpr constraintExpr_searchAndAdd (/*@only@*/ constraintExpr c, /*@observer@*/ constraintExpr find, /*@observer@*/ constraintExpr add)
{
constraintExprKind kind;
constraintExpr temp;
if ( constraintExpr_similar (c, find) )
{
- #warning mem leak
constraintExpr new;
+
+ cstring cPrint;
+
+ cPrint = constraintExpr_unparse(c);
+
+
+ new = constraintExpr_makeAddExpr (c, constraintExpr_copy(add) );
- new = constraintExpr_makeAddConstraintExpr (c, add);
-
- DPRINTF((message ("Replacing %s with %s",
- constraintExpr_unparse(c), constraintExpr_unparse(new)
+ DPRINTF((message ("Replacing %q with %q",
+ cPrint, constraintExpr_unparse(new)
)));
return new;
}
break;
case unaryExpr:
temp = constraintExprData_unaryExprGetExpr (c->data);
- temp = constraintExpr_searchAndAdd (temp, find, add);
+ temp = constraintExpr_searchAndAdd (constraintExpr_copy(temp), find, add);
c->data = constraintExprData_unaryExprSetExpr (c->data, temp);
break;
case binaryexpr:
temp = constraintExprData_binaryExprGetExpr1 (c->data);
- temp = constraintExpr_searchAndAdd (temp, find, add);
+ temp = constraintExpr_searchAndAdd (constraintExpr_copy(temp), find, add);
c->data = constraintExprData_binaryExprSetExpr1 (c->data, temp);
temp = constraintExprData_binaryExprGetExpr2 (c->data);
- temp = constraintExpr_searchAndAdd (temp, find, add);
+ temp = constraintExpr_searchAndAdd (constraintExpr_copy(temp), find, add);
c->data = constraintExprData_binaryExprSetExpr2 (c->data, temp);
break;
default:
}
-constraint constraint_searchAndAdd (constraint c, constraintExpr find, constraintExpr add)
+/*@noaccess constraintExpr @*/
+
+static constraint constraint_searchAndAdd (/*@returned@*/ constraint c, /*@observer@*/ constraintExpr find, /*@observer@*/ constraintExpr add)
{
llassert (constraint_search (c, find) );
}
-constraintList constraintList_searchAndAdd (constraintList list,
- constraintExpr find, constraintExpr add)
+/*@only@*/ static constraintList constraintList_searchAndAdd (/*@returned@*/ constraintList list,
+ /*@observer@*/ constraintExpr find, /*@observer@*/ constraintExpr add)
{
constraintList newConstraints;
constraintList ret;
- newConstraints = constraintList_new();
+ newConstraints = constraintList_makeNew();
constraintList_elements (list, el)
{
new = constraint_copy (el);
new = constraint_searchAndAdd (new, find, add);
+ DPRINTF (( (message ("Adding constraint %s ", constraint_print (new)) ) ));
newConstraints = constraintList_add (newConstraints, new);
- DPRINTF (( (message ("Adding constraint %s ", constraint_print (new)) ) ));
}
}
end_constraintList_elements;
- ret = constraintList_addList (list, newConstraints);
+ ret = constraintList_addListFree (list, newConstraints);
return ret;
}
-void doAdjust(exprNode e, exprNode forPred, exprNode forBody, constraintExpr iterations)
+static void doAdjust(/*@unused@*/ exprNode e, /*@unused@*/ exprNode forPred, /*@observer@*/ exprNode forBody, /*@observer@*/ constraintExpr iterations)
{
constraintList_elements (forBody->ensuresConstraints, el)
{
- // look fro var = var + 1
+ // look for var = var + 1
if (incVar(el) )
{
DPRINTF((message ("Found inc variable constraint : %s", constraint_print (el) ) ));
void forLoopHeuristics( exprNode e, exprNode forPred, exprNode forBody)
{
- exprNode init, test, inc, t1, t2, t3 ,t4;
- constraint con;
+ exprNode init, test, inc;
+
constraintExpr iterations;
init = exprData_getTripleInit (forPred->edata);
iterations = getForTimes (forPred, forBody );
- if (iterations)
+ if (iterations != NULL)
{
doAdjust ( e, forPred, forBody, iterations);
+ constraintExpr_free(iterations);
}
-
}
andersk / splint.git / blobdiff