diff options
| author |  stefanheule <unknown> | 2012-03-13 03:59:01 -0700 |
|---|---|---|
| committer | stefanheule <unknown> | 2012-03-13 03:59:01 -0700 |
| commit | 217c504e2a8fc9fc8add93b479229855f9f09eb2 (patch) | |
| tree | d4986aa06d14b2a2528823d5b5f46d529cfef7e2 /Chalice/src/main | |
| parent | 18fe46b4cb59101e49a8248471456266ee2c32f8 (diff) | |
Chalice: Fix problem introduced by backing out changeset 622fb6995ea4 (namely, track folded predicates for unfoldings correctly)
Diffstat (limited to 'Chalice/src/main')
| -rw-r--r-- | Chalice/src/main/scala/Translator.scala | 16 |
1 files changed, 11 insertions, 5 deletions
diff --git a/Chalice/src/main/scala/Translator.scala b/Chalice/src/main/scala/Translator.scala index 94232fdd..6bf33230 100644 --- a/Chalice/src/main/scala/Translator.scala +++ b/Chalice/src/main/scala/Translator.scala @@ -1616,18 +1616,18 @@ class ExpressionTranslator(val globals: Globals, preGlobals: Globals, val fpi: F case unfolding@Unfolding(acc@Access(pred@MemberAccess(obj, f), perm), e) =>
val (tmpGlobalsV, tmpGlobals) = this.FreshGlobals("unfolding")
val tmpTranslator = new ExpressionTranslator(tmpGlobals, this.oldEtran.globals, currentClass);
+ val o = Tr(obj)
+ val (flagV, flag) = Boogie.NewBVar("predFlag", tbool, true)
- val receiverOk = isDefined(obj) ::: prove(nonNull(Tr(obj)), obj.pos, "Receiver might be null.");
+ val receiverOk = isDefined(obj) ::: prove(nonNull(o), obj.pos, "Receiver might be null.");
val definition = scaleExpressionByPermission(SubstThis(DefinitionOf(pred.predicate), obj), perm, unfolding.pos)
// pick new k
val (unfoldingKV, unfoldingK) = Boogie.NewBVar("unfoldingK", tint, true)
- // record folded predicate
- etran.fpi.addFoldedPredicate()
-
- Comment("unfolding") ::
+ val res = Comment("unfolding") ::
BLocal(unfoldingKV) :: bassume(0 < unfoldingK && 1000*unfoldingK < percentPermission(1)) ::
+ BLocal(flagV) :: (flag := true) ::
// check definedness
receiverOk ::: isDefined(perm) :::
// copy state into temporary variables
@@ -1642,6 +1642,12 @@ class ExpressionTranslator(val globals: Globals, preGlobals: Globals, val fpi: F TransferPermissionToSecMask(pred.predicate, obj, perm, unfolding.pos) :::
// check definedness of e in state where the predicate is unfolded
tmpTranslator.isDefined(e)
+
+ // record folded predicate
+ val version = etran.Heap.select(o, pred.predicate.FullName)
+ etran.fpi.addFoldedPredicate(FoldedPredicate(pred.predicate, o, version, etran.fpi.currentConditions, flag))
+
+ res
case Iff(e0,e1) =>
isDefined(e0) ::: isDefined(e1)
case Implies(e0,e1) =>
|