diff options
| author |  mueller <unknown> | 2010-06-09 21:05:40 +0000 |
|---|---|---|
| committer | mueller <unknown> | 2010-06-09 21:05:40 +0000 |
| commit | 0f3d7426f849219350c19119a9ecde285df4351b (patch) | |
| tree | e0269f148fc88e5229e64a653afd2b9c68a2070b | |
| parent | 1e156f9e83cb5ace0f74330f2aa49f8ce09d0afe (diff) | |
Chalice: fixed bug in the exhale of permissions (to handle negative epsilons)
| -rw-r--r-- | Chalice/src/Translator.scala | 6 |
1 files changed, 3 insertions, 3 deletions
diff --git a/Chalice/src/Translator.scala b/Chalice/src/Translator.scala index b89fd91a..72dbf9e4 100644 --- a/Chalice/src/Translator.scala +++ b/Chalice/src/Translator.scala @@ -1792,10 +1792,10 @@ class ExpressionTranslator(globals: List[Boogie.Expr], preGlobals: List[Boogie.E val g = (new Boogie.MapSelect(Mask, obj, field, "perm$N") !=@ Boogie.VarExpr("Permission$MinusInfinity"))
Boogie.If(g, MapUpdate3(Mask, obj, field, "perm$N", Boogie.VarExpr("Permission$PlusInfinity")), Nil)
}
-
def DecPermission(obj: Boogie.Expr, field: String, howMuch: Boogie.Expr, mask: Boogie.Expr, error: ErrorMessage, pos: Position) = {
- val xyz: Boogie.Expr = new Boogie.MapSelect(mask, obj, field, "perm$R")
- bassert(howMuch <= xyz, error.pos, error.message + " Insufficient fraction at " + pos + " for " + field + ".") ::
+ val fP: Boogie.Expr = new Boogie.MapSelect(mask, obj, field, "perm$R")
+ val fC: Boogie.Expr = new Boogie.MapSelect(mask, obj, field, "perm$N")
+ bassert(howMuch <= fP && (howMuch ==@ fP ==> 0 <= fC), error.pos, error.message + " Insufficient fraction at " + pos + " for " + field + ".") ::
MapUpdate3(mask, obj, field, "perm$R", new Boogie.MapSelect(mask, obj, field, "perm$R") - howMuch)
}
def DecPermissionEpsilon(obj: Boogie.Expr, field: String, epsilons: Boogie.Expr, mask: Boogie.Expr, error: ErrorMessage, pos: Position) =
|