It mostly works but it has a convolted API that needs fixxing.

diff --git a/src/constraint.c b/src/constraint.c
index 4b7b5c244dbf80ca06e4611a415d40c5036b523b..7693e2f97a882621e4acf388cbbd01f44c1eae5e 100644 (file)
--- a/src/constraint.c
+++ b/src/constraint.c
@@ -350,7 +350,7 @@ cstring  constraint_printDetailed (constraint c)
     }
   else
     {
-    st = message ("Function Post condition:\nBased on the constraint %s this function appears to have the post condition %s", constraint_print (c), constraint_print(c->orig) );
+    st = message ("Function Post condition:\nThis function appears to have the post condition %s\n based on %s", constraint_print (c), constraint_print(c->orig) );
     }
   return st;
 }

diff --git a/src/constraintGeneration.c b/src/constraintGeneration.c
index ed0bbd7b17eab0053dd53ba74b6599d4ae995b2d..70e1ae8da8f4a8bf7e1d0e8feeb21797bd63ed26 100644 (file)
--- a/src/constraintGeneration.c
+++ b/src/constraintGeneration.c
@@ -211,12 +211,14 @@ bool exprNode_stmtList  (exprNode e)
   stmt1 = exprData_getPairA (e->edata);
   stmt2 = exprData_getPairB (e->edata);
 
-  
+
+  DPRINTF(("XW        stmtlist       ") );
+  DPRINTF ((message("XW%s    |        %s", exprNode_unparse(stmt1), exprNode_unparse(stmt2) ) ) );
+   
   exprNode_stmt (stmt1);
   DPRINTF(("\nstmt after stmtList call " ));
 
   exprNode_stmt (stmt2);
