diff options
| author |  stefanheule <unknown> | 2011-07-05 15:43:19 +0200 |
|---|---|---|
| committer | stefanheule <unknown> | 2011-07-05 15:43:19 +0200 |
| commit | d786b753f39294f4e2d5f57d16c69bb450abc799 (patch) | |
| tree | 622494df73ab7f2ca872b948791f89fed2b856ab | |
| parent | c57c5cf1a3e200ce59d01fcc7b9764074e4d8ebb (diff) | |
Chalice: fix workitem 8236 (lockchange on return values causes invalid Boogie code).
| -rw-r--r-- | Chalice/src/Translator.scala | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/Chalice/src/Translator.scala b/Chalice/src/Translator.scala index 5e9943a0..b1aaeea9 100644 --- a/Chalice/src/Translator.scala +++ b/Chalice/src/Translator.scala @@ -969,7 +969,7 @@ class Translator { // havoc formal outs
(for (v <- formalOuts) yield Havoc(v)) :::
// havoc lockchanges
- LockHavoc(for (e <- LockChanges(c.m.Spec) map (p => SubstVars(p, formalThis, c.m.Ins, formalIns))) yield etran.Tr(e), postEtran) :::
+ LockHavoc(for (e <- LockChanges(c.m.Spec) map (p => SubstVars(p, formalThis, c.m.Ins ++ c.m.Outs, formalIns ++ formalOuts))) yield etran.Tr(e), postEtran) :::
// inhale postconditions (using the state before the call as the "old" state)
postEtran.Inhale(Postconditions(c.m.Spec) map
(p => SubstVars(p, formalThis, c.m.Ins ++ c.m.Outs, formalIns ++ formalOuts)) , "postcondition", false, methodCallK) :::
|