Chalice:

* fix bugs -- translateAssert and etran.fromPreGlobals were referring to globals by name instead of using current globals
* example of finding duplicate elements in a sequence using a bitset

1 files changed, 4 insertions, 5 deletions

diff --git a/Chalice/src/Translator.scala b/Chalice/src/Translator.scala
index 2ab7f668..3b6955b1 100644
--- a/Chalice/src/Translator.scala
+++ b/Chalice/src/Translator.scala
@@ -414,9 +414,9 @@ class Translator {
         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)) ::

-        BLocal(tmpMask._1) :: (tmpMask._2 := VarExpr(MaskName)) ::

-        BLocal(tmpCredits._1) :: (tmpCredits._2 := VarExpr(CreditsName)) ::

+        BLocal(tmpHeap._1) :: (tmpHeap._2 := etran.Heap) ::

+        BLocal(tmpMask._1) :: (tmpMask._2 := etran.Mask) ::

+        BLocal(tmpCredits._1) :: (tmpCredits._2 := etran.Credits) ::

         tmpTranslator.Exhale(List((e, ErrorMessage(s.pos, "Assertion might not hold."))), "assert", true)

       case Assume(e) =>

         Comment("assume") ::

@@ -1363,9 +1363,8 @@ class ExpressionTranslator(globals: List[Boogie.Expr], preGlobals: List[Boogie.E
   }

 

   def FromPreGlobals(preGlobals: List[Boogie.BVar]) = {

-    val g = for ((id,t) <- ExpressionTranslator.Globals) yield VarExpr(id)

     val pg = preGlobals map (g => new VarExpr(g))

-    new ExpressionTranslator(g, pg, currentClass, checkTermination)

+    new ExpressionTranslator(globals, pg, currentClass, checkTermination)

   }

 

   def UseCurrentAsOld() = {