diff options
| author |  stefanheule <unknown> | 2012-02-25 03:23:00 -0800 |
|---|---|---|
| committer | stefanheule <unknown> | 2012-02-25 03:23:00 -0800 |
| commit | a6788b834573f72131f78a2d445ce9c1c4c97f5a (patch) | |
| tree | 2eecd9a4b8994531f0365096e48fb4ed2ceb6c67 /Chalice/src | |
| parent | 2f08c4fe4ca32c0fa2a55dbfa969e1edb269b642 (diff) | |
Chalice: Do not remove permission from the secondary mask during the exhale that takes place during unfold.
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 cd3fb270..a943e923 100644 --- a/Chalice/src/main/scala/Translator.scala +++ b/Chalice/src/main/scala/Translator.scala @@ -2258,7 +2258,7 @@ class ExpressionTranslator(val globals: Globals, preGlobals: Globals, val fpi: F (if (transferPermissionToSecMask) InhalePermission(perm, trE, memberName, currentK, sm)
else Nil) :::
// give up secondary permission to locations of the body of the predicate (also recursively)
- (if (e.isPredicate)
+ (if (e.isPredicate && !transferPermissionToSecMask)
(if (isUpdatingSecMask)
UpdateSecMask(e.predicate, trE, Heap.select(trE, memberName), perm, currentK, recurseOnPredicatesDepth, previousReceivers)
else
|