diff options
| author |  stefanheule <unknown> | 2012-05-20 17:51:24 +0200 |
|---|---|---|
| committer | stefanheule <unknown> | 2012-05-20 17:51:24 +0200 |
| commit | 88cf411f8a95912749c7402d1cddd0b5a3f87e73 (patch) | |
| tree | 70084843af01f1366ae078e94e95bca81bc81359 /Chalice | |
| parent | 6603e01b1b7faf7be5a3cc0b28b39960f56ef029 (diff) | |
Chalice: Remove some old code updating the secondary mask, and add a missing well-formed assumption.
Diffstat (limited to 'Chalice')
| -rw-r--r-- | Chalice/src/main/scala/Translator.scala | 7 |
1 files changed, 2 insertions, 5 deletions
diff --git a/Chalice/src/main/scala/Translator.scala b/Chalice/src/main/scala/Translator.scala index 85ae2ec0..7f500eb9 100644 --- a/Chalice/src/main/scala/Translator.scala +++ b/Chalice/src/main/scala/Translator.scala @@ -1659,15 +1659,12 @@ class ExpressionTranslator(val globals: Globals, preGlobals: Globals, val fpi: F tmpTranslator.ExhaleDuringUnfold(List((acc, ErrorMessage(unfolding.pos, "Unfolding might fail."))), "unfolding", false, unfoldingK, false) :::
// inhale the definition of the predicate
tmpTranslator.Inhale(List(definition), "unfolding", false, unfoldingK) :::
- // remove secondary permissions (if any), and add them again
- (if (isOldEtran) Nil else
- UpdateSecMaskDuringUnfold(pred.predicate, Tr(obj), Heap.select(Tr(obj), pred.predicate.FullName), perm, unfoldingK) :::
- TransferPermissionToSecMask(pred.predicate, obj, perm, unfolding.pos)) :::
// update the predicate mask to indicate the predicates that are folded under 'pred'
(if (isOldEtran) Nil
else etran.keepFoldedLocations(definition, o, pred.predicate, etran.Mask, etran.Heap, etran.fpi.getFoldedPredicates(pred.predicate))) :::
// check definedness of e in state where the predicate is unfolded
- tmpTranslator.isDefined(e)
+ tmpTranslator.isDefined(e) :::
+ bassume(wf(etran.Heap, etran.Mask, etran.SecMask)) :: Nil
// record folded predicate
val version = Heap.select(o, pred.predicate.FullName)
|