# include "lclintMacros.nf"
# include "llbasic.h"
-constraintList constraintList_new ()
+
+/*@iter constraintList_elements_private (sef constraintList x, yield constraint el); @*/
+# define constraintList_elements_private(x, m_el) \
+ { int m_ind; constraint *m_elements = &((x)->elements[0]); \
+ for (m_ind = 0 ; m_ind < (x)->nelements; m_ind++) \
+ { constraint m_el = *(m_elements++);
+
+# define end_constraintList_elements_private }}
+
+
+constraintList constraintList_makeNew ()
{
constraintList s = (constraintList) dmalloc (sizeof (*s));
s->elements = newelements;
}
-void constraintList_exprNodemerge()
-{
-}
+
constraintList
-constraintList_add (constraintList s, constraint el)
+constraintList_add (/*@returned@*/ constraintList s, /*@only@*/ constraint el)
{
+ /*drl7x */
+ // el = constraint_simplify (el);
+ if (resolve (el, s) )
+ {
+ constraint_free (el);
+ return s;
+ }
+
if (s->nspace <= 0)
constraintList_grow (s);
return s;
}
-constraintList constraintList_addList (constraintList s, constraintList new)
+/* frees everything but actual constraints */
+/* This function should only be used if you have
+ other references to unshared constraints
+*/
+static void constraintList_freeShallow (/*@only@*/ constraintList c)
+{
+ if (constraintList_isDefined(c) )
+ {
+ free (c->elements);
+ c->elements = NULL;
+ c->nelements = -1;
+ c->nspace = -1;
+ }
+ free (c);
+ c = NULL;
+}
+
+/*@only@*/ constraintList constraintList_addList (/*@returned@*/ constraintList s, /*@observer@*/ constraintList new)
+{
+ llassert(constraintList_isDefined(s) );
+ llassert(constraintList_isDefined(new) );
+
+ if (new == constraintList_undefined)
+ return s;
+
+ constraintList_elements (new, elem)
+ {
+ s = constraintList_add (s, constraint_copy(elem) );
+ }
+ end_constraintList_elements;
+
+ return s;
+}
+
+
+
+/*@only@*/ constraintList constraintList_addListFree (/*@only@*/ constraintList s, /*@only@*/ constraintList new)
{
- constraintList_elements(new, elem)
+ llassert(constraintList_isDefined(s) );
+ llassert(constraintList_isDefined(new) );
+
+ if (new == constraintList_undefined)
+ return s;
+
+ constraintList_elements_private(new, elem)
+ {
s = constraintList_add (s, elem);
- end_constraintList_elements
+ }
+ end_constraintList_elements_private
+
+ constraintList_freeShallow(new);
return s;
}
cstring
-constraintList_print (constraintList s)
+constraintList_print (constraintList s) /*@*/
{
int i;
cstring st = cstring_undefined;
bool first = TRUE;
if (s->nelements == 0)
- st = cstring_makeLiteral("<List Empty>");
-
+ {
+ st = cstring_makeLiteral("<List Empty>");
+ return st;
+ }
+
for (i = 0; i < s->nelements; i++)
{
cstring type = cstring_undefined;
if (current != NULL)
{
- cstring temp1 = constraint_print(current);
+ cstring temp1;
+ if ( context_getFlag (FLG_ORCONSTRAINT) )
+ temp1 = constraint_printOr(current);
+ else
+ temp1 = constraint_print(current);
type = message ("%q %q\n", type, temp1 );
}
{
st = message ("%q, %q", st, type);
}
+ } //end for
+
+ return st;
+}
+
+void constraintList_printErrorPostConditions (constraintList s, fileloc loc)
+{
+
+ constraintList_elements (s, elem)
+ {
+ if (elem != NULL)
+ {
+ constraint_printErrorPostCondition (elem, loc);
+ }
+ }
+ end_constraintList_elements;
+ return;
+}
+
+
+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)
+{
+ int i;
+ cstring st = cstring_undefined;
+ bool first = TRUE;
+
+ if (s->nelements == 0)
+ {
+ st = cstring_makeLiteral("<List Empty>");
+ return st;
+ }
+
+ for (i = 0; i < s->nelements; i++)
+ {
+ cstring type = cstring_undefined;
+ constraint current = s->elements[i];
+
+ if (current != NULL)
+ {
+ cstring temp1 = constraint_printDetailed (current);
+ type = message ("%s %s\n", type, temp1 );
+ cstring_free(temp1);
+ }
+
+ if (first)
+ {
+ st = type;
+ first = FALSE;
+ }
+ else
+ {
+ st = message ("%s %s", st, type);
+ }
}
return st;
}
+/*{ x: constraint | (x in l1 -> resolve (x, l2) || (x in l2 -> resolve (x, l1)
+} */
+
+constraintList
+constraintList_logicalOr (/*@observer@*/ constraintList l1, /*@observer@*/ constraintList l2)
+{
+ constraint temp;
+ constraintList ret;
+ DPRINTF ( (message ("Logical or on %s and %s",
+ constraintList_print(l1),
+ constraintList_print(l2)) ) );
+
+ ret = constraintList_makeNew();
+ constraintList_elements (l1, el)
+ {
+ temp = substitute (el, l2);
+
+ if (resolve (el, l2) || resolve(temp,l2) )
+ { /*avoid redundant constraints*/
+ if (!resolve (el, ret) )
+ {
+ constraint temp2;
+ temp2 = constraint_copy(el);
+ ret = constraintList_add (ret, temp2);
+ }
+ }
+ constraint_free(temp);
+ }
+ 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) )
+ {
+ constraint temp2;
+ temp2 = constraint_copy(el);
+ ret = constraintList_add (ret, temp2);
+ }
+ }
+ constraint_free(temp);
+ }
+ end_constraintList_elements;
+
+
+ return ret;
+}
+
void
-constraintList_free (constraintList s)
+constraintList_free (/*@only@*/ constraintList s)
{
int i;
+
+ llassert(constraintList_isDefined(s) );
+
+
for (i = 0; i < s->nelements; i++)
{
- // constraint_free (s->elements[i]);
+ constraint_free (s->elements[i]);
}
sfree (s->elements);
+ s->elements = NULL;
+ s->nelements = -1;
+ s->nspace = -1;
sfree (s);
+ s = NULL;
}
constraintList
constraintList_copy (constraintList s)
{
- constraintList ret = constraintList_new ();
+ constraintList ret = constraintList_makeNew ();
constraintList_elements (s, el)
{
return ret;
}
+constraintList constraintList_preserveOrig (constraintList c)
+{
+ DPRINTF((message("constraintList_preserveOrig preserving the originial constraints for %s ", constraintList_print (c) ) ));
+
+ constraintList_elements_private (c, el)
+ {
+ el = constraint_preserveOrig (el);
+ }
+ end_constraintList_elements_private;
+ return c;
+}
+
+constraintList constraintList_preserveCallInfo (/*@returned@*/ constraintList c, exprNode fcn)
+{
+ DPRINTF((message("constraintList_preserveOrig preserving the originial constraints for %s ", constraintList_print (c) ) ));
+
+ constraintList_elements_private (c, el)
+ {
+ // el = constraint_preserveOrig (el);
+ el = constraint_setFcnPre(el);
+ el = constraint_origAddGeneratingExpr (el, fcn);
+ }
+ end_constraintList_elements_private;
+ return c;
+}
+
+
+
+constraintList constraintList_addGeneratingExpr (constraintList c, exprNode e)
+{
+ DPRINTF ((message ("entering constraintList_addGeneratingExpr for %s ", exprNode_unparse(e) ) ));
+
+ constraintList_elements_private (c, el)
+ {
+ DPRINTF ((message ("setting generatingExpr for %s to %s", constraint_print(el), exprNode_unparse(e) ) ));
+ el = constraint_addGeneratingExpr (el, e);
+ }
+ end_constraintList_elements_private;
+ return c;
+}
+
+/*@only@*/ constraintList constraintList_doFixResult (/*@only@*/constraintList postconditions, exprNode fcnCall)
+{
+ constraintList ret;
+ ret = constraintList_makeNew();
+ constraintList_elements_private (postconditions, el)
+ {
+ ret = constraintList_add (ret, constraint_doFixResult (el, fcnCall) );
+ }
+ end_constraintList_elements_private;
+
+ constraintList_free(postconditions);
+ return ret;
+}
+
+/*@only@*/ constraintList constraintList_doSRefFixConstraintParam (constraintList preconditions, exprNodeList arglist)
+{
+ constraintList ret;
+ ret = constraintList_makeNew();
+
+ constraintList_elements (preconditions, el)
+ {
+ ret = constraintList_add(ret, constraint_doSRefFixConstraintParam (el, arglist) );
+ }
+ end_constraintList_elements;
+
+ constraintList_free (preconditions);
+
+ return ret;
+}
+constraintList constraintList_doSRefFixBaseParam (/*@observer@*/ constraintList preconditions, /*@observer@*/
+ exprNodeList arglist)
+{
+ constraintList ret;
+ constraint temp;
+ ret = constraintList_makeNew();
+
+ constraintList_elements (preconditions, el)
+ {
+ temp = constraint_copy(el);
+ ret = constraintList_add(ret, constraint_doSRefFixBaseParam (temp, arglist) );
+ }
+ end_constraintList_elements;
+
+ return ret;
+}
+
+constraintList constraintList_togglePost (/*@returned@*/ constraintList c)
+{
+ constraintList_elements_private (c, el)
+ {
+ el = constraint_togglePost(el);
+ if (el->orig)
+ {
+ el->orig = constraint_togglePost(el->orig);
+ }
+ }
+ end_constraintList_elements_private;
+ return c;
+}
+
andersk / splint.git / blobdiff