diff options
| -rw-r--r-- | Chalice/src/main/scala/Translator.scala | 17 |
1 files changed, 9 insertions, 8 deletions
diff --git a/Chalice/src/main/scala/Translator.scala b/Chalice/src/main/scala/Translator.scala index dd5e02e2..f736c65a 100644 --- a/Chalice/src/main/scala/Translator.scala +++ b/Chalice/src/main/scala/Translator.scala @@ -2215,6 +2215,15 @@ class ExpressionTranslator(val globals: Globals, preGlobals: Globals, val fpi: F // transfer permission to secondary mask if necessary
(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 (isUpdatingSecMask)
+ UpdateSecMask(e.predicate, trE, Heap.select(trE, memberName), perm, currentK, recurseOnPredicatesDepth, previousReceivers)
+ else
+ UpdateSecMask(e.predicate, trE, Heap.select(trE, memberName), perm, currentK)
+ )
+ else Nil) :::
+ // update version number (if necessary)
(if (e.isPredicate && !isUpdatingSecMask)
Boogie.If(!CanRead(trE, memberName, m, sm), // if we cannot access the predicate anymore, then its version will be havoced
(if (!duringUnfold) bassume(Heap.select(trE, memberName) < eh.select(trE, memberName)) :: Nil // assume that the predicate's version grows monotonically
@@ -2227,14 +2236,6 @@ class ExpressionTranslator(val globals: Globals, preGlobals: Globals, val fpi: F }),
Nil) :: Nil
else Nil) :::
- // give up secondary permission to locations of the body of the predicate (also recursively)
- (if (e.isPredicate)
- (if (isUpdatingSecMask)
- UpdateSecMask(e.predicate, trE, Heap.select(trE, memberName), perm, currentK, recurseOnPredicatesDepth, previousReceivers)
- else
- UpdateSecMask(e.predicate, trE, Heap.select(trE, memberName), perm, currentK)
- )
- else Nil) :::
bassume(AreGoodMasks(m, sm)) ::
bassume(wf(Heap, m, sm))
}
|