]> andersk Git - splint.git/blobdiff - src/constraintResolve.c
Merged with Dave Evans's changes.
[splint.git] / src / constraintResolve.c
index 033ed585e49a68f6d0f4fbc65fb7f23017ef69da..de80027b29636402b2608f04549b011ff98af443 100644 (file)
 # include "exprChecks.h"
 # include "aliasChecks.h"
 # include "exprNodeSList.h"
-//# include "exprData.i"
 
 
 /*@access constraint, exprNode @*/
 
+static bool rangeCheck (arithType ar1, /*@observer@*/ constraintExpr expr1, arithType ar2, /*@observer@*/ constraintExpr expr2);
 
-constraint  inequalitySubstituteUnsound  (constraint c, constraintList p);
+static constraint  inequalitySubstituteUnsound  (/*@returned@*/ constraint c, constraintList p);
 
-static constraint constraint_searchandreplace (constraint c, constraintExpr old, constraintExpr new);
-//bool rangeCheck (arithType ar1, constraintExpr expr1, arithType ar2, constraintExpr expr2);
-//bool satifies (constraint pre, constraint post);
-//bool resolve (constraint c, constraintList p);
-//constraintList reflectChangesEnsures (constraintList pre2, constraintList post1);
-//constraint constraint_simplify (constraint c);
+static constraint constraint_searchandreplace (/*@returned@*/ constraint c, constraintExpr old, constraintExpr new);
 
-//constraintList constraintList_fixConflicts (constraintList list1, constraintList list2);
 
-//constraintList constraintList_subsumeEnsures (constraintList list1, constraintList list2);
+static constraint constraint_addOr (/*@returned@*/ constraint orig, /*@observer@*/ constraint or);
 
-//constraintList constraintList_mergeEnsures (constraintList list1, constraintList list2);
-constraint  inequalitySubstitute  (constraint c, constraintList p);
+static bool resolveOr (/*@observer@*/ constraint c, /*@observer@*/ constraintList list);
+
+static /*@only@*/ constraintList reflectChangesEnsuresFree1 (/*@only@*/ constraintList pre2, constraintList post1);
 
 /*********************************************/
 
+
+
+
+/*@only@*/ constraintList constraintList_mergeEnsuresFreeFirst (constraintList list1, constraintList list2)
+{
+  constraintList ret;
+
+  ret = constraintList_mergeEnsures (list1, list2);
+
+  constraintList_free(list1);
+  return ret;
+}
                                            
-constraintList constraintList_mergeEnsures (constraintList list1, constraintList list2)
+/*@only@*/ constraintList constraintList_mergeEnsures (constraintList list1, constraintList list2)
 {
   constraintList ret;
   constraintList temp;
@@ -47,20 +54,23 @@ constraintList constraintList_mergeEnsures (constraintList list1, constraintList
   //ret = constraintList_makeNew();
 
   llassert(constraintList_isDefined(list1) );
-  llassert(constraintList_isDefined(list1) );
+  llassert(constraintList_isDefined(list2) );
 
   DPRINTF(( message ("constraintList_mergeEnsures: list1 %s list2 %s",
                     constraintList_print(list1), constraintList_print(list2)
                     )));
   
   ret = constraintList_fixConflicts (list1, list2);
-  ret = reflectChangesEnsures (ret, list2);
-  ret = constraintList_subsumeEnsures (ret, list2);
-  list2 = constraintList_subsumeEnsures (list2, ret);
-  temp = constraintList_copy(list2);
+  ret = reflectChangesEnsuresFree1 (ret, list2);
+  temp = constraintList_subsumeEnsures (ret, list2);
+  constraintList_free(ret);
+  ret = temp;
 
-  temp = constraintList_addList (temp, ret);
+  temp = constraintList_subsumeEnsures (list2, ret);
 
+  temp = constraintList_addList (temp, ret);
+  constraintList_free(ret);
+  
   DPRINTF(( message ("constraintList_mergeEnsures: returning %s ",
                     constraintList_print(temp) )
                     ));
@@ -71,7 +81,19 @@ constraintList constraintList_mergeEnsures (constraintList list1, constraintList
   //return ret;
 }
 
-constraintList constraintList_mergeRequires (constraintList list1, constraintList list2)
+
+/*@only@*/ constraintList constraintList_mergeRequiresFreeFirst (/*@only@*/ constraintList list1, constraintList list2)
+{
+  constraintList ret;
+
+  ret = constraintList_mergeRequires(list1, list2);
+
+  constraintList_free(list1);
+
+  return ret;
+}
+
+/*@only@*/ constraintList constraintList_mergeRequires (constraintList list1, constraintList list2)
 {
   constraintList ret;
   constraintList temp;
@@ -87,14 +109,14 @@ constraintList constraintList_mergeRequires (constraintList list1, constraintLis
  
   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) ) ) );
 
   return ret;
 }
 
