Fixed library dump support so that buffer constraint annotations are read and written...

[splint.git] / src / constraintResolve.c

diff --git a/src/constraintResolve.c b/src/constraintResolve.c
index c6ba1503368f2397e0997d7e9f251b033667dea3..4e8f172dcc5530df1d2e2d0beaaad2e023311862 100644 (file)
--- a/src/constraintResolve.c
+++ b/src/constraintResolve.c
@@ -14,7 +14,6 @@
 # include "exprChecks.h"
 # include "aliasChecks.h"
 # include "exprNodeSList.h"
-//# include "exprData.i"
 
 
 /*@access constraint, exprNode @*/
@@ -70,7 +69,8 @@ static /*@only@*/ constraintList reflectChangesEnsuresFree1 (/*@only@*/ constrai
   temp = constraintList_subsumeEnsures (list2, ret);
 
   temp = constraintList_addList (temp, ret);
-
+  constraintList_free(ret);
+  
   DPRINTF(( message ("constraintList_mergeEnsures: returning %s ",
                     constraintList_print(temp) )
                     ));
@@ -109,7 +109,7 @@ static /*@only@*/ constraintList reflectChangesEnsuresFree1 (/*@only@*/ constrai
  
   DPRINTF((message ("constraintList_mergeRequires: ret =  %s", constraintList_print(ret) ) ) );
   
-  ret = constraintList_addList (ret, temp);
+  ret = constraintList_addListFree (ret, temp);
   
   DPRINTF((message ("constraintList_mergeRequires: returning  %s", constraintList_print(ret) ) ) );
 
@@ -157,7 +157,8 @@ constraintList checkCall (exprNode fcn, exprNodeList arglist)
 
   if (preconditions != constraintList_undefined)
     {
-      preconditions= constraintList_togglePost (preconditions);   
+      preconditions = constraintList_togglePost (preconditions);
+      preconditions = constraintList_preserveCallInfo(preconditions, fcn);
       preconditions = constraintList_doSRefFixConstraintParam (preconditions, arglist);
     }
   else
@@ -165,7 +166,8 @@ constraintList checkCall (exprNode fcn, exprNodeList arglist)
       if (preconditions == NULL)
        preconditions = constraintList_makeNew();
     }
-  
+  DPRINTF (( message("Done checkCall\n") ));
+  DPRINTF (( message("Returning list %q ", constraintList_printDetailed(preconditions) ) ));
   return preconditions;
 }
 
@@ -334,13 +336,19 @@ void mergeResolve (exprNode parent, exprNode child1, exprNode child2)
              //so we don't want to store the result but we do it anyway
              temp2 = constraint_copy (temp);
              //                  if (context_getFlag (FLG_ORCONSTRAINT) )
-                temp2 = inequalitySubstitute (temp2, post1); 
-                     if (!resolve (temp2, post1) )
-                       {
-                         temp2 = inequalitySubstituteUnsound (temp2, post1); 
-                         if (!resolve (temp2, post1) )
-                             ret = constraintList_add (ret, temp2);
-                       }
+             temp2 = inequalitySubstitute (temp2, post1); 
+             if (!resolve (temp2, post1) )
+               {
+                 temp2 = inequalitySubstituteUnsound (temp2, post1); 
+                 if (!resolve (temp2, post1) )
+                   ret = constraintList_add (ret, temp2);
+                 else
+                   constraint_free(temp2);
+               }
+             else
+               {
+                 constraint_free(temp2);
+               }
            }
          constraint_free(temp);
        }
@@ -454,9 +462,13 @@ static /*@only@*/ constraint doResolveOr (constraint c, constraintList post1, /*
 
   if (*resolved)
     {
-      constraint_free(next);
-      constraint_free(ret);
-      return NULL;
+      if (next != NULL)
+       constraint_free(next);
+
+      /*we don't need to free ret when resolved is false because ret is null*/
+      llassert(ret == NULL);
+      
+       return NULL;
     }
 
   while (next != NULL)
@@ -468,14 +480,19 @@ static /*@only@*/ constraint doResolveOr (constraint c, constraintList post1, /*
       curr = doResolve (curr, post1, resolved);
       if (*resolved)
        {
-         constraint_free(curr);
-         constraint_free(next);
+         /* curr is null so we don't try to free it*/
+         llassert(curr == NULL);
+         
+         if (next != NULL)
+           constraint_free(next);
+
          constraint_free(ret);
          return NULL;
        }
       ret = constraint_addOr (ret, curr);
+      constraint_free(curr);
     }
-  constraint_free(curr);
+
   return ret;
 }
 
@@ -500,6 +517,12 @@ static /*@only@*/ constraint doResolveOr (constraint c, constraintList post1, /*
        {
          ret = constraintList_add(ret, temp);
        }
+      else
+       {
+     /*we don't need to free ret when resolved is false because ret is null*/
+         llassert(temp == NULL);
+       }
+      
     } end_constraintList_elements;
 
     DPRINTF((message ("reflectChangesOr: returning %s", constraintList_print(ret) ) ) );
@@ -519,6 +542,8 @@ static /*@only@*/ constraintList reflectChangesEnsures (/*@observer@*/ constrain
 
          if (!resolve (temp, post1) )
            ret = constraintList_add (ret, temp);
+         else
+           constraint_free(temp);  
        }
       else
        {
@@ -1078,7 +1103,6 @@ return ret;
   constraintList_elements(target, el)
   { 
     constraint temp;
-    #warning make sure this side effect is the right things
     #warning make sure that a side effect is not expected
 
     temp = substitute(el, subList);
@@ -1089,7 +1113,7 @@ return ret;
   return ret;
 }
 
-constraint constraint_solve (constraint c)
+constraint constraint_solve (/*@returned@*/ constraint c)
 {
   DPRINTF( (message ("Solving %s\n", constraint_print(c) ) ) );
   c->expr = constraintExpr_solveBinaryExpr (c->lexpr, c->expr);