diff options
| author |  stefanheule <unknown> | 2012-02-25 04:04:12 -0800 |
|---|---|---|
| committer | stefanheule <unknown> | 2012-02-25 04:04:12 -0800 |
| commit | 73cb09a2bc90c18325e765e753af3440e137e8de (patch) | |
| tree | 827a3d4d19cb5b28e8f3349b4d0beb70dd81b0b9 /Chalice/src | |
| parent | f5094e7df835e2ea59d93041dfeffcc1f37348a2 (diff) | |
Chalice: fix error introduced by the previous merge.
Diffstat (limited to 'Chalice/src')
| -rw-r--r-- | Chalice/src/main/scala/Translator.scala | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/Chalice/src/main/scala/Translator.scala b/Chalice/src/main/scala/Translator.scala index 7d53dd2b..213fa1c8 100644 --- a/Chalice/src/main/scala/Translator.scala +++ b/Chalice/src/main/scala/Translator.scala @@ -1217,7 +1217,7 @@ class Translator { (for ((v, w) <- duringA zip duringC) yield (new VariableExpr(v) := new VariableExpr(w))) :::
BLocal(m) :: BLocal(sm) ::
(me := absTran.Mask) :: (sme := absTran.SecMask) ::
- absTran.Exhale(s.post, me, absTran.Heap, ErrorMessage(r.pos, "Refinement may fail to satisfy the specification statement post-condition."), false, methodK, false, false) :::
+ absTran.Exhale(me, sme, List((s.post,ErrorMessage(r.pos, "Refinement may fail to satisfy specification statement post-condition."))), "SpecStmt", false, methodK, 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 outside of the frame of the specification statement: " + v.id)),
keepTag)
|