diff options
author | stefanheule <unknown> | 2012-02-25 03:23:16 -0800 |
---|---|---|
committer | stefanheule <unknown> | 2012-02-25 03:23:16 -0800 |
commit | 8e2a3b7af5d7781a055b35f52e4decc0fe940e1e (patch) | |
tree | 00b23b6d352b302da3bc0e960a7c330801149cce /Chalice/src/main/scala/Translator.scala | |
parent | db95796499d3ec21c690679b39449d83c0f295fe (diff) |
Chalice: Add function trigger for unfold and unfolding.
Diffstat (limited to 'Chalice/src/main/scala/Translator.scala')
-rw-r--r-- | Chalice/src/main/scala/Translator.scala | 2 |
1 files changed, 2 insertions, 0 deletions
diff --git a/Chalice/src/main/scala/Translator.scala b/Chalice/src/main/scala/Translator.scala index 213a361b..add4fafb 100644 --- a/Chalice/src/main/scala/Translator.scala +++ b/Chalice/src/main/scala/Translator.scala @@ -715,6 +715,7 @@ class Translator { // pick new k
val (unfoldKV, unfoldK) = Boogie.NewBVar("unfoldK", tint, true)
Comment("unfold") ::
+ functionTrigger(o, pred.predicate) ::
BLocal(unfoldKV) :: bassume(0 < unfoldK && unfoldK < percentPermission(1) && 1000*unfoldK < methodK) ::
isDefined(e) :::
bassert(nonNull(o), s.pos, "The target of the fold statement might be null.") ::
@@ -2051,6 +2052,7 @@ class ExpressionTranslator(val globals: Globals, preGlobals: Globals, val fpi: F val o = TrExpr(obj);
val stmts = BLocal(receiverV) :: (receiver := o) ::
+ 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) :::
|