*** empty log message ***

diff --git a/src/Makefile b/src/Makefile
index cb7a79bf11aebae5bf5afb5fcc27104efa0bc986..90f5bede1c22d92d628b489d3169df43a5459daa 100644 (file)
--- a/src/Makefile
+++ b/src/Makefile
@@ -389,7 +389,7 @@ linttest:
        ${LCLINTNEW} -f lclint.lclintrc $(CPPFLAGS) +singleinclude cpphash.c +forcehints -misplacedsharequal +showsourceloc -unrecogcomments -supcounts -fcnuse -exportlocal -constuse -mts file -mts filerw +partial
 
 lint: 
-       ../bin/lclint -f lclint.lclintrc llmain.c $(CPPFLAGS) +singleinclude $(ALLSRC) -dump lclint +forcehints -misplacedsharequal +showsourceloc -supcounts -fcnuse -exportlocal -constuse  -mts file
+       ../bin/lclint -f lclint.lclintrc llmain.c $(CPPFLAGS) +singleinclude $(ALLSRC) -dump lclint +forcehints -misplacedsharequal +showsourceloc -supcounts -fcnuse -exportlocal -unrecogcomments -constuse  -mts file
 
 # -mts file
 

diff --git a/src/constraint.c b/src/constraint.c
index 4a83dc822e1de4cac2056e5783d1b752d67636bb..6a8c98979cda2aef8c91ca200ed2f1788a971305 100644 (file)
--- a/src/constraint.c
+++ b/src/constraint.c
@@ -1073,6 +1073,7 @@ constraint constraint_undump (FILE *f)
   c->expr =  expr;
 
   free(os);
+  c = constraint_preserveOrig(c);
   return c;
 }
 