-
   mergeResolve (e, stmt1, stmt2 );
   DPRINTF ( (message ("smtlist constraints are: pre: %s \n and \t post %s\n",
                      constraintList_print(e->requiresConstraints),

diff --git a/src/constraintResolve.c b/src/constraintResolve.c
index 24d43cf8aec7e4539e557bf3bf64bb00d51fc53c..6367d5c25449a12b33bb1102497131aab0fbb13e 100644 (file)
--- a/src/constraintResolve.c
+++ b/src/constraintResolve.c
@@ -187,6 +187,22 @@ constraint solveforterm (constraint c)
     return c;
 }
 
+constraint solveforOther (constraint c)
+{
+  constraintExpr p;
+    p = c->expr;
+    while (p->expr != NULL)
+      {
+       TPRINTF( (message("Moving %s", constraintExpr_print (c->expr) ) ) );
+       c->lexpr = termMove(c->lexpr, p);
+       p->op = p->expr->op;
+       #warning memleak
+
+       p->expr = p->expr->expr;
+      }
+    return c;
+}
+
 constraint constraint_simplify (constraint c)
 {
   c =  solveforterm (c);
@@ -230,11 +246,76 @@ constraintExpr constraintExpr_substituteTerm (constraintExpr expr, constraintTer
 
    return expr;
 }
-constraint constraint_substituteTerm (constraint c, constraintTerm oldterm, constraintExpr replacement)
+
+/* returns true  if fileloc for term2 is closer to file for term1 than is term3*/
+
+bool fileloc_closer (constraintTerm term1, constraintTerm term2, constraintTerm term3)
 {
-  c->lexpr = constraintExpr_substituteTerm (c->lexpr, oldterm, replacement);
-  c->expr   = constraintExpr_substituteTerm (c->expr, oldterm, replacement);
-  return c;
+   if ( fileloc_lessthan (term1->loc, term2->loc) )
+     {
+       if (fileloc_lessthan (term2->loc, term3->loc) )
+        {
+          llassert (fileloc_lessthan (term1->loc, term3->loc) );
+          return TRUE;
+        }
+       else
+        {
+          return FALSE;
+        }
+     }
+
+   if ( ! (fileloc_lessthan (term1->loc, term2->loc) ) )
+     {
+       if (!fileloc_lessthan (term2->loc, term3->loc) )
+        {
+          llassert (fileloc_lessthan (term3->loc, term1->loc) );
+          return TRUE;
+        }
+       else
+        {
+          return FALSE;
+          
+        }
+     }
+
+   llassert(FALSE);
+   return FALSE;
+}
+
+constraint constraint_substituteTerm (constraint c, constraint subs)
+{
+  constraintTerm oldterm;
+  constraintExpr replacement;
+  
+    llassert(subs->lexpr->expr == NULL);
+    
+
+    oldterm = subs->lexpr->term;
+    replacement = subs->expr;       
+    
+    // Chessy hack assumes that subs always has the form g:1 = g:2 + expr
+
+    /*@i2*/
+    
+    /*find out which value to substitute*/
+    TPRINTF((message ("doing substitute for %s and %s", constraint_print (c), constraint_print(subs) ) ) );
+    if ( constraintExpr_containsTerm (subs->expr, subs->lexpr->term) )
+      {
+       TPRINTF(("doing new stuff"));
+       if (fileloc_closer (c->lexpr->term, subs->expr->term, subs->lexpr->term) )
+         {
+           // use the other term
+           constraint new;
+           new = constraint_copy (subs);
+           new = solveforOther(new);
+           oldterm = new->expr->term;
+           replacement = new->lexpr;
+         }
+      }
+
+    c->lexpr = constraintExpr_substituteTerm (c->lexpr, oldterm, replacement);
+    c->expr   = constraintExpr_substituteTerm (c->expr, oldterm, replacement);
+    return c;
 }
 
 constraint substitute (constraint c, constraintList p)
@@ -243,19 +324,18 @@ constraint substitute (constraint c, constraintList p)
     {
       if ( el->ar == EQ)
        if (constraint_hasTerm (c, el->lexpr->term) )
-         //        constraintTerm_same(c->lexpr->term, el->lexpr->term) )
          {
-           {
+             llassert(el->lexpr->expr == NULL);
              DPRINTF((message ("doing substitute for %s", constraint_print (c) ) ) );
-             c = constraint_substituteTerm (c, el->lexpr->term, el->expr); 
+             
+             c = constraint_substituteTerm (c, el); 
              DPRINTF((message ("substituted constraint is now %s", constraint_print (c) ) ) );
              // c->lexpr = constraintExpr_copy (el->expr);
              c = constraint_simplify(c);
              c = constraint_simplify(c);
              c = constraint_simplify(c);
              return c;
-           }
-       }
+         }
     }
   end_constraintList_elements;
 
@@ -282,6 +362,25 @@ constraintList reflectChanges (constraintList pre2, constraintList post1)
     return ret;
 }
 
+bool constraintExpr_containsTerm (constraintExpr p, constraintTerm term)
+{
+  TPRINTF(("constraintExpr_containsTerm"));
+  
+  while (p != NULL)
+    {
+      if (constraintTerm_similar (p->term, term) )
+       return TRUE;
+
+      p = p->expr->expr;
+    }
+  DPRINTF((
+          message ("constraintExpr_hasTerm returned fallse for %s %S",
+                   constraint_print(c), constraintTerm_print(term)
+                   )
+          ));
+  return FALSE;
+}
+
 
 /*check if rvalue side has term*/
 bool constraintExpr_hasTerm (constraint c, constraintTerm term)
@@ -330,16 +429,16 @@ constraintExpr solveEq (constraint c, constraintTerm t)
 
 constraint updateConstraint (constraint c, constraintList p)
 {
-  DPRINTF(("start updateConstraints"));
+  TPRINTF(("start updateConstraints"));
   constraintList_elements (p, el)
     {
       
       if (constraintTerm_same(c->lexpr->term, el->lexpr->term) )
        {
-         DPRINTF((""));
+         TPRINTF((""));
          if ( el->ar == EQ)
            {
-                 TPRINTF((""));
+                 TPRINTF(("j"));
 
              if  (constraintExpr_hasTerm (el, c->lexpr->term) )
                {
@@ -373,7 +472,7 @@ constraintList reflectChangesEnsures (constraintList pre2, constraintList post1)
     {
       if (!resolve (el, post1) )
        {
-         temp = updateConstraint (el, post1);
+         temp = substitute (el, post1);
          if (temp != NULL)
            ret = constraintList_add (ret, temp);
        }
@@ -387,21 +486,30 @@ void mergeResolve (exprNode parent, exprNode child1, exprNode child2)
   constraintList temp;
   DPRINTF( (message ("magically merging constraint into parent:%s for children:  %s and %s", exprNode_unparse (parent), exprNode_unparse (child1), exprNode_unparse(child2) )
            ) );
-  llassert (!exprNode_isError (child1)  || !exprNode_isError(child2) );
-  if (exprNode_isError (child1) )
-      {
-       parent->requiresConstraints = constraintList_copy (child2->requiresConstraints);
-       parent->ensuresConstraints = constraintList_copy (child2->ensuresConstraints);
-       DPRINTF((message ("Copied child constraints: pre: %s and post: %s",
-                         constraintList_print( child2->requiresConstraints),
-                         constraintList_print (child2->ensuresConstraints)
-                         )
-                ));
-       return;
-      }
-
-  llassert(!exprNode_isError(child2) );
-  
+   if (exprNode_isError (child1)  || exprNode_isError(child2) )
+     {
+       if (exprNode_isError (child1) && !exprNode_isError(child2) )
+        {
+          parent->requiresConstraints = constraintList_copy (child2->requiresConstraints);
+          parent->ensuresConstraints = constraintList_copy (child2->ensuresConstraints);
+          DPRINTF((message ("Copied child constraints: pre: %s and post: %s",
+                            constraintList_print( child2->requiresConstraints),
+                            constraintList_print (child2->ensuresConstraints)
+                            )
+                   ));
+          return;
+        }
+       else
+        {
+          llassert(exprNode_isError(child2) );
+          parent->requiresConstraints = constraintList_new();
+          parent->ensuresConstraints = constraintList_new();
+          return;
+        }
+     }
+
+   llassert(!exprNode_isError (child1)  && ! exprNode_isError(child2) );
+   
   DPRINTF( (message ("Child constraints are %s %s and %s %s",
                     constraintList_print (child1->requiresConstraints),
                     constraintList_print (child1->ensuresConstraints),

diff --git a/src/constraintTerm.c b/src/constraintTerm.c
index 471dae77401a498bd6a21ebc79cba1f286454bce..e7f05511ddde20da0850826e728a93a588165960 100644 (file)
--- a/src/constraintTerm.c
+++ b/src/constraintTerm.c
@@ -320,7 +320,7 @@ bool constraintTerm_similar (constraintTerm term1, constraintTerm term2)
       return FALSE;
     }
       
- DPRINTF ( (message
+ TPRINTF ( (message
            ("Comparing srefs for %s and  %s ", constraintTerm_print(term1), constraintTerm_print(term2)
             )
            )
@@ -333,7 +333,7 @@ bool constraintTerm_similar (constraintTerm term1, constraintTerm term2)
    }
  else
    {
-     DPRINTF ((message (" %s and %s are not same", constraintTerm_print(term1), constraintTerm_print(term2)  )  ));
+     TPRINTF ((message (" %s and %s are not same", constraintTerm_print(term1), constraintTerm_print(term2)  )  ));
      return FALSE;
    }