Backed out changeset: 2945d608ce60 (the change appears to perform worse in that verification now takes longer).

1 files changed, 5 insertions, 5 deletions

diff --git a/Chalice/src/main/scala/Translator.scala b/Chalice/src/main/scala/Translator.scala
index 1567a209..67649df5 100644
--- a/Chalice/src/main/scala/Translator.scala
+++ b/Chalice/src/main/scala/Translator.scala
@@ -2238,18 +2238,18 @@ class ExpressionTranslator(val globals: Globals, preGlobals: Globals, val fpi: F
     val foldedPredicates = etran.fpi.getFoldedPredicates()

     (for (fp <- foldedPredicates) yield {

       val allButCurrentPredicate = foldedPredicates filter (a => a != fp)

-      restoreFoldedLocationsHelperPred(fp.predicate, fp.receiver, fp.version, mask, heap, exhaleHeap, allButCurrentPredicate, unconditional = false)

+      restoreFoldedLocationsHelperPred(fp.predicate, fp.receiver, mask, heap, exhaleHeap, allButCurrentPredicate, unconditional = false)

     }) flatten

   }

   

   /** copy all the values of locations that are folded (one or more levels down) under the predicate 'pred' from the 'heap' to 'exhaleHeap'. If 'unconditional' is false, then the statements are guarded by the condition that permission to 'receiver.pred' is available in 'mask'. */

-  def restoreFoldedLocationsHelperPred(pred: Predicate, receiver: Expr, version: Expr, mask: Expr, heap: Boogie.Expr, exhaleHeap: Boogie.Expr, otherPredicates: List[FoldedPredicate], unconditional: Boolean = false): List[Boogie.Stmt] = {

+  def restoreFoldedLocationsHelperPred(pred: Predicate, receiver: Expr, mask: Expr, heap: Boogie.Expr, exhaleHeap: Boogie.Expr, otherPredicates: List[FoldedPredicate], unconditional: Boolean = false): List[Boogie.Stmt] = {

     val definition = SubstThis(DefinitionOf(pred), BoogieExpr(receiver))

     val stmts = restoreFoldedLocationsHelper(definition, mask, heap, exhaleHeap, otherPredicates)

     if (unconditional)

       stmts

     else

-      Boogie.If(CanRead(receiver, pred.FullName, mask, ZeroMask) && version ==@ heap.select(receiver, pred.FullName), stmts, Nil)

+      Boogie.If(CanRead(receiver, pred.FullName, mask, ZeroMask), stmts, Nil)

   }

   

   def restoreFoldedLocationsHelper(expr: Expression, mask: Expr, heap: Boogie.Expr, exhaleHeap: Boogie.Expr, otherPredicates: List[FoldedPredicate]): List[Boogie.Stmt] = {

@@ -2270,8 +2270,8 @@ class ExpressionTranslator(val globals: Globals, preGlobals: Globals, val fpi: F
           // check for recursively nested things

           (for (fp <- otherPredicates) yield {

             val allButCurrentPredicate = otherPredicates filter (a => a != fp)

-            Boogie.If(fp.receiver ==@ trE && fp.version ==@ heap.select(trE, fp.predicate.FullName),

-              restoreFoldedLocationsHelperPred(fp.predicate, fp.receiver, fp.version, mask, heap, exhaleHeap, allButCurrentPredicate, unconditional = true),

+            Boogie.If(fp.receiver ==@ trE,

+              restoreFoldedLocationsHelperPred(fp.predicate, fp.receiver, mask, heap, exhaleHeap, allButCurrentPredicate, unconditional = true),

               Nil)

           })

         } else Nil) :::