Chalice: Changed definition of waitlevel to take into account rdlock. Adapted definition of IsGoodInhaleState and an axiom.

1 files changed, 3 insertions, 2 deletions

diff --git a/Chalice/src/Prelude.scala b/Chalice/src/Prelude.scala
index 3dcc0ccb..2fb58697 100644
--- a/Chalice/src/Prelude.scala
+++ b/Chalice/src/Prelude.scala
@@ -97,7 +97,8 @@ function IsGoodInhaleState(ih: HeapType, h: HeapType,
   (forall<T> o: ref, f: Field T :: { ih[o, f] }  CanRead(m, o, f) ==> ih[o, f] == h[o, f]) &&

   (forall o: ref :: { ih[o, held] }  (0<ih[o, held]) == (0<h[o, held])) &&

   (forall o: ref :: { ih[o, rdheld] }  ih[o, rdheld] == h[o, rdheld]) &&

-  (forall o: ref :: { h[o, held] }  (0<h[o, held]) ==> ih[o, mu] == h[o, mu])

+  (forall o: ref :: { h[o, held] }  (0<h[o, held]) ==> ih[o, mu] == h[o, mu]) &&

+  (forall o: ref :: { h[o, rdheld] }  h[o, rdheld] ==> ih[o, mu] == h[o, mu])

 }

 

 function ite<T>(bool, T, T) returns (T);

@@ -199,7 +200,7 @@ function Seq#Range(min: int, max: int) returns (Seq int);
 axiom (forall min: int, max: int :: { Seq#Length(Seq#Range(min, max)) } (min < max ==> Seq#Length(Seq#Range(min, max)) == max-min) && (max <= min ==> Seq#Length(Seq#Range(min, max)) == 0));

 axiom (forall min: int, max: int, j: int :: { Seq#Index(Seq#Range(min, max), j) } 0<=j && j<max-min ==> Seq#Index(Seq#Range(min, max), j) == min + j);

 

-axiom (forall h: HeapType, m: MaskType, o: ref, q: ref :: {wf(h, m), h[o, mu], h[q, mu]} wf(h, m) && o!=q && (0 < h[o, held]) && (0 < h[q, held]) ==> h[o, mu] != h[q, mu]);

+axiom (forall h: HeapType, m: MaskType, o: ref, q: ref :: {wf(h, m), h[o, mu], h[q, mu]} wf(h, m) && o!=q && (0 < h[o, held] || h[o, rdheld]) && (0 < h[q, held] || h[q, rdheld]) ==> h[o, mu] != h[q, mu]);

 

 function DecPerm<T>(m: MaskType, o: ref, f: Field T, howMuch: int) returns (MaskType);