# include "aliasChecks.h"
# include "exprNodeSList.h"
-# include "exprData.i"
# include "exprDataQuite.i"
/*@access constraint, exprNode @*/
/*@access constraintExpr @*/
-static bool isInc (constraintExpr c) /*@*/
+static bool isInc (/*@observer@*/ constraintExpr c) /*@*/
{
llassert(constraintExpr_isDefined(c) );
/*@noaccess constraintExpr @*/
-static bool increments (constraint c,
- constraintExpr var)
+static bool increments (/*@observer@*/ constraint c,
+ /*@observer@*/ constraintExpr var)
{
llassert(constraint_isDefined(c) );
return FALSE;
}
-static constraintList getLessThanConstraints (constraintList c)
+static /*@only@*/ constraintList getLessThanConstraints (/*@observer@*/ constraintList c)
{
constraintList ret;
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;
{
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 (/*@notnull@*/ exprNode forPred, /*@notnull@*/ 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;
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) )
/*@access constraintExpr @*/
-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:
/*@noaccess constraintExpr @*/
-constraint constraint_searchAndAdd (constraint c, constraintExpr find, constraintExpr add)
+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;
}
end_constraintList_elements;
- ret = constraintList_addList (list, newConstraints);
+ ret = constraintList_addListFree (list, newConstraints);
return ret;
}
-static void doAdjust(/*@unused@*/ exprNode e, /*@unused@*/ 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)
iterations = getForTimes (forPred, forBody );
- if (iterations)
+ if (iterations != NULL)
{
doAdjust ( e, forPred, forBody, iterations);
+ constraintExpr_free(iterations);
}
-
}