X-Git-Url: http://andersk.mit.edu/gitweb/splint.git/blobdiff_plain/2934b455c4074408a0f819009c071456f021ba21..4109ede4aeaeba5a1f9294d544b4229d7602064f:/src/constraintList.c

diff --git a/src/constraintList.c b/src/constraintList.c
index f959c3a..65c243d 100644
--- a/src/constraintList.c
+++ b/src/constraintList.c
@@ -33,16 +33,25 @@
 # include "llbasic.h"
 
 
-/*@iter constraintList_elements_private (sef constraintList x, yield constraint el); @*/
+/*@iter constraintList_elements_private_only (sef constraintList x, yield only constraint el); @*/
+# define constraintList_elements_private_only(x, m_el) \
+   { if (constraintList_isDefined (x)) { 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_only }}}
+
+
+/*@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]); \
+   { if (constraintList_isDefined (x)) { 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 }}
+# define end_constraintList_elements_private }}}
 
 
-constraintList constraintList_makeNew ()
+/*@only@*/ constraintList constraintList_makeNew ()
 {
   constraintList s = (constraintList) dmalloc (sizeof (*s));
 
@@ -60,6 +69,8 @@ constraintList_grow (constraintList s)
   int i;
   constraint *newelements; 
 
+  llassert (constraintList_isDefined (s));
+
   s->nspace += constraintListBASESIZE;
   newelements = (constraint *) dmalloc (sizeof (*newelements)
 				     * (s->nelements + s->nspace));
@@ -77,9 +88,11 @@ constraintList_grow (constraintList s)
 constraintList 
 constraintList_add (/*@returned@*/ constraintList s, /*@only@*/ constraint el)
 {
+  llassert (constraintList_isDefined (s));
+
   /*drl7x */
   //   el = constraint_simplify (el);
-  if (resolve (el, s) )
+  if (constraintList_resolve (el, s) )
     {
       constraint_free (el);
       return s;
@@ -111,15 +124,15 @@ static void constraintList_freeShallow (/*@only@*/ constraintList c)
   c = NULL;
 }
 
-/*@only@*/ constraintList constraintList_addList (/*@returned@*/ constraintList s, /*@observer@*/ constraintList new)
+/*@only@*/ constraintList constraintList_addList (/*@only@*/ /*@returned@*/ constraintList s, /*@observer@*/ constraintList newList)
 {
   llassert(constraintList_isDefined(s) );
-  llassert(constraintList_isDefined(new) );
+  llassert(constraintList_isDefined(newList) );
 
-  if (new == constraintList_undefined)
+  if (newList == constraintList_undefined)
     return s;
   
-  constraintList_elements (new, elem)
+  constraintList_elements (newList, elem)
     {
     s = constraintList_add (s, constraint_copy(elem) );
     }
@@ -128,30 +141,42 @@ static void constraintList_freeShallow (/*@only@*/ constraintList c)
   return s;
 }
 
-/*@only@*/ constraintList constraintList_addListFree (/*@only@*/ constraintList s, /*@only@*/ constraintList new)
+constraintList constraintList_addListFree (/*@returned@*/ constraintList s, /*@only@*/ constraintList newList)
 {
   llassert(constraintList_isDefined(s) );
-  llassert(constraintList_isDefined(new) );
+  llassert(constraintList_isDefined(newList) );
 
-  if (new == constraintList_undefined)
+  if (constraintList_isUndefined(newList) )
     return s;
   
-  constraintList_elements_private(new, elem)
+  constraintList_elements_private_only(newList, elem)
     {
     s = constraintList_add (s, elem);
     }
-  end_constraintList_elements_private
+  end_constraintList_elements_private_only
 
-    constraintList_freeShallow(new);
+    constraintList_freeShallow(newList);
     return s;
 }
 
-cstring
-constraintList_print (constraintList s) /*@*/
+
+extern /*@only@*/ cstring constraintList_unparse ( /*@observer@*/ constraintList s) /*@*/
+{
+  return (constraintList_print(s));
+}
+
+
+/*@only@*/ cstring
+constraintList_print (/*@temp@*/ constraintList s) /*@*/
 {
   int i;
   cstring st = cstring_undefined;
   bool first = TRUE;
+  
+  if (!constraintList_isDefined (s))
+    {
+      return cstring_makeLiteral ("<undefined>");
+    }
 
   if (s->nelements == 0)
     {
@@ -164,7 +189,7 @@ constraintList_print (constraintList s) /*@*/
       cstring type = cstring_undefined;
       constraint current = s->elements[i];
 
-      if (current != NULL)
+      if (constraint_isDefined(current) )
 	{
 	  cstring temp1;
 	    if ( context_getFlag (FLG_ORCONSTRAINT) )
@@ -193,7 +218,7 @@ void constraintList_printErrorPostConditions (constraintList s, fileloc loc)
 
   constraintList_elements (s, elem)
     {
-      if (elem != NULL)
+      if (constraint_isDefined(elem))
 	{
 	  constraint_printErrorPostCondition (elem, loc);
 	}
@@ -207,9 +232,12 @@ void constraintList_printError (constraintList s, fileloc loc)
 
   constraintList_elements (s, elem)
     {
-      if (elem != NULL)
+      if (constraint_isDefined(elem) )
 	{
-	  constraint_printError (elem, loc);
+	  if (constraint_isPost(elem) )
+	    constraint_printErrorPostCondition (elem, loc);
+	  else
+	    constraint_printError (elem, loc);
 	}
     }
   end_constraintList_elements;
@@ -224,6 +252,11 @@ constraintList_printDetailed (constraintList s)
   cstring st = cstring_undefined;
   bool first = TRUE;
 
+  if (!constraintList_isDefined (s))
+    {
+      return cstring_makeLiteral ("<undefined>");
+    }
+
   if (s->nelements == 0)
     {
       st = cstring_makeLiteral("<List Empty>");
@@ -235,7 +268,7 @@ constraintList_printDetailed (constraintList s)
       cstring type = cstring_undefined;
       constraint current = s->elements[i];
 
-      if (current != NULL)
+      if (constraint_isDefined(current ) )
 	{
 	  cstring temp1 = constraint_printDetailed (current);
 	  type = message ("%s %s\n", type, temp1 );
@@ -246,10 +279,11 @@ constraintList_printDetailed (constraintList s)
 	{
 	  st = type;
 	  first = FALSE;
+	  type = NULL;
 	}
       else
 	{
-	  st = message ("%s %s", st, type);
+	  st = message ("%q %q", st, type);
 	}
     }
   return st;
@@ -270,11 +304,11 @@ constraintList_logicalOr (/*@observer@*/ constraintList l1, /*@observer@*/ const
   ret = constraintList_makeNew();
   constraintList_elements (l1, el)
     {
-      temp = substitute (el, l2);
+      temp = constraint_substitute (el, l2);
       
-      if (resolve (el, l2) || resolve(temp,l2) )
+      if (constraintList_resolve (el, l2) || constraintList_resolve(temp,l2) )
 	{   /*avoid redundant constraints*/
-	  if (!resolve (el, ret) )
+	  if (!constraintList_resolve (el, ret) )
 	    {
 	      constraint temp2;
 	      temp2 = constraint_copy(el);
@@ -287,12 +321,12 @@ constraintList_logicalOr (/*@observer@*/ constraintList l1, /*@observer@*/ const
 
    constraintList_elements (l2, el)
     {
-      temp = substitute (el, l1);
+      temp = constraint_substitute (el, l1);
       
-      if (resolve (el, l1) || resolve(temp,l1) )
+      if (constraintList_resolve (el, l1) || constraintList_resolve(temp,l1) )
 	{
 	  /*avoid redundant constraints*/
-	  if (!resolve (el, ret) )
+	  if (!constraintList_resolve (el, ret) )
 	    {
 	      constraint temp2;
 	      temp2 = constraint_copy(el);
@@ -329,7 +363,7 @@ constraintList_free (/*@only@*/ constraintList s)
 }
 
 constraintList
-constraintList_copy (constraintList s)
+constraintList_copy (/*@observer@*/ /*@temp@*/ constraintList s)
 {
   constraintList ret = constraintList_makeNew ();
 
@@ -353,9 +387,9 @@ constraintList constraintList_preserveOrig (constraintList c)
   return c;
 }
 
-constraintList constraintList_preserveCallInfo (/*@returned@*/ constraintList c, exprNode fcn)
+constraintList constraintList_preserveCallInfo (/*@returned@*/ constraintList c,/*@observer@*/ /*@dependent@*/ /*@observer@*/  exprNode fcn)
 {
-  DPRINTF((message("constraintList_preserveOrig preserving the originial constraints for %s ", constraintList_print (c) ) ));
+  DPRINTF((message("constraintList_preserveCallInfo %s ", constraintList_print (c) ) ));
 
   constraintList_elements_private (c, el)
   {
@@ -367,9 +401,15 @@ constraintList constraintList_preserveCallInfo (/*@returned@*/ constraintList c,
   return c;
 }
 
+constraintList constraintList_single (constraint c)
+{
+  constraintList res;
+  res = constraintList_makeNew();
+  res = constraintList_add (res, c);
+  return res;
+}
 
-
-constraintList constraintList_addGeneratingExpr (constraintList c, exprNode e)
+constraintList constraintList_addGeneratingExpr (constraintList c,/*@dependent@*/ exprNode e)
 {
   DPRINTF ((message ("entering constraintList_addGeneratingExpr for %s ", exprNode_unparse(e) ) ));
   
@@ -396,7 +436,7 @@ constraintList constraintList_addGeneratingExpr (constraintList c, exprNode e)
   return ret;
 }
 
-/*@only@*/ constraintList constraintList_doSRefFixConstraintParam (constraintList preconditions, exprNodeList arglist)
+/*@only@*/ constraintList constraintList_doSRefFixConstraintParam (constraintList preconditions, /*@temp@*/ /*@observer@*/ exprNodeList arglist)
 {
   constraintList ret;
   ret = constraintList_makeNew();
@@ -411,7 +451,7 @@ constraintList constraintList_addGeneratingExpr (constraintList c, exprNode e)
 
   return ret;
 }
-constraintList constraintList_doSRefFixBaseParam (/*@observer@*/ constraintList preconditions, /*@observer@*/
+constraintList constraintList_doSRefFixBaseParam (constraintList preconditions, /*@observer@*/
 						   exprNodeList arglist)
 {
   constraintList ret;
@@ -442,4 +482,54 @@ constraintList constraintList_togglePost (/*@returned@*/ constraintList c)
   return c;
 }
 
+/*@only@*/ constraintList constraintList_undump (FILE *f)
+{
+  constraintList ret;
+  char *s = mstring_create (MAX_DUMP_LINE_LENGTH);
+  char *os;
+  
+  ret = constraintList_makeNew();
+
+  os = s;
+  s = fgets (os, MAX_DUMP_LINE_LENGTH, f);
+
+  while (s != NULL && *s != ';')
+    {
+      constraint temp;
+      char * c;
+
+      c =  reader_getWord(&s);
+      
+      if (strcmp (c, "C") != 0)
+	{
+	  llfatalbug(message("Error reading library.  File may be corrupted"));
+	}
+
+      temp = constraint_undump (f);
+      ret = constraintList_add (ret, temp);
+      s = fgets (os, MAX_DUMP_LINE_LENGTH, f);
+      free(c);
+    }
+  free(s);
+
+  return ret;
+}
+
+
+void constraintList_dump (/*@observer@*/ constraintList c,  FILE *f)
+{
+  constraintList_elements (c, el)
+    {
+      fprintf(f, "C\n");
+      constraint_dump (el, f);
+    }
+  end_constraintList_elements; ;
+}
+
 
+constraintList constraintList_sort (/*@returned@*/ constraintList ret)
+{
+  qsort (ret->elements, (size_t) ret->nelements,
+	 (sizeof (*ret->elements) ), constraint_compare);
+  return ret;
+}