From 4aa8fe117b03c0cd3781308d9b2c48d7ca9f4aff Mon Sep 17 00:00:00 2001
From: mueller <unknown>
Date: Fri, 25 Jun 2010 18:40:15 +0000
Subject: Chalice: Applied patch #6192

Patches the translation of "assert" statements, so that the meaning of "old" is preserved when the temporary copy of the heap is made for the exhale.
---
 Chalice/src/Translator.scala | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

(limited to 'Chalice')

diff --git a/Chalice/src/Translator.scala b/Chalice/src/Translator.scala
index 72dbf9e4..6b85ed8a 100644
--- a/Chalice/src/Translator.scala
+++ b/Chalice/src/Translator.scala
@@ -301,7 +301,7 @@ class Translator {
         val tmpHeap = Boogie.NewBVar(HeapName, theap, true);
         val tmpMask = Boogie.NewBVar(MaskName, tmask, true); 
         val tmpCredits = Boogie.NewBVar(CreditsName, tcredits, true); 
-        val tmpTranslator = new ExpressionTranslator(List(tmpHeap._1.id, tmpMask._1.id, tmpCredits._1.id), currentClass);
+        val tmpTranslator = new ExpressionTranslator(List(tmpHeap._1.id, tmpMask._1.id, tmpCredits._1.id), List(etran.ChooseEtran(true).Heap, etran.ChooseEtran(true).Mask, etran.ChooseEtran(true).Credits), currentClass);        
         Comment("assert") ::
         // exhale e in a copy of the heap/mask/credits
         BLocal(tmpHeap._1) :: (tmpHeap._2 := VarExpr(HeapName)) ::
-- 
cgit v1.2.3