diff options
| author |  stefanheule <unknown> | 2012-02-25 03:15:20 -0800 |
|---|---|---|
| committer | stefanheule <unknown> | 2012-02-25 03:15:20 -0800 |
| commit | 5ab16929977cc99aaef92e79a9f1f367d8a3c7f4 (patch) | |
| tree | d83222d6feeac45d72aeb0cc598a69eb96766dc2 /Chalice/src | |
| parent | 5c7a3486155078ac12e4e831f0cd7e6b779eff60 (diff) | |
Chalice: correctly introduce a temporary secondary mask
Diffstat (limited to 'Chalice/src')
| -rw-r--r-- | Chalice/src/main/scala/Translator.scala | 13 |
1 files changed, 8 insertions, 5 deletions
diff --git a/Chalice/src/main/scala/Translator.scala b/Chalice/src/main/scala/Translator.scala index c8172e05..112c376f 100644 --- a/Chalice/src/main/scala/Translator.scala +++ b/Chalice/src/main/scala/Translator.scala @@ -2042,14 +2042,17 @@ class ExpressionTranslator(val globals: Globals, preGlobals: Globals, val fpi: F assert ((isUpdatingSecMask && recurseOnPredicatesDepth >= 0) || (!isUpdatingSecMask && recurseOnPredicatesDepth == -1)) // check assumption 2
if (predicates.size == 0) return Nil;
val (ehV, eh) = Boogie.NewBVar("exhaleHeap", theap, true)
- val (emV, em) = Boogie.NewBVar("exhaleMask", tmask, true)
+ var (emV, em: Expr) = Boogie.NewBVar("exhaleMask", tmask, true)
Comment("begin exhale (" + occasion + ")") ::
(if (!isUpdatingSecMask)
- BLocal(emV) :: (em := Mask) ::
+ BLocal(emV) :: (em := m) ::
BLocal(ehV) :: Boogie.Havoc(eh) :: Nil
- else Nil) :::
- (for (p <- predicates) yield ExhaleHelper(p._1, m, sm, eh, p._2, check, currentK, exactchecking, false, transferPermissionToSecMask, recurseOnPredicatesDepth, isUpdatingSecMask)).flatten :::
- (for (p <- predicates) yield ExhaleHelper(p._1, m, sm, eh, p._2, check, currentK, exactchecking, true, transferPermissionToSecMask, recurseOnPredicatesDepth, isUpdatingSecMask)).flatten :::
+ else {
+ em = m
+ Nil
+ }) :::
+ (for (p <- predicates) yield ExhaleHelper(p._1, em, sm, eh, p._2, check, currentK, exactchecking, false, transferPermissionToSecMask, recurseOnPredicatesDepth, isUpdatingSecMask)).flatten :::
+ (for (p <- predicates) yield ExhaleHelper(p._1, em, sm, eh, p._2, check, currentK, exactchecking, true, transferPermissionToSecMask, recurseOnPredicatesDepth, isUpdatingSecMask)).flatten :::
(if (!isUpdatingSecMask)
(m := em) ::
bassume(IsGoodExhaleState(eh, Heap, m, sm)) ::
|