diff options
| author |  stefanheule <unknown> | 2012-03-08 02:34:41 -0800 |
|---|---|---|
| committer | stefanheule <unknown> | 2012-03-08 02:34:41 -0800 |
| commit | 336eea5a645941e0e183b27706693772eb46f16e (patch) | |
| tree | fb92d54ac56e25053a04a204a36738a7d5991634 /Chalice/src | |
| parent | cce07f4f4362eee9ab7fcf2e9e311021ae2f4e1f (diff) | |
Chalice: Fix problem with "held" ghost field, which is managed without permissions and its value should be preserved across heap havocs.
Diffstat (limited to 'Chalice/src')
| -rw-r--r-- | Chalice/src/main/scala/Prelude.scala | 1 |
1 files changed, 1 insertions, 0 deletions
diff --git a/Chalice/src/main/scala/Prelude.scala b/Chalice/src/main/scala/Prelude.scala index f78ebe1b..721b0131 100644 --- a/Chalice/src/main/scala/Prelude.scala +++ b/Chalice/src/main/scala/Prelude.scala @@ -199,6 +199,7 @@ function IsGoodExhaleState(eh: HeapType, h: HeapType, (forall o: ref :: { h[o, held] } (0<h[o, held]) ==> eh[o, mu] == h[o, mu]) &&
(forall o: ref :: { h[o, rdheld] } h[o, rdheld] ==> eh[o, mu] == h[o, mu]) &&
(forall o: ref :: { h[o, forkK] } { eh[o, forkK] } h[o, forkK] == eh[o, forkK]) &&
+ (forall o: ref :: { h[o, held] } { eh[o, held] } h[o, held] == eh[o, held]) &&
(forall o: ref, f: Field int :: { eh[o, f], PredicateField(f) } PredicateField(f) ==> h[o, f] <= eh[o, f])
}"""
}
|