s->elements = newelements;
}
-void constraintList_exprNodemerge()
-{
-}
+/* void constraintList_exprNodemerge(void) */
+/* { */
+/* } */
constraintList
constraintList_add (constraintList s, constraint el)
{
+ if (resolve (el, s) )
+ return s;
+
if (s->nspace <= 0)
constraintList_grow (s);
constraintList constraintList_addList (constraintList s, constraintList new)
{
+ llassert(s);
+ llassert(new);
+
+ if (new == constraintList_undefined)
+ return s;
+
constraintList_elements(new, elem)
+ {
s = constraintList_add (s, elem);
+ }
end_constraintList_elements
return s;
}
cstring
-constraintList_print (constraintList s)
+constraintList_print (constraintList s) /*@*/
{
int i;
cstring st = cstring_undefined;
return st;
}
+void constraintList_printError (constraintList s, fileloc loc)
+{
+
+ constraintList_elements (s, elem)
+ {
+ if (elem != NULL)
+ {
+ constraint_printError (elem, loc);
+ }
+ }
+ end_constraintList_elements;
+ return;
+}
cstring
constraintList_printDetailed (constraintList s)
return st;
}
+/*{ x: constraint | (x in l1 -> resolve (x, l2) || (x in l2 -> resolve (x, l1)
+} */
+
+constraintList
+constraintList_logicalOr (constraintList l1, constraintList l2)
+{
+ constraint temp;
+ constraintList ret;
+ DPRINTF ( (message ("Logical of on %s and %s",
+ constraintList_print(l1),
+ constraintList_print(l2)) ) );
+
+ ret = constraintList_new();
+ constraintList_elements (l1, el)
+ {
+ temp = substitute (el, l2);
+
+ if (resolve (el, l2) || resolve(temp,l2) )
+ { /*avoid redundant constraints*/
+ if (!resolve (el, ret) )
+ ret = constraintList_add (ret, el);
+ }
+ }
+ end_constraintList_elements;
+
+ constraintList_elements (l2, el)
+ {
+ temp = substitute (el, l1);
+
+ if (resolve (el, l1) || resolve(temp,l1) )
+ {
+ /*avoid redundant constraints*/
+ if (!resolve (el, ret) )
+ ret = constraintList_add (ret, el);
+ }
+ }
+ end_constraintList_elements;
+
+
+ return ret;
+}
+
void
constraintList_free (constraintList s)
{
constraintList constraintList_preserveOrig (constraintList c)
{
- constraintList_elements (c, el);
+ constraintList_elements (c, el)
{
el = constraint_preserveOrig (el);
}
end_constraintList_elements;
return c;
}
+
+constraintList constraintList_addGeneratingExpr (constraintList c, exprNode e)
+{
+ DPRINTF ((message ("entering constraintList_addGeneratingExpr for %s ", exprNode_unparse(e) ) ));
+
+ constraintList_elements (c, el)
+ {
+ DPRINTF ((message ("setting generatingExpr for %s to %s", constraint_print(el), exprNode_unparse(e) ) ));
+ el = constraint_addGeneratingExpr (el, e);
+ }
+ end_constraintList_elements;
+ return c;
+}
+
+constraintList constraintList_doFixResult (constraintList postconditions, exprNode fcnCall)
+{
+ constraintList ret;
+ ret = constraintList_new();
+ constraintList_elements (postconditions, el)
+ {
+ ret = constraintList_add (ret, constraint_doFixResult (el, fcnCall) );
+ }
+ end_constraintList_elements;
+
+ return ret;
+}
+
+constraintList constraintList_doSRefFixConstraintParam (constraintList preconditions, exprNodeList arglist)
+{
+ constraintList ret;
+ ret = constraintList_new();
+
+ constraintList_elements (preconditions, el)
+ {
+ ret = constraintList_add(ret, constraint_doSRefFixConstraintParam (el, arglist) );
+ }
+ end_constraintList_elements;
+
+ return ret;
+}
+constraintList constraintList_doSRefFixBaseParam (constraintList preconditions,
+ exprNodeList arglist)
+{
+ constraintList ret;
+ ret = constraintList_new();
+
+ constraintList_elements (preconditions, el)
+ {
+ ret = constraintList_add(ret, constraint_doSRefFixBaseParam (el, arglist) );
+ }
+ end_constraintList_elements;
+
+ return ret;
+}
+
+constraintList constraintList_togglePost (/*@returned@*/ constraintList c)
+{
+ constraintList_elements (c, el)
+ {
+ el->post = !el->post;
+ }
+ end_constraintList_elements;
+ return c;
+}
+
+