diff options
| author |  stefanheule <unknown> | 2012-03-08 02:35:56 -0800 |
|---|---|---|
| committer | stefanheule <unknown> | 2012-03-08 02:35:56 -0800 |
| commit | 589992fa582a62c7fe9e6665ff538d29015c0fc7 (patch) | |
| tree | fe68cda1d46087f65ae4587ffe6cce6dad552d91 | |
| parent | 336eea5a645941e0e183b27706693772eb46f16e (diff) | |
Chalice: Add additional assumption about "held" field for "holds(o)" construction.
| -rw-r--r-- | Chalice/src/main/scala/Translator.scala | 6 |
1 files changed, 4 insertions, 2 deletions
diff --git a/Chalice/src/main/scala/Translator.scala b/Chalice/src/main/scala/Translator.scala index cb77d30f..422120d4 100644 --- a/Chalice/src/main/scala/Translator.scala +++ b/Chalice/src/main/scala/Translator.scala @@ -1737,8 +1737,9 @@ class ExpressionTranslator(val globals: Globals, preGlobals: Globals, val fpi: F case _:PermissionExpr => throw new InternalErrorException("permission expression unexpected here: " + e.pos)
case _:Credit => throw new InternalErrorException("credit expression unexpected here")
case Holds(e) =>
- (0 < Heap.select(trrecursive(e), "held")) &&
- !Heap.select(trrecursive(e), "rdheld")
+ var ee = trrecursive(e)
+ (0 < Heap.select(ee, "held")) &&
+ !Heap.select(ee, "rdheld")
case RdHolds(e) =>
Heap.select(trrecursive(e), "rdheld")
case a: Assigned =>
@@ -2018,6 +2019,7 @@ class ExpressionTranslator(val globals: Globals, preGlobals: Globals, val fpi: F new Boogie.MapSelect(ih, trE, "held")) ::
bassume(0 < new Boogie.MapSelect(ih, trE, "held")) ::
bassume(! new Boogie.MapSelect(ih, trE, "rdheld")) ::
+ bassume(new Boogie.MapSelect(ih, trE, "mu") !=@ bLockBottom) ::
bassume(wf(Heap, Mask, SecMask)) ::
bassume(AreGoodMasks(Mask, SecMask)) ::
bassume(IsGoodState(heapFragment(new Boogie.MapSelect(ih, trE, "held")))) ::
|