X-Git-Url: http://andersk.mit.edu/gitweb/splint.git/blobdiff_plain/4a689c7f182a8860dda9ef42e85afc3fbc9b7cab..508533c52d02429894d89b95224577d8e3cf3c48:/src/constraintResolve.c

diff --git a/src/constraintResolve.c b/src/constraintResolve.c
index 5231742..6f795b3 100644
--- a/src/constraintResolve.c
+++ b/src/constraintResolve.c
@@ -17,8 +17,8 @@
 ** the Free Software Foundation, Inc., 59 Temple Place - Suite 330, Boston,
 ** MA 02111-1307, USA.
 **
-** For information on splint: splint@cs.virginia.edu
-** To report a bug: splint-bug@cs.virginia.edu
+** For information on splint: info@splint.org
+** To report a bug: splint-bug@splint.org
 ** For more information: http://www.splint.org
 */
 
@@ -39,7 +39,13 @@
 # include "exprNodeSList.h"
 
 
-/*@access constraint, exprNode @*/
+/*@access constraint, exprNode @*/ /*!!! NO! Don't do this so recklessly - design your code more carefully so you don't need to! */
+
+/*@-nullderef@*/ /* !!! DRL needs to fix this code! */
+/*@-nullstate@*/ /* !!! DRL needs to fix this code! */
+/*@-nullpass@*/ /* !!! DRL needs to fix this code! */
+/*@-temptrans@*/ /* !!! DRL needs to fix this code! */
+
 
 
 static constraint  inequalitySubstitute  (/*@returned@*/ constraint p_c, constraintList p_p);
@@ -128,7 +134,7 @@ static /*@only@*/ constraintList reflectChangesEnsuresFree1 (/*@only@*/ constrai
   if (context_getFlag (FLG_REDUNDANTCONSTRAINTS) )
     {
       ret = constraintList_copy(list1);
-      ret = constraintList_addList(ret, list2);
+      ret = constraintList_addList(ret, list2); 
       return ret;
     }
     
@@ -378,12 +384,22 @@ static /*@only@*/ constraint doResolve (/*@only@*/ constraint c, constraintList
   constraint temp;
 
   llassert(constraint_isUndefined (c->or ) );
+
+  DPRINTF((message("doResolve:: call on constraint c = : %q and constraintList %q",
+		   constraint_printOr(c), constraintList_print(post1)
+		   )
+	   ));
   
   if (!resolveOr (c, post1) )
     {
       
       temp = constraint_substitute (c, post1);
       
+      DPRINTF((message("doResolve:: after substitute temp is %q",
+		   constraint_printOr(temp)
+		       )
+	       ));
+  
       if (!resolveOr (temp, post1) )
 	{
 	  /* try inequality substitution */
@@ -407,11 +423,57 @@ static /*@only@*/ constraint doResolve (/*@only@*/ constraint c, constraintList
 		  if (!resolveOr (temp2, post1) )
 		    {
 		      if (!constraint_same (temp, temp2) )
-			temp = constraint_addOr (temp, temp2);
-		      
+			{
+			  /* drl added 8/28/2002*/
+			  /*make sure that the information from
+			    a post condition like i = i + 1 is transfered
+			  */
+			  constraint tempSub;
+			  tempSub = constraint_substitute (temp2, post1);
+
+			  DPRINTF((
+				   message("doResolve: adding %s ",
+					   constraint_printOr(tempSub)
+					   )
+				   ));
+			  
+			  DPRINTF((
+				   message("doResolve: not adding %s ",
+					   constraint_printOr(temp2)
+					   )
+				   ));
+			  
+			  temp = constraint_addOr (temp, tempSub);
+			  constraint_free(tempSub);
+			  
+			}
 		      if (!constraint_same (temp, temp3) && !constraint_same (temp3, temp2) )
-			temp = constraint_addOr (temp, temp3);
-		      
+			{
+			 /* drl added 8/28/2002*/
+			  /*make sure that the information from
+			    a post condition like i = i + 1 is transfered
+			  */
+			  constraint tempSub;
+			  
+			  tempSub = constraint_substitute (temp3, post1);
+
+			  DPRINTF((
+				   message("doResolve: adding %s ",
+					   constraint_printOr(tempSub)
+					   )
+				   ));
+
+			  
+			  DPRINTF((
+				   message("doResolve: not adding %s ",
+					   constraint_printOr(temp3)
+					   )
+				   ));
+
+			  temp = constraint_addOr (temp, tempSub);
+
+			  constraint_free(tempSub);
+			}
 		      *resolved = FALSE;
 		      
 		      constraint_free(temp2);
@@ -439,7 +501,7 @@ static /*@only@*/ constraint doResolve (/*@only@*/ constraint c, constraintList
     }
   constraint_free(c);
   
-  *resolved = TRUE;
+  /*drl bee: pbr*/ *resolved = TRUE;
   return NULL;
 }
 
@@ -454,7 +516,7 @@ static /*@only@*/ constraint doResolveOr (/*@observer@*/ /*@temp@*/ constraint c
 
 
   
-  *resolved = FALSE;
+   /*drl bee: pbr*/ *resolved = FALSE;
 
 
   ret = constraint_copy(c);
@@ -488,7 +550,7 @@ static /*@only@*/ constraint doResolveOr (/*@observer@*/ /*@temp@*/ constraint c
 
       curr = doResolve (curr, post1, resolved);
       
-      if (*resolved)
+    /*drl bee: pbr*/    if (*resolved)
 	{
 	  /* curr is null so we don't try to free it*/
 	  llassert(curr == NULL);
@@ -1286,20 +1348,22 @@ static constraint  inequalitySubstituteUnsound  (/*@returned@*/ constraint c, co
 	     
 	     temp = constraint_adjust(temp, ret);
 
-	     DPRINTF((message ("Substituting %s in the constraint %s",
-			       constraint_print (temp), constraint_print (ret)
+	     DPRINTF((message ("constraint_substitute :: Substituting in %s using %s",
+			       constraint_print (ret), constraint_print (temp)
 			       ) ) );
 			       
 	  
 	     ret = constraint_searchandreplace (ret, temp->lexpr, temp->expr);
-	     DPRINTF(( message ("The new constraint is %s", constraint_print (ret) ) ));
+	     DPRINTF(( message (" constraint_substitute :: 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);
+
+  DPRINTF(( message (" constraint_substitute :: The final new constraint is %s", constraint_print (ret) ) ));
+
   return ret;
 }