-void checkArgumentList (exprNode temp, exprNodeList arglist, fileloc sequencePoint)
+void checkArgumentList (/*@out@*/ exprNode temp, exprNodeList arglist, fileloc sequencePoint)
 {
   temp->requiresConstraints = constraintList_makeNew();
   temp->ensuresConstraints = constraintList_makeNew();
@@ -103,9 +125,15 @@ void checkArgumentList (exprNode temp, exprNodeList arglist, fileloc sequencePoi
   
   exprNodeList_elements (arglist, el)
     {
+      constraintList temp2;
       exprNode_exprTraverse (el, FALSE, FALSE, sequencePoint);
+      temp2 = el->requiresConstraints;
       el->requiresConstraints = exprNode_traversRequiresConstraints(el);
+      constraintList_free(temp2);
+
+      temp2 = el->ensuresConstraints;
       el->ensuresConstraints  = exprNode_traversEnsuresConstraints(el);
+      constraintList_free(temp2);
 
       temp->requiresConstraints = constraintList_addList(temp->requiresConstraints,
                                                            el->requiresConstraints);
@@ -127,17 +155,19 @@ constraintList checkCall (exprNode fcn, exprNodeList arglist)
 
   preconditions = uentry_getFcnPreconditions (temp);
 
-  if (preconditions)
+  if (preconditions != constraintList_undefined)
     {
-      preconditions = constraintList_copy(preconditions);
-      preconditions= constraintList_togglePost (preconditions);   
+      preconditions = constraintList_togglePost (preconditions);
+      preconditions = constraintList_preserveCallInfo(preconditions, fcn);
       preconditions = constraintList_doSRefFixConstraintParam (preconditions, arglist);
     }
   else
     {
-      preconditions = constraintList_makeNew();
+      if (preconditions == NULL)
+       preconditions = constraintList_makeNew();
     }
-  
+  DPRINTF (( message("Done checkCall\n") ));
+  DPRINTF (( message("Returning list %q ", constraintList_printDetailed(preconditions) ) ));
   return preconditions;
 }
 
@@ -151,9 +181,8 @@ constraintList getPostConditions (exprNode fcn, exprNodeList arglist, exprNode f
 
   postconditions = uentry_getFcnPostconditions (temp);
 
-  if (postconditions)
+  if (postconditions != constraintList_undefined)
     {
-      postconditions = constraintList_copy(postconditions);
       postconditions = constraintList_doFixResult (postconditions, fcnCall);
       postconditions = constraintList_doSRefFixConstraintParam (postconditions, arglist);
     }
@@ -167,17 +196,21 @@ constraintList getPostConditions (exprNode fcn, exprNodeList arglist, exprNode f
 
 void mergeResolve (exprNode parent, exprNode child1, exprNode child2)
 {
-  constraintList temp;
+  constraintList temp, temp2;
 
-  DPRINTF( (message ("magically merging constraint into parent:%s for", exprNode_unparse (parent) )));
+  DPRINTF( (message ("magically merging constraint into parent:%s for", exprNode_unparse (parent) )) );
 
   DPRINTF( (message (" children:  %s and %s", exprNode_unparse (child1), exprNode_unparse(child2) ) ) );
 
   if (exprNode_isError (child1)  || exprNode_isError(child2) )
-     {
-       if (exprNode_isError (child1) && !exprNode_isError(child2) )
+    {
+      if (exprNode_isError (child1) && !exprNode_isError(child2) )
         {
+          constraintList_free(parent->requiresConstraints);
+
           parent->requiresConstraints = constraintList_copy (child2->requiresConstraints);
+          constraintList_free(parent->ensuresConstraints);
+
           parent->ensuresConstraints = constraintList_copy (child2->ensuresConstraints);
           DPRINTF((message ("Copied child constraints: pre: %s and post: %s",
                             constraintList_print( child2->requiresConstraints),
@@ -189,8 +222,8 @@ void mergeResolve (exprNode parent, exprNode child1, exprNode child2)
        else
         {
           llassert(exprNode_isError(child2) );
-          parent->requiresConstraints = constraintList_makeNew();
-          parent->ensuresConstraints = constraintList_makeNew();
+          //parent->requiresConstraints = constraintList_makeNew();
+          //parent->ensuresConstraints = constraintList_makeNew();
           return;
         }
      }
@@ -204,8 +237,8 @@ void mergeResolve (exprNode parent, exprNode child1, exprNode child2)
                     constraintList_print (child2->ensuresConstraints)
                     ) ) );
  
-  parent->requiresConstraints = constraintList_makeNew();
-  parent->ensuresConstraints = constraintList_makeNew();
+   constraintList_free(parent->requiresConstraints);
 
   parent->requiresConstraints = constraintList_copy (child1->requiresConstraints);
 
@@ -213,11 +246,22 @@ void mergeResolve (exprNode parent, exprNode child1, exprNode child2)
     temp = reflectChangesOr (child2->requiresConstraints, child1->ensuresConstraints);
   else
     temp = reflectChanges (child2->requiresConstraints, child1->ensuresConstraints);
+
+  temp2 = constraintList_mergeRequires (parent->requiresConstraints, temp);
+  constraintList_free(parent->requiresConstraints);
+  constraintList_free(temp);
   
-  parent->requiresConstraints = constraintList_mergeRequires (parent->requiresConstraints, temp);
+  parent->requiresConstraints = temp2;
+
+  DPRINTF( (message ("Parent requires constraints are %s  ",
+                    constraintList_print (parent->requiresConstraints)
+                    ) ) );
+
+   constraintList_free(parent->ensuresConstraints);
 
   parent->ensuresConstraints = constraintList_mergeEnsures(child1->ensuresConstraints,
                                                           child2->ensuresConstraints);
+
   
   DPRINTF( (message ("Parent constraints are %s and %s ",
                     constraintList_print (parent->requiresConstraints),
@@ -229,7 +273,7 @@ void mergeResolve (exprNode parent, exprNode child1, exprNode child2)
 
   
   
-constraintList constraintList_subsumeEnsures (constraintList list1, constraintList list2)
+/*@only@*/ constraintList constraintList_subsumeEnsures (constraintList list1, constraintList list2)
 {
   constraintList ret;
   ret = constraintList_makeNew();
@@ -239,7 +283,9 @@ constraintList constraintList_subsumeEnsures (constraintList list1, constraintLi
       DPRINTF ((message ("Examining %s", constraint_print (el) ) ) );
       if (!resolve (el, list2) )
        {
-           ret = constraintList_add (ret, el);
+         constraint temp;
+         temp = constraint_copy(el);
+         ret = constraintList_add (ret, temp);
        }
       else
        {
@@ -251,12 +297,28 @@ constraintList constraintList_subsumeEnsures (constraintList list1, constraintLi
 }
 
 
+
 /* tries to resolve constraints in list pre2 using post1 */
-constraintList reflectChanges (constraintList pre2, constraintList post1)
+/*@only@*/ constraintList reflectChangesFreePre (/*@only@*/ constraintList pre2, /*@observer@*/ constraintList post1)
+{
+  constraintList ret;
+  
+  ret = reflectChanges (pre2, post1);
+
+  constraintList_free (pre2);
+  
+  return ret;
+}
+
+
+/* tries to resolve constraints in list pre2 using post1 */
+/*@only@*/ constraintList reflectChanges (/*@observer@*/ constraintList pre2, /*@observer@*/ constraintList post1)
 {
   
   constraintList ret;
   constraint temp;
+  constraint temp2;
+
   ret = constraintList_makeNew();
   DPRINTF((message ("reflectChanges: lists %s and %s", constraintList_print(pre2), constraintList_print(post1) )));
   
@@ -268,13 +330,13 @@ constraintList reflectChanges (constraintList pre2, constraintList post1)
          if (!resolve (temp, post1) )
            {
              // try inequality substitution
-             constraint temp2;
+             //constraint temp2;
              
              // the inequality substitution may cause us to lose information
              //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 (temp, post1); 
+                temp2 = inequalitySubstitute (temp2, post1); 
                      if (!resolve (temp2, post1) )
                        {
                          temp2 = inequalitySubstituteUnsound (temp2, post1); 
@@ -282,6 +344,7 @@ constraintList reflectChanges (constraintList pre2, constraintList post1)
                              ret = constraintList_add (ret, temp2);
                        }
            }
+         constraint_free(temp);
        }
     } end_constraintList_elements;
 
@@ -290,7 +353,7 @@ constraintList reflectChanges (constraintList pre2, constraintList post1)
 }
 
 
-constraint constraint_addOr (constraint orig, constraint or)
+static constraint constraint_addOr (/*@returned@*/ constraint orig, /*@observer@*/ constraint or)
 {
   constraint c;
   c = orig;
@@ -309,7 +372,7 @@ constraint constraint_addOr (constraint orig, constraint or)
 }
 
 
-bool resolveOr (constraint c, constraintList list)
+static bool resolveOr (/*@observer@*/ constraint c, /*@observer@*/ constraintList list)
 {
   constraint temp;
 
@@ -327,14 +390,17 @@ bool resolveOr (constraint c, constraintList list)
   return FALSE;
 }
 
+/*This is a "helper" function for doResolveOr */
 
-constraint doResolve (constraint c, constraintList post1, bool * resolved)
+static /*@only@*/ constraint doResolve (/*@only@*/ constraint c, constraintList post1, bool * resolved)
 {
   constraint temp;
   
  if (!resolveOr (c, post1) )
        {
+
          temp = substitute (c, post1);
+         
          if (!resolveOr (temp, post1) )
            {
              // try inequality substitution
@@ -345,20 +411,29 @@ constraint doResolve (constraint c, constraintList post1, bool * resolved)
              temp2 = constraint_copy (c);
              //                  if (context_getFlag (FLG_ORCONSTRAINT) )
              temp2 = inequalitySubstitute (temp2, post1); 
-                     if (!resolveOr (temp2, post1) )
-                       {
-                         temp2 = inequalitySubstituteUnsound (temp2, post1); 
-                         if (!resolveOr (temp2, post1) )
-                           {
-                             if (!constraint_same (temp, temp2) )
-                               temp = constraint_addOr (temp, temp2);
-                             *resolved = FALSE;
-                             return temp;
-                           }
-                       }
+             if (!resolveOr (temp2, post1) )
+               {
+                 temp2 = inequalitySubstituteUnsound (temp2, post1); 
+                 if (!resolveOr (temp2, post1) )
+                   {
+                     if (!constraint_same (temp, temp2) )
+                       temp = constraint_addOr (temp, temp2);
+                     *resolved = FALSE;
+
+                     constraint_free(temp2);
+                     constraint_free(c);
+         
+                     return temp;
+                   }
+               }
+             
+             constraint_free(temp2);
            }
+         constraint_free(temp);
        }
-
+ constraint_free(c);
  *resolved = TRUE;
  return NULL;
 
@@ -366,7 +441,7 @@ constraint doResolve (constraint c, constraintList post1, bool * resolved)
 
 }
 
-constraint doResolveOr (constraint c, constraintList post1, /*@out@*/bool * resolved)
+static /*@only@*/ constraint doResolveOr (constraint c, constraintList post1, /*@out@*/bool * resolved)
 {
   constraint ret;
   constraint next;
@@ -378,6 +453,17 @@ constraint doResolveOr (constraint c, constraintList post1, /*@out@*/bool * reso
   ret->or = NULL;
 
   ret = doResolve (ret, post1, resolved);
+
+  if (*resolved)
+    {
+      if (next != NULL)
+       constraint_free(next);
+
+      /*we don't need to free ret when resolved is false*/
+      //      constraint_free(ret);
+      /*@i1*/ return NULL;
+    }
+
   while (next != NULL)
     {
       curr = next;
@@ -386,11 +472,19 @@ constraint doResolveOr (constraint c, constraintList post1, /*@out@*/bool * reso
 
       curr = doResolve (curr, post1, resolved);
       if (*resolved)
-       return NULL;
-            
+       {
+         /* curr is null so we don't try to free it*/
+         //constraint_free(curr);
+         
+         if (next != NULL)
+           constraint_free(next);
+         constraint_free(ret);
+         /*@i1*/ return NULL;
+       }
       ret = constraint_addOr (ret, curr);
+      constraint_free(curr);
     }
-  
+
   return ret;
 }
 
@@ -399,7 +493,7 @@ constraint doResolveOr (constraint c, constraintList post1, /*@out@*/bool * reso
 
 
 /* tries to resolve constraints in list pr2 using post1 */
-constraintList reflectChangesOr (constraintList pre2, constraintList post1)
+/*@only@*/ constraintList reflectChangesOr (constraintList pre2, constraintList post1)
 {
   bool resolved;
   constraintList ret;
@@ -420,8 +514,7 @@ constraintList reflectChangesOr (constraintList pre2, constraintList post1)
     DPRINTF((message ("reflectChangesOr: returning %s", constraintList_print(ret) ) ) );
     return ret;
 }
-
-constraintList reflectChangesEnsures (constraintList pre2, constraintList post1)
+static /*@only@*/ constraintList reflectChangesEnsures (/*@observer@*/ constraintList pre2, constraintList post1)
 {  
   constraintList ret;
   constraint temp;
@@ -446,7 +539,19 @@ constraintList reflectChangesEnsures (constraintList pre2, constraintList post1)
 }
 
 
-bool constraint_conflict (constraint c1, constraint c2)
+static /*@only@*/ constraintList reflectChangesEnsuresFree1 (/*@only@*/ constraintList pre2, constraintList post1)
+{
+  constraintList ret;
+
+  ret = reflectChangesEnsures (pre2, post1);
+  
+  constraintList_free(pre2);
+
+  return ret;
+}
+
+
+static bool constraint_conflict (constraint c1, constraint c2)
 {
   
   if (constraintExpr_similar(c1->lexpr, c2->lexpr) )
@@ -465,20 +570,18 @@ bool constraint_conflict (constraint c1, constraint c2)
 
 }
 
-void constraint_fixConflict (constraint good, constraint conflicting)
+static void constraint_fixConflict ( constraint good, /*@observer@*/ constraint conflicting) /*@modifies good@*/
 {
-  constraint temp;
   if (conflicting->ar ==EQ )
     {
       good->expr = constraintExpr_searchandreplace (good->expr, conflicting->lexpr, conflicting->expr);
-      temp = constraint_simplify (good);
-      constraint_overWrite (good, temp);
+      good = constraint_simplify (good);
     }
 
 
 }
 
-bool conflict (constraint c, constraintList list)
+static bool conflict (constraint c, constraintList list)
 {
 
   constraintList_elements (list, el)
@@ -494,7 +597,7 @@ bool conflict (constraint c, constraintList list)
 
 }
 
-//check if constraint in list1 and conflict with constraints in List2.  If so we
+//check if constraint in list1 conflicts with constraints in List2.  If so we
 //remove form list1 and change list2.
 constraintList constraintList_fixConflicts (constraintList list1, constraintList list2)
 {
@@ -505,34 +608,17 @@ constraintList constraintList_fixConflicts (constraintList list1, constraintList
     {
       if (! conflict (el, list2) )
        {
-           ret = constraintList_add (ret, el);
+         constraint temp;
+         temp = constraint_copy(el);
+         ret = constraintList_add (ret, temp);
        }
     } end_constraintList_elements;
 
     return ret;
-  
-    
-}
-
-bool resolve (/*@observer@*/ constraint c, /*@observer@*/ constraintList p)
-{
-  constraintList_elements (p, el)
-    {
-      if ( satifies (c, el) )
-       {
-         DPRINTF ( (message ("\n%s Satifies %s\n ", constraint_print(el), constraint_print(c) ) ) );
-         return TRUE;
-       }
-        DPRINTF ( (message ("\n%s does not satify %s\n ", constraint_print(el), constraint_print(c) ) ) );
-    }
-  end_constraintList_elements;
-  DPRINTF ( (message ("no constraints satify %s", constraint_print(c) ) ));
-  return FALSE;
 }
 
-
 /*returns true if constraint post satifies cosntriant pre */
-bool satifies (constraint pre, constraint post)
+static bool satifies (constraint pre, constraint post)
 {
   if (constraint_isAlwaysTrue (pre)  )
     return TRUE;
@@ -550,7 +636,24 @@ bool satifies (constraint pre, constraint post)
   return rangeCheck (pre->ar, pre->expr, post->ar, post->expr);
 }
 
-bool arithType_canResolve (arithType ar1, arithType ar2)
+
+bool resolve (/*@observer@*/ constraint c, /*@observer@*/ constraintList p)
+{
+  constraintList_elements (p, el)
+    {
+      if ( satifies (c, el) )
+       {
+         DPRINTF ( (message ("\n%s Satifies %s\n ", constraint_print(el), constraint_print(c) ) ) );
+         return TRUE;
+       }
+        DPRINTF ( (message ("\n%s does not satify %s\n ", constraint_print(el), constraint_print(c) ) ) );
+    }
+  end_constraintList_elements;
+  DPRINTF ( (message ("no constraints satify %s", constraint_print(c) ) ));
+  return FALSE;
+}
+
+static bool arithType_canResolve (arithType ar1, arithType ar2)
 {
   switch (ar1)
     {
@@ -581,7 +684,7 @@ bool arithType_canResolve (arithType ar1, arithType ar2)
 
 /* We look for constraint which are tautologies */
 
-bool constraint_isAlwaysTrue (constraint c)
+bool constraint_isAlwaysTrue (/*@observer@*/ constraint c)
 {
   constraintExpr l, r;
   bool /*@unused@*/ lHasConstant, rHasConstant;
@@ -645,6 +748,10 @@ bool constraint_isAlwaysTrue (constraint c)
     {
       DPRINTF(( message("constraint_IsAlwaysTrue: after removing constants  %s and %s are similar", constraintExpr_unparse(l), constraintExpr_unparse(r) ) ));
       DPRINTF(( message("constraint_IsAlwaysTrue: rconstant is  %d", rConstant ) ));
+      
+      constraintExpr_free(l);
+      constraintExpr_free(r);
+      
       switch (c->ar)
        {
        case EQ:
@@ -666,6 +773,8 @@ bool constraint_isAlwaysTrue (constraint c)
     }  
       else
       {
+       constraintExpr_free(l);
+       constraintExpr_free(r);
        DPRINTF(( message("Constraint %s is not always true", constraint_print(c) ) ));
        return FALSE;
       }
@@ -673,7 +782,7 @@ bool constraint_isAlwaysTrue (constraint c)
   BADEXIT;
 }
 
-bool rangeCheck (arithType ar1, constraintExpr expr1, arithType ar2, constraintExpr expr2)
+static bool rangeCheck (arithType ar1, /*@observer@*/ constraintExpr expr1, arithType ar2, /*@observer@*/ constraintExpr expr2)
 
 {
   DPRINTF ((message ("Doing Range CHECK %s and %s", constraintExpr_unparse(expr1), constraintExpr_unparse(expr2) ) ));
@@ -694,17 +803,27 @@ bool rangeCheck (arithType ar1, constraintExpr expr1, arithType ar2, constraintE
        constraintExpr e1, e2;
        bool p1, p2;
        int const1, const2;
-              
-       e1 = constraintExpr_propagateConstants (expr1, &p1, &const1);
+       
+       e1 = constraintExpr_copy(expr1);
+       e2 = constraintExpr_copy(expr2);
+
+       e1 = constraintExpr_propagateConstants (e1, &p1, &const1);
 
-       e2 = constraintExpr_propagateConstants (expr2, &p2, &const2);
+       e2 = constraintExpr_propagateConstants (e2, &p2, &const2);
 
        if (p1 && p2)
         if (const1 <= const2)
           if (constraintExpr_similar (e1, e2) )
-            return TRUE;
+            {
+              constraintExpr_free(e1);
+              constraintExpr_free(e2);
+              return TRUE;
+            }
        
        DPRINTF( ("Can't Get value"));
+       
+       constraintExpr_free(e1);
+       constraintExpr_free(e2);
        return FALSE;
      }
    
@@ -729,14 +848,23 @@ bool rangeCheck (arithType ar1, constraintExpr expr1, arithType ar2, constraintE
        bool p1, p2;
        int const1, const2;
        
-       e1 = constraintExpr_propagateConstants (expr1, &p1, &const1);
+       e1 = constraintExpr_copy(expr1);
+       e2 = constraintExpr_copy(expr2);
 
-       e2 = constraintExpr_propagateConstants (expr2, &p2, &const2);
+       e1 = constraintExpr_propagateConstants (e1, &p1, &const1);
+
+       e2 = constraintExpr_propagateConstants (e2, &p2, &const2);
 
        if (p1 && p2)
         if (const1 >= const2)
           if (constraintExpr_similar (e1, e2) )
-            return TRUE;
+            {
+              constraintExpr_free(e1);
+              constraintExpr_free(e2);
+              return TRUE;
+            }
+       constraintExpr_free(e1);
+       constraintExpr_free(e2);
        
        DPRINTF( ("Can't Get value"));
        return FALSE;
@@ -748,13 +876,13 @@ bool rangeCheck (arithType ar1, constraintExpr expr1, arithType ar2, constraintE
    return FALSE;
    
  default:
-     llcontbug((message("Unhandled case in switch: %s", arithType_print(ar1) ) ) );
+     llcontbug((message("Unhandled case in switch: %q", arithType_print(ar1) ) ) );
  }
   BADEXIT;
 }
 
 
-constraint constraint_searchandreplace (constraint c, constraintExpr old, constraintExpr new)
+static constraint constraint_searchandreplace (/*@returned@*/ constraint c, constraintExpr old, constraintExpr new)
 {
   DPRINTF (("Doing replace for lexpr") );
   c->lexpr = constraintExpr_searchandreplace (c->lexpr, old, new);
@@ -774,7 +902,7 @@ bool constraint_search (constraint c, constraintExpr old) /*@*/
 }
 
 //adjust file locs and stuff
-constraint constraint_adjust (constraint substitute, constraint old)
+static constraint constraint_adjust (/*@returned@*/ constraint substitute, /*@observer@*/ constraint old)
 {
   fileloc loc1, loc2, loc3;
 
@@ -802,6 +930,10 @@ constraint constraint_adjust (constraint substitute, constraint old)
        substitute = constraint_simplify(substitute);
       }
 
+  fileloc_free (loc1);
+  fileloc_free (loc2);
+  fileloc_free (loc3);
+
   return substitute;
   
 }
@@ -812,7 +944,7 @@ constraint constraint_adjust (constraint substitute, constraint old)
 
    Warning this is sound but throws out information
  */
-constraint  inequalitySubstitute  (constraint c, constraintList p)
+constraint  inequalitySubstitute  (/*@returned@*/ constraint c, constraintList p)
 {
   if (c->ar != GTE)
     return c;
@@ -822,10 +954,12 @@ constraint  inequalitySubstitute  (constraint c, constraintList p)
        if ( el->ar == LT)
         //      if (!constraint_conflict (c, el) )
           {
-            constraint temp;
+            //constraint temp;
             constraintExpr  temp2;
             
-            temp = constraint_copy(el);
+            /*@i22*/
+
+            //temp = constraint_copy(el);
             
             //      temp = constraint_adjust(temp, c);
 
@@ -837,6 +971,7 @@ constraint  inequalitySubstitute  (constraint c, constraintList p)
                                   constraintExpr_print (el->expr) )
                          ));
                 temp2   = constraintExpr_copy (el->lexpr);
+                constraintExpr_free(c->expr);
                 c->expr =  constraintExpr_makeIncConstraintExpr (temp2);
               }
             
@@ -855,7 +990,7 @@ constraint  inequalitySubstitute  (constraint c, constraintList p)
    Like inequalitySubstitute we're throwing away some information
 */
 
-constraint  inequalitySubstituteUnsound  (constraint c, constraintList p)
+static constraint  inequalitySubstituteUnsound  (/*@returned@*/ constraint c, constraintList p)
 {
   DPRINTF (( message ("Doing inequalitySubstituteUnsound " ) ));
   
@@ -868,10 +1003,10 @@ constraint  inequalitySubstituteUnsound  (constraint c, constraintList p)
        if ( ( el->ar == LTE) || (el->ar == LT) )
         //      if (!constraint_conflict (c, el) )
           {
-            constraint temp;
+            // constraint temp;
             constraintExpr  temp2;
             
-            temp = constraint_copy(el);
+            //temp = constraint_copy(el);
             
             //      temp = constraint_adjust(temp, c);
             temp2   = constraintExpr_copy (el->expr);
@@ -885,6 +1020,7 @@ constraint  inequalitySubstituteUnsound  (constraint c, constraintList p)
                               constraintExpr_print (temp2) ) ));
             
             c->lexpr = constraintExpr_searchandreplace (c->lexpr, el->lexpr, temp2);
+            constraintExpr_free(temp2);
           }
     }
   end_constraintList_elements;
@@ -893,7 +1029,7 @@ constraint  inequalitySubstituteUnsound  (constraint c, constraintList p)
   return c;
 }
 
-constraint substitute (constraint c, constraintList p)
+/*@only@*/ constraint substitute (/*@observer@*/ constraint c, constraintList p)
 {
   constraint ret;
 
@@ -905,6 +1041,7 @@ constraint substitute (constraint c, constraintList p)
 
           {
             constraint temp;
+            
             temp = constraint_copy(el);
             
             temp = constraint_adjust(temp, ret);
@@ -916,17 +1053,31 @@ constraint substitute (constraint c, constraintList p)
          
             ret = constraint_searchandreplace (ret, temp->lexpr, temp->expr);
             DPRINTF(( message ("The new constraint is %s", constraint_print (ret) ) ));
+            constraint_free(temp);
           }
     }
   end_constraintList_elements;
+  DPRINTF(( message ("The finial new constraint is %s", constraint_print (ret) ) ));
 
   ret = constraint_simplify(ret);
   return ret;
 }
 
+
+/*@only@*/ constraintList constraintList_substituteFreeTarget (/*@only@*/ constraintList target, /*@observer@*/ constraintList subList)
+{
+constraintList ret;
+
+ret = constraintList_substitute (target, subList);
+
+constraintList_free(target);
+
+return ret;
+}
+
 /* we try to do substitutions on each constraint in target using the constraint in sublist*/
 
-constraintList constraintList_substitute (constraintList target, constraintList subList)
+/*@only@*/ constraintList constraintList_substitute (constraintList target,/*2observer@*/  constraintList subList)
 {
 
   constraintList ret;
@@ -935,29 +1086,18 @@ constraintList constraintList_substitute (constraintList target, constraintList
   
   constraintList_elements(target, el)
   { 
-    el = substitute(el, subList);
-    ret = constraintList_add (ret, el);
+    constraint temp;
+    #warning make sure that a side effect is not expected
+
+    temp = substitute(el, subList);
+    ret = constraintList_add (ret, temp);
   }
   end_constraintList_elements;
-#warning mem leak
-  return ret;
-}
-
-constraint constraint_solveWithFlag (constraint c, bool *b)
-{
 
-  *b = FALSE;
-  if (c->lexpr->kind == binaryexpr)
-    {
-      *b = TRUE;
-      DPRINTF( (message ("Solving %s\n", constraint_print(c) ) ) );
-      c->expr = constraintExpr_solveBinaryExpr (c->lexpr, c->expr);
-      DPRINTF( (message ("Solved and got %s\n", constraint_print(c) ) ) );
-    }
-  return c;
+  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);
@@ -986,7 +1126,7 @@ static arithType flipAr (arithType ar)
   BADEXIT;
 }
 
-static constraint  constraint_swapLeftRight (constraint c)
+static constraint  constraint_swapLeftRight (/*@returned@*/ constraint c)
 {
   constraintExpr temp;
   c->ar = flipAr (c->ar);
@@ -999,12 +1139,12 @@ static constraint  constraint_swapLeftRight (constraint c)
 
 
 
-constraint constraint_simplify (constraint c)
+constraint constraint_simplify ( /*@returned@*/ constraint c)
 {
   c->lexpr = constraintExpr_simplify (c->lexpr);
   c->expr  = constraintExpr_simplify (c->expr);
 
-  if (c->lexpr->kind == binaryexpr)
+  if (constraintExpr_isBinaryExpr (c->lexpr) )
     {
       c = constraint_solve (c);
       
This page took 0.070475 seconds and 4 git commands to generate.