Remove empty configure file. This should not be in CVS.

[splint.git] / src / constraintResolve.c

diff --git a/src/constraintResolve.c b/src/constraintResolve.c
index d154f95df806d567cf98046b70e840769e9bd06f..6f795b399bc2392354e954d5aca03d4c3b616329 100644 (file)
--- 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);
-      /*@i5232@*/ ret = constraintList_addList(ret, list2); /* fix this? */
+      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);
@@ -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;
 }