From 65da7c1240c91692ae873dda6a1138887ae7d41a Mon Sep 17 00:00:00 2001
From: kyessenov <unknown>
Date: Mon, 23 Aug 2010 22:27:06 +0000
Subject: Chalice: exhale spec statement post condition in refinement block
 translation; tag global coupling assertions (bug fix)

---
 Chalice/refinements/Counter.chalice | 12 +++++++++++-
 Chalice/src/Translator.scala        | 12 +++++++++---
 2 files changed, 20 insertions(+), 4 deletions(-)

(limited to 'Chalice')

diff --git a/Chalice/refinements/Counter.chalice b/Chalice/refinements/Counter.chalice
index 16cd8473..f2184a2d 100644
--- a/Chalice/refinements/Counter.chalice
+++ b/Chalice/refinements/Counter.chalice
@@ -49,7 +49,12 @@ class Counter1 refines Counter0 {
   refines dec() 
   {
     this.z := this.z + 1;
-  }       
+  }      
+
+  refines magic() returns (c: Cell)
+  {
+    c := new Cell;
+  } 
 }
 
 class Cell {var n: int}
@@ -82,6 +87,11 @@ class Counter2 refines Counter0 {
   {
     this.b.n := this.b.n + 1;
   }
+
+  refines magic() returns (c: Cell)
+  {
+    c := a;
+  }
 }
 
 class Client {
diff --git a/Chalice/src/Translator.scala b/Chalice/src/Translator.scala
index 0c23db04..2ab7f668 100644
--- a/Chalice/src/Translator.scala
+++ b/Chalice/src/Translator.scala
@@ -1086,11 +1086,15 @@ class Translator {
     { etran = absTran;
     r.abs match {
       case List(s: SpecStmt) =>
+        var (m, me) = NewBVar("specMask", tmask, true)
+
         tag(
           Comment("give witnesses to declared local variables") ::
           (for (v <- duringA) yield BLocal(Variable2BVarWhere(v))) :::
           (for ((v, w) <- duringA zip duringC) yield (new VariableExpr(v) := new VariableExpr(w))) :::
-          bassert(s.post, r.pos, "Refinement may fail to satisfy specification statement post-condition") ::
+          BLocal(m) ::
+          (me := absTran.Mask) ::
+          absTran.Exhale(s.post, me, absTran.Heap, ErrorMessage(r.pos, "Refinement may fail to satisfy specification statement post-condition."), false) :::
           (for ((v, w) <- beforeV zip before; if (! s.lhs.exists(ve => ve.v == w))) yield
              bassert(new VariableExpr(v) ==@ new VariableExpr(w), r.pos, "Refinement may change a variable not in frame of the specification statement: " + v.id)),
           keepTag)
@@ -1127,8 +1131,10 @@ class Translator {
         yield Boogie.If((ci.fields.map(f => absTran.CanRead(new VarExpr("this"), f.FullName)).reduceLeft(_ || _)),
           copy(ci.e), Nil)) :::
       // assert equality on shared globals (except those that are replaced)
-      (for (f <- currentClass.refines.Fields; if ! currentClass.CouplingInvariants.exists(_.fields.contains(f)))
-        yield bassert((absTran.Heap.select(ve, f.FullName) ==@ conTran.Heap.select(ve, f.FullName)).forall(v), r.pos, "Refinement may change value of field " + f.FullName)) 
+      tag(
+        for (f <- currentClass.refines.Fields; if ! currentClass.CouplingInvariants.exists(_.fields.contains(f)))
+          yield bassert((absTran.Heap.select(ve, f.FullName) ==@ conTran.Heap.select(ve, f.FullName)).forall(v), r.pos, "Refinement may change value of field " + f.FullName),
+        keepTag)            
     } :::
     Comment("end of refinement block")
   }
-- 
cgit v1.2.3