+ end_constraintList_elements_private;
+ return c;
+}
+
+constraintList constraintList_preserveCallInfo (/*@returned@*/ constraintList c,/*@observer@*/ /*@dependent@*/ /*@observer@*/ exprNode fcn)
+{
+ DPRINTF((message("constraintList_preserveCallInfo %s ", constraintList_print (c) ) ));
+
+ constraintList_elements_private (c, el)
+ {
+ el = constraint_setFcnPre(el);
+ el = constraint_origAddGeneratingExpr (el, fcn);
+ }
+ end_constraintList_elements_private;
+ return c;
+}
+
+constraintList constraintList_single (constraint c)
+{
+ constraintList res;
+ res = constraintList_makeNew();
+ res = constraintList_add (res, c);
+ return res;
+}
+
+constraintList constraintList_addGeneratingExpr (constraintList c,/*@dependent@*/ 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;
+}
+/*
+Commenting out because function is not yet stable
+
+/ *@only@* / constraintList constraintList_doSRefFixStructConstraint(constraintList invars, sRef s, ctype ct )
+{
+ constraintList ret;
+ ret = constraintList_makeNew();
+
+ constraintList_elements (invars, el)
+ {
+ ret = constraintList_add(ret, constraint_doSRefFixInvarConstraint (el, s, ct) );
+ }
+ end_constraintList_elements;
+
+ / * constraintList_free (invars);* /
+
+ return ret;
+}
+*/
+
+/*@only@*/ constraintList constraintList_doSRefFixConstraintParam (constraintList preconditions, /*@temp@*/ /*@observer@*/ 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 (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) );
+ }