diff options
author | kyessenov <unknown> | 2010-08-23 22:27:06 +0000 |
---|---|---|
committer | kyessenov <unknown> | 2010-08-23 22:27:06 +0000 |
commit | 65da7c1240c91692ae873dda6a1138887ae7d41a (patch) | |
tree | e5eaf3d60f7c59060b7467ffe76c23e6643b00b0 /Chalice | |
parent | 5c779b7e1542cdedccf00ba0cd056d6de6435d6c (diff) |
Chalice: exhale spec statement post condition in refinement block translation; tag global coupling assertions (bug fix)
Diffstat (limited to 'Chalice')
-rw-r--r-- | Chalice/refinements/Counter.chalice | 12 | ||||
-rw-r--r-- | Chalice/src/Translator.scala | 12 |
2 files changed, 20 insertions, 4 deletions
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")
}
|