diff options
| author |  kyessenov <unknown> | 2010-07-22 03:30:30 +0000 |
|---|---|---|
| committer | kyessenov <unknown> | 2010-07-22 03:30:30 +0000 |
| commit | 8d4941a93f581250da6a6d170a5f8e4cf8aec9ea (patch) | |
| tree | 95bd33377eb82c140e7fc8b2cc170d0c0a7652f3 /Chalice | |
| parent | 765d1a6621452672962626a8253c1092025c703e (diff) | |
Chalice: bug -- permissions were implicity converted to Booge expressions (due to "implicit def")
Diffstat (limited to 'Chalice')
| -rw-r--r-- | Chalice/src/Translator.scala | 4 |
1 files changed, 2 insertions, 2 deletions
diff --git a/Chalice/src/Translator.scala b/Chalice/src/Translator.scala index 0690cffa..0e6e4590 100644 --- a/Chalice/src/Translator.scala +++ b/Chalice/src/Translator.scala @@ -1753,10 +1753,10 @@ class ExpressionTranslator(globals: List[Boogie.Expr], preGlobals: List[Boogie.E val mn = em(ref, memberName)("perm$N");
bassert((FunctionApp("Seq#Contains", List(e, ref)) ==>
- perm match {
+ (perm match {
case _: Read => mr ==@ 0 ==> n <= mn
case _: Write => r <= mr && (r ==@ mr ==> 0 <= mn)
- }).forall(refV), error.pos, error.message + " Insufficient permissions") ::
+ })).forall(refV), error.pos, error.message + " Insufficient permissions") ::
(em := Lambda(List(aV), List(refV, fV),
(FunctionApp("Seq#Contains", List(e, ref)) && f ==@ memberName).thenElse(
Lambda(List(), List(pcV), (pc ==@ "perm$R").thenElse(mr - r, mn - n)),
|