diff options
| author |  stefanheule <unknown> | 2012-02-25 03:12:13 -0800 |
|---|---|---|
| committer | stefanheule <unknown> | 2012-02-25 03:12:13 -0800 |
| commit | c62d74275f293df40e7e73adb1a77f1950c288db (patch) | |
| tree | 6814e643c3155524f9f4ff2f254524158183a521 /Chalice/src/main | |
| parent | f70084b6b9990f3ff52dd080c40c8630906f3bf7 (diff) | |
Chalice: preserve some information about versions to predicates for which we do not have access.
Diffstat (limited to 'Chalice/src/main')
| -rw-r--r-- | Chalice/src/main/scala/Prelude.scala | 3 |
1 files changed, 2 insertions, 1 deletions
diff --git a/Chalice/src/main/scala/Prelude.scala b/Chalice/src/main/scala/Prelude.scala index 0aa9958e..11d78a4e 100644 --- a/Chalice/src/main/scala/Prelude.scala +++ b/Chalice/src/main/scala/Prelude.scala @@ -198,7 +198,8 @@ function IsGoodExhaleState(eh: HeapType, h: HeapType, (forall o: ref :: { eh[o, rdheld] } eh[o, rdheld] == h[o, rdheld]) &&
(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, forkK] } { eh[o, forkK] } h[o, forkK] == eh[o, forkK]) &&
+ (forall<T> o: ref, f: Field int :: { eh[o, f], PredicateField(f) } PredicateField(f) ==> h[o, f] <= eh[o, f])
}"""
}
object PermissionFunctionsAndAxiomsPL extends PreludeComponent {
|