Chalice: fix workitem 10194 (unfolding and old-expressions).

1 files changed, 8 insertions, 8 deletions

diff --git a/Chalice/src/Translator.scala b/Chalice/src/Translator.scala
index 1718a29f..ea05d4bc 100644
--- a/Chalice/src/Translator.scala
+++ b/Chalice/src/Translator.scala
@@ -1449,7 +1449,7 @@ class ExpressionTranslator(globals: List[Boogie.Expr], preGlobals: List[Boogie.E
         val (tmpHeapV, tmpHeap) = Boogie.NewBVar("Heap", theap, true);

         val (tmpMaskV, tmpMask) = Boogie.NewBVar("Mask", tmask, true); 

         val (tmpCreditsV, tmpCredits) = Boogie.NewBVar("Credits", tcredits, true); 

-        val tmpTranslator = new ExpressionTranslator(List(tmpHeap,tmpMask,tmpCredits), currentClass);

+        val tmpTranslator = new ExpressionTranslator(List(tmpHeap,tmpMask,tmpCredits), etran.oldEtran.Globals, currentClass);

         

         // pick new k

         val (funcappKV, funcappK) = Boogie.NewBVar("funcappK", tint, true)

@@ -1475,7 +1475,7 @@ class ExpressionTranslator(globals: List[Boogie.Expr], preGlobals: List[Boogie.E
         val (tmpHeapV, tmpHeap) = Boogie.NewBVar("Heap", theap, true);

         val (tmpMaskV, tmpMask) = Boogie.NewBVar("Mask", tmask, true);

         val (tmpCreditsV, tmpCredits) = Boogie.NewBVar("Credits", tcredits, true);

-        val tmpTranslator = new ExpressionTranslator(List(tmpHeap, tmpMask, tmpCredits), currentClass);

+        val tmpTranslator = new ExpressionTranslator(List(tmpHeap, tmpMask, tmpCredits), etran.oldEtran.Globals, currentClass);

         

         val receiverOk = isDefined(obj) ::: prove(nonNull(Tr(obj)), obj.pos, "Receiver might be null.");

         val definition = scaleExpressionByPermission(SubstThis(DefinitionOf(pred.predicate), obj), perm, unfolding.pos)

@@ -1549,7 +1549,7 @@ class ExpressionTranslator(globals: List[Boogie.Expr], preGlobals: List[Boogie.E
         isDefined(e0) ::: isDefined(e1)

       case Eval(h, e) =>

         val (evalHeap, evalMask, evalCredits, checks, assumptions) = fromEvalState(h);

-        val evalEtran = new ExpressionTranslator(List(evalHeap, evalMask, evalCredits), currentClass);

+        val evalEtran = new ExpressionTranslator(List(evalHeap, evalMask, evalCredits), etran.oldEtran.Globals, currentClass);

         evalEtran.isDefined(e)

       case _ : SeqQuantification => throw new InternalErrorException("should be desugared")

       case tq @ TypeQuantification(_, _, _, e, (min, max)) =>

@@ -1675,7 +1675,7 @@ class ExpressionTranslator(globals: List[Boogie.Expr], preGlobals: List[Boogie.E
     case Contains(e0, e1) => SeqContains(Tr(e1), Tr(e0))

     case Eval(h, e) =>

       val (evalHeap, evalMask, evalCredits, checks, assumptions) = fromEvalState(h);

-      val evalEtran = new ExpressionTranslator(List(evalHeap, evalMask, evalCredits), currentClass);

+      val evalEtran = new ExpressionTranslator(List(evalHeap, evalMask, evalCredits), etran.oldEtran.Globals, currentClass);

       evalEtran.Tr(e)

     case _:SeqQuantification => throw new InternalErrorException("should be desugared")

     case tq @ TypeQuantification(Forall, _, _, e, _) =>

@@ -1746,10 +1746,10 @@ class ExpressionTranslator(globals: List[Boogie.Expr], preGlobals: List[Boogie.E
   }

 

   def Inhale(p: Expression, ih: Boogie.Expr, check: Boolean, currentK: Expr): List[Boogie.Stmt] = desugar(p) match {

-    case pred@MemberAccess(e, p) if pred.isPredicate => 
-      val chk = (if (check) {
-        isDefined(e)(true) ::: 
-        bassert(nonNull(Tr(e)), e.pos, "Receiver might be null.") :: Nil
+    case pred@MemberAccess(e, p) if pred.isPredicate => 

+      val chk = (if (check) {

+        isDefined(e)(true) ::: 

+        bassert(nonNull(Tr(e)), e.pos, "Receiver might be null.") :: Nil

       } else Nil)

       val tmp = Access(pred, Full);

       tmp.pos = pred.pos;