Added check of user specified post conditions.

[splint.git] / src / constraintList.c

diff --git a/src/constraintList.c b/src/constraintList.c
index bb3c588da0cb5a533760abc42e55700185350b2a..1ce9f550a908ade2265fe9097b02c240e35ecb89 100644 (file)
--- a/src/constraintList.c
+++ b/src/constraintList.c
@@ -75,7 +75,7 @@ constraintList_grow (constraintList s)
 
 
 constraintList 
-constraintList_add (constraintList s, constraint el)
+constraintList_add (/*@returned@*/ constraintList s, /*@only@*/ constraint el)
 {
   /*drl7x */
   //   el = constraint_simplify (el);
@@ -101,12 +101,36 @@ constraintList_add (constraintList s, constraint el)
 static void constraintList_freeShallow (/*@only@*/ constraintList c)
 {
   if (constraintList_isDefined(c) )
-    free (c->elements);
-  
+    {
+      free (c->elements);
+      c->elements = NULL;
+      c->nelements = -1;
+      c->nspace = -1;
+    }
   free (c);
+  c = NULL;
 }
 
-constraintList constraintList_addList (/*@returned@*/ constraintList s, /*@only@*/ constraintList new)
+/*@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)
 {
   llassert(constraintList_isDefined(s) );
   llassert(constraintList_isDefined(new) );
@@ -166,20 +190,36 @@ constraintList_print (constraintList s) /*@*/
   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_private (s, elem)
+  constraintList_elements (s, elem)
     {
       if (elem != NULL)
        {
          constraint_printError (elem, loc);
        }
     }
-  end_constraintList_elements_private;
+  end_constraintList_elements;
   return;
 }
 
+
 cstring
 constraintList_printDetailed (constraintList s)
 {
@@ -222,29 +262,33 @@ constraintList_printDetailed (constraintList s)
 } */
 
 constraintList
-constraintList_logicalOr (constraintList l1, constraintList l2)
+constraintList_logicalOr (/*@observer@*/ constraintList l1, /*@observer@*/ constraintList l2)
 {
   constraint temp;
   constraintList ret;
-  DPRINTF ( (message ("Logical of on %s and %s",
+  DPRINTF ( (message ("Logical or on %s and %s",
                      constraintList_print(l1), 
                      constraintList_print(l2)) ) );
   
   ret = constraintList_makeNew();
-  constraintList_elements_private (l1, el)
+  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);
+           {
+             constraint temp2;
+             temp2 = constraint_copy(el);
+             ret = constraintList_add (ret, temp2);
+           }
        }
       constraint_free(temp);
     }
-  end_constraintList_elements_private;
+  end_constraintList_elements;
 
-   constraintList_elements_private (l2, el)
+   constraintList_elements (l2, el)
     {
       temp = substitute (el, l1);
       
@@ -252,27 +296,39 @@ constraintList_logicalOr (constraintList l1, constraintList l2)
        {
          /*avoid redundant constraints*/
          if (!resolve (el, ret) )
-           ret = constraintList_add (ret, el);
+           {
+             constraint temp2;
+             temp2 = constraint_copy(el);
+             ret = constraintList_add (ret, temp2);
+           }
        }
       constraint_free(temp);
     }
-  end_constraintList_elements_private;
+  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
@@ -280,10 +336,10 @@ constraintList_copy (constraintList s)
 {
   constraintList ret = constraintList_makeNew ();
 
-  constraintList_elements_private (s, el)
+  constraintList_elements (s, el)
     {
       ret = constraintList_add (ret, constraint_copy (el));
-    } end_constraintList_elements_private;
+    } end_constraintList_elements;
 
   return ret;
 }
@@ -300,6 +356,22 @@ constraintList constraintList_preserveOrig (constraintList c)
   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) ) ));
@@ -327,32 +399,34 @@ constraintList constraintList_addGeneratingExpr (constraintList c, exprNode e)
   return ret;
 }
 
-constraintList constraintList_doSRefFixConstraintParam (constraintList preconditions, exprNodeList arglist)
+/*@only@*/ constraintList constraintList_doSRefFixConstraintParam (constraintList preconditions, exprNodeList arglist)
 {
   constraintList ret;
   ret = constraintList_makeNew();
 
-  constraintList_elements_private (preconditions, el)
+  constraintList_elements (preconditions, el)
     {
       ret = constraintList_add(ret, constraint_doSRefFixConstraintParam (el, arglist) );
     }
-  end_constraintList_elements_private;
+  end_constraintList_elements;
 
   constraintList_free (preconditions);
 
   return ret;
 }
-constraintList constraintList_doSRefFixBaseParam (constraintList preconditions,
+constraintList constraintList_doSRefFixBaseParam (/*@observer@*/ constraintList preconditions, /*@observer@*/
                                                   exprNodeList arglist)
 {
   constraintList ret;
+  constraint temp;
   ret = constraintList_makeNew();
 
-  constraintList_elements_private (preconditions, el)
+  constraintList_elements (preconditions, el)
     {
-      ret = constraintList_add(ret, constraint_doSRefFixBaseParam (el, arglist) );
+      temp = constraint_copy(el);
+      ret = constraintList_add(ret, constraint_doSRefFixBaseParam (temp, arglist) );
     }
-  end_constraintList_elements_private;
+  end_constraintList_elements;
 
   return ret;
 }
@@ -362,6 +436,10 @@ 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;