Removed some .out files.

[splint.git] / src / constraintList.c

diff --git a/src/constraintList.c b/src/constraintList.c
index 427638acc527112bdd00b8679c0372571534cbde..26dbaa3bc977fda29bf85a76f9b18ded3cc7a02b 100644 (file)
--- a/src/constraintList.c
+++ b/src/constraintList.c
@@ -63,12 +63,15 @@ constraintList_grow (constraintList s)
   s->elements = newelements;
 }
 
-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);
 
@@ -78,41 +81,145 @@ constraintList_add (constraintList s, constraint el)
   return s;
 }
 
-/*  cstring */
-/*  constraintList_unparse (constraintList s) */
-/*  { */
-/*    int i; */
-/*    cstring st = cstring_undefined; */
-/*    bool first = TRUE; */
-
-/*    for (i = 0; i < s->nelements; i++) */
-/*      { */
-/*        cstring type = cstring_undefined; */
-/*        constraint current = s->elements[i]; */
-
-/*        if (current->isObj) */
-/*     { */
-/*       type = cstring_makeLiteral ("obj "); */
-/*     } */
-
-/*        if (current->type != NULL) */
-/*     { */
-/*       type = message (": %q%q", type, lclTypeSpecNode_unparse (current->type)); */
-/*     } */
-
-/*        if (first) */
-/*     { */
-/*       st = type; */
-/*       first = FALSE; */
-/*     } */
-/*        else */
-/*     { */
-/*       st = message ("%q, %q", st, type); */
-/*     } */
-/*      } */
-
-/*    return st; */
-/*  } */
+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) /*@*/
+{
+  int i;
+  cstring st = cstring_undefined;
+  bool first = TRUE;
+
+  if (s->nelements == 0)
+    st = cstring_makeLiteral("<List Empty>");
+  
+  for (i = 0; i < s->nelements; i++)
+    {
+      cstring type = cstring_undefined;
+      constraint current = s->elements[i];
+
+      if (current != NULL)
+       {
+         cstring temp1 = constraint_print(current);
+         type = message ("%q %q\n", type, temp1 );
+       }
+
+      if (first)
+       {
+         st = type;
+         first = FALSE;
+       }
+      else
+       {
+         st = message ("%q, %q", st, type);
+       }
+    }
+  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)
+{
+  int i;
+  cstring st = cstring_undefined;
+  bool first = TRUE;
+
+  if (s->nelements == 0)
+    st = cstring_makeLiteral("<List Empty>");
+  
+  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 );
+       }
+
+      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 (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)
@@ -139,3 +246,79 @@ constraintList_copy (constraintList s)
 
   return ret;
 }
+
+constraintList constraintList_preserveOrig (constraintList c)
+{
+  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;
+}
+
+