diff --git a/src/constraintGeneration.c b/src/constraintGeneration.c
index 5919beebc9b0f91679ce242826b4f915676affb7..21d175fe8cedf21c1364d84852b0f5fae9e17bff 100644 (file)
--- a/src/constraintGeneration.c
+++ b/src/constraintGeneration.c
@@ -369,6 +369,8 @@ static exprNode doIf (/*@returned@*/  exprNode e, /*@dependent@*/ exprNode test,
   DPRINTF ((message ("doIf: test true ensures %s ", constraintList_print(test->trueEnsuresConstraints) ) ) );
   
   constraintList_free(e->requiresConstraints);
+
+  
   e->requiresConstraints = constraintList_reflectChanges(body->requiresConstraints, test->trueEnsuresConstraints);
 
   e->requiresConstraints = constraintList_reflectChangesFreePre (e->requiresConstraints,
@@ -593,8 +595,7 @@ static void exprNode_doGenerateConstraintSwitch (/*@dependent@*/ exprNode switch
 
   if (body->kind != XPR_STMTLIST )
     {
-      DPRINTF((message("exprNode_doGenerateConstraintSwitch: non
-stmtlist: %s",
+      DPRINTF((message("exprNode_doGenerateConstraintSwitch: non stmtlist: %s",
                       exprNode_unparse(body) )
               ));
       //      llassert(body->kind == XPR_STMT );
@@ -611,8 +612,7 @@ stmtlist: %s",
       stmtList = exprNode_makeDependent(stmtList);
     }
 
-  DPRINTF((message("exprNode_doGenerateConstraintSwitch: stmtlist: %s
-stmt: %s",
+  DPRINTF((message("exprNode_doGenerateConstraintSwitch: stmtlist: %s stmt: %s",
                   exprNode_unparse(stmtList), exprNode_unparse(stmt) )
           ));
 

diff --git a/src/constraintList.c b/src/constraintList.c
index 7c9752f7686eb0033a057e1a2ba9db9ab3885ac8..d5db31658b2d79a670867b59eff0d5625acd8434 100644 (file)
--- a/src/constraintList.c
+++ b/src/constraintList.c
@@ -386,7 +386,7 @@ constraintList constraintList_preserveOrig (constraintList c)
 
 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)
   {

diff --git a/src/constraintResolve.c b/src/constraintResolve.c
index 38979ad7f432a654a2406607dfc85b66063e4614..5a70dacae4220f8b5ea9cb1e860bcdcc3d621f4d 100644 (file)
--- a/src/constraintResolve.c
+++ b/src/constraintResolve.c
@@ -25,6 +25,8 @@ static bool rangeCheck (arithType p_ar1, /*@observer@*/ constraintExpr p_expr1,
 
 static constraint  inequalitySubstituteUnsound  (/*@returned@*/ constraint p_c, constraintList p_p);
 
+static constraint  inequalitySubstituteStrong  (/*@returned@*/ constraint p_c, constraintList p_p);
+
 static constraint constraint_searchandreplace (/*@returned@*/ constraint p_c, constraintExpr p_old, constraintExpr p_newExpr);
 
 
@@ -238,14 +240,18 @@ void exprNode_mergeResolve (exprNode parent, exprNode child1, exprNode child2)
 }
 
 
+
 /* tries to resolve constraints in list pre2 using post1 */
-/*@only@*/ constraintList constraintList_reflectChanges(/*@observer@*/ constraintList pre2, /*@observer@*/ constraintList post1)
+
+static /*@only@*/ constraintList reflectChangesNoOr (/*@observer@*/ /*@temp@*/ constraintList pre2, /*@observer@*/ /*@temp@*/ constraintList post1)
 {
   
   constraintList ret;
   constraint temp;
   constraint temp2;
 
+  llassert  (! context_getFlag (FLG_ORCONSTRAINT) );
+
   ret = constraintList_makeNew();
   DPRINTF((message ("reflectChanges: lists %s and %s", constraintList_print(pre2), constraintList_print(post1) )));
   
@@ -285,6 +291,19 @@ void exprNode_mergeResolve (exprNode parent, exprNode child1, exprNode child2)
     return ret;
 }
 
+/* tries to resolve constraints in list pre2 using post1 */
+/*@only@*/ constraintList constraintList_reflectChanges(/*@observer@*/ constraintList pre2, /*@observer@*/ constraintList post1)
+{
+  constraintList temp;
+  
+  if ( context_getFlag (FLG_ORCONSTRAINT) )
+    
+    temp = constraintList_reflectChangesOr (pre2, post1);
+  else
+    temp = reflectChangesNoOr(pre2, post1);
+
+  return temp;                          
+}
 
 static constraint constraint_addOr (/*@returned@*/ constraint orig, /*@observer@*/ constraint orConstr)
 {
@@ -340,38 +359,57 @@ static /*@only@*/ constraint doResolve (/*@only@*/ constraint c, constraintList
              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
+             //so we don't want to store the result but we do  anyway
              temp2 = constraint_copy (c);
              //                  if (context_getFlag (FLG_ORCONSTRAINT) )
-             temp2 = inequalitySubstitute (temp2, post1); 
+             temp2 = inequalitySubstitute (temp2, post1);
              if (!resolveOr (temp2, post1) )
                {
-                 temp2 = inequalitySubstituteUnsound (temp2, post1); 
-                 if (!resolveOr (temp2, post1) )
+                 constraint temp3;
+                 temp3 = constraint_copy(temp2);
+                 
+                 temp3 = inequalitySubstituteStrong (temp3, post1);
+                 if (!resolveOr (temp3, post1) )
                    {
-                     if (!constraint_same (temp, temp2) )
-                       temp = constraint_addOr (temp, temp2);
-                     *resolved = FALSE;
-
+                     temp2 = inequalitySubstituteUnsound (temp2, post1); 
+                     if (!resolveOr (temp2, post1) )
+                       {
+                         if (!constraint_same (temp, temp2) )
+                           temp = constraint_addOr (temp, temp2);
+
+                         if (!constraint_same (temp, temp3) && !constraint_same (temp3, temp2) )
+                           temp = constraint_addOr (temp, temp3);
+                         
+                         *resolved = FALSE;
+                         
+                         constraint_free(temp2);
+                         constraint_free(temp3);
+                         constraint_free(c);
+                         
+                         return temp;
+                       }
                      constraint_free(temp2);
-                     constraint_free(c);
-         
-                     return temp;
+                     constraint_free(temp3);
+                   }
+                 else
+                   {
+                     constraint_free(temp2);
+                     constraint_free(temp3);
                    }
                }
-             
-             constraint_free(temp2);
+             else
+               {
+                 constraint_free(temp2);
+               }                 
+
            }
          constraint_free(temp);
        }
- 
  constraint_free(c);
  
  *resolved = TRUE;
  return NULL;
 
-
-
 }
 
 static /*@only@*/ constraint doResolveOr (constraint c, constraintList post1, /*@out@*/bool * resolved)
@@ -901,6 +939,7 @@ static constraint constraint_adjust (/*@returned@*/ constraint substitute, /*@ob
 
    Warning this is sound but throws out information
  */
+
 constraint  inequalitySubstitute  (/*@returned@*/ constraint c, constraintList p)
 {
   if (c->ar != GTE)
@@ -908,7 +947,7 @@ constraint  inequalitySubstitute  (/*@returned@*/ constraint c, constraintList p
   
   constraintList_elements (p, el)
     {
-       if ( el->ar == LT)
+      if ( (el->ar == LT )  )
         //      if (!constraint_conflict (c, el) )
           {
             //constraint temp;
@@ -922,7 +961,7 @@ constraint  inequalitySubstitute  (/*@returned@*/ constraint c, constraintList p
 
             if (constraintExpr_same (el->expr, c->expr) )
               {
-                DPRINTF((message ("inequalitySubstitute Replacing %s in %s with  %s",
+                DPRINTF((message ("inequalitySubstitute Replacing %q in %q with  %q",
                                   constraintExpr_print (c->expr),
                                   constraint_print (c),
                                   constraintExpr_print (el->expr) )
@@ -930,6 +969,7 @@ constraint  inequalitySubstitute  (/*@returned@*/ constraint c, constraintList p
                 temp2   = constraintExpr_copy (el->lexpr);
                 constraintExpr_free(c->expr);
                 c->expr =  constraintExpr_makeIncConstraintExpr (temp2);
+
               }
             
           }
@@ -940,6 +980,70 @@ constraint  inequalitySubstitute  (/*@returned@*/ constraint c, constraintList p
   return c;
 }
 
+
+/* drl7x 7/26/001
+
+   THis function is like inequalitySubstitute but it adds the rule
+   added the rules x >= y &&  y <= b  ===> x >= b
+    x >= y &&  y < b  ===> x >= b + 1
+
+   This is sound but sonce it throws out additional information it should only one used
+   if we're oring constraints.
+ */
+
+static constraint  inequalitySubstituteStrong  (/*@returned@*/ constraint c, constraintList p)
+{
+  DPRINTF (( message ("inequalitySubstituteStrong examining substituting for %q", constraint_print(c) ) ));      
+
+  if (c->ar != GTE)
+    return c;
+  
+  DPRINTF (( message ("inequalitySubstituteStrong examining substituting for %q with %q",
+                     constraint_print(c), constraintList_print(p) ) ));      
+  constraintList_elements (p, el)
+    {
+      DPRINTF (( message ("inequalitySubstituteStrong examining substituting %s on %s", constraint_print(el), constraint_print(c) ) ));      
+
+      if ( (el->ar == LT ) ||  (el->ar == LTE )  )
+        //      if (!constraint_conflict (c, el) )
+          {
+            //constraint temp;
+            constraintExpr  temp2;
+            
+            /*@i22*/
+
+            //temp = constraint_copy(el);
+            
+            //      temp = constraint_adjust(temp, c);
+
+            if (constraintExpr_same (el->lexpr, c->expr) )
+              {
+                DPRINTF((message ("inequalitySubstitute Replacing %s in %s with  %s",
+                                  constraintExpr_print (c->expr),
+                                  constraint_print (c),
+                                  constraintExpr_print (el->expr) )
+                         ));
+                temp2   = constraintExpr_copy (el->expr);
+                constraintExpr_free(c->expr);
+                if ( (el->ar == LTE ) )
+                  {
+                    c->expr = temp2;
+                  }
+                else
+                  {
+                    c->expr =  constraintExpr_makeIncConstraintExpr (temp2);
+                  }
+              }
+            
+          }
+    }
+  end_constraintList_elements;
+
+  c = constraint_simplify(c);
+  return c;
+}
+
+
 /* This function performs substitutions based on the rule:
    for a constraint of the form expr1 >= expr2;   a < b =>
    a = b -1 for all a in expr1.  This will work in most cases.