diff options
| author |  stefanheule <unknown> | 2012-03-11 15:55:35 -0700 |
|---|---|---|
| committer | stefanheule <unknown> | 2012-03-11 15:55:35 -0700 |
| commit | 69c2322de145868daba6aba5277e8a571768e9d7 (patch) | |
| tree | 5cda3dca9643cedcee331b55d8e707b5768b0b87 /Chalice/src/main | |
| parent | 479cc5d0843bdd7b4c5240cdf49ea69af80777db (diff) | |
Chalice: Fix treatment of 'unfolding' w.r.t. secondary permissions.
Diffstat (limited to 'Chalice/src/main')
| -rw-r--r-- | Chalice/src/main/scala/Translator.scala | 13 |
1 files changed, 11 insertions, 2 deletions
diff --git a/Chalice/src/main/scala/Translator.scala b/Chalice/src/main/scala/Translator.scala index af241ed5..9f5e6497 100644 --- a/Chalice/src/main/scala/Translator.scala +++ b/Chalice/src/main/scala/Translator.scala @@ -1612,6 +1612,9 @@ class ExpressionTranslator(val globals: Globals, preGlobals: Globals, val fpi: F // pick new k
val (unfoldingKV, unfoldingK) = Boogie.NewBVar("unfoldingK", tint, true)
+ // record folded predicate
+ etran.fpi.addFoldedPredicate()
+
Comment("unfolding") ::
BLocal(unfoldingKV) :: bassume(0 < unfoldingK && 1000*unfoldingK < percentPermission(1)) ::
// check definedness
@@ -1623,6 +1626,9 @@ 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
+ etran.UpdateSecMaskDuringUnfold(pred.predicate, Tr(obj), etran.Heap.select(Tr(obj), pred.predicate.FullName), perm, unfoldingK) :::
+ TransferPermissionToSecMask(pred.predicate, obj, perm, unfolding.pos) :::
// check definedness of e in state where the predicate is unfolded
tmpTranslator.isDefined(e)
case Iff(e0,e1) =>
@@ -2048,8 +2054,11 @@ class ExpressionTranslator(val globals: Globals, preGlobals: Globals, val fpi: F BLocal(flagV) :: (flag := true) ::
functionTrigger(o, pred.predicate) ::
BLocal(versionV) :: (version := etran.Heap.select(o, pred.predicate.FullName)) ::
- (if(check) isDefined(uf)(true) else Nil) :::
- TransferPermissionToSecMask(pred.predicate, BoogieExpr(receiver), perm, uf.pos) :::
+ (if(check) isDefined(uf)(true) else
+ // remove secondary permissions (if any), and add them again
+ etran.UpdateSecMaskDuringUnfold(pred.predicate, o, etran.Heap.select(o, pred.predicate.FullName), perm, currentK) :::
+ TransferPermissionToSecMask(pred.predicate, BoogieExpr(receiver), perm, uf.pos)
+ ) :::
bassume(Tr(uf))
// record folded predicate
|