Merge

5 files changed, 146 insertions, 173 deletions

diff --git a/Chalice/src/main/scala/Boogie.scala b/Chalice/src/main/scala/Boogie.scala
index 900ad6d1..e775b688 100644
--- a/Chalice/src/main/scala/Boogie.scala
+++ b/Chalice/src/main/scala/Boogie.scala
@@ -66,8 +66,8 @@ object Boogie {
    def +(that: Expr) = BinaryExpr("+", this, that)

    def -(that: Expr) = BinaryExpr("-", this, that)

    def *(that: Expr) = BinaryExpr("*", this, that)

-   def /(that: Expr) = BinaryExpr("/", this, that)

-   def %(that: Expr) = BinaryExpr("%", this, that)

+   def /(that: Expr) = BinaryExpr("div", this, that)

+   def %(that: Expr) = BinaryExpr("mod", this, that)

    def := (that: Expr) = Assign(this, that)

    def apply(e: Expr, f: Expr) = new MapSelect(this, e, Some(f))

    def apply(e: Expr) = new MapSelect(this, e, None)

@@ -78,6 +78,7 @@ object Boogie {
    def store(e: Expr, f: Expr, rhs: Expr) = MapUpdate(this, e, Some(f), rhs)

  }

  case class IntLiteral(n: Int) extends Expr

+ case class RealLiteral(d: Double) extends Expr

  case class BoolLiteral(b: Boolean) extends Expr

  case class Null() extends Expr

  case class VarExpr(id: String) extends Expr {

@@ -252,6 +253,7 @@ object Boogie {
  }

  def PrintExpr(e: Expr, useParens: Boolean): String = e match {

    case IntLiteral(n) => n.toString

+   case RealLiteral(d) => d.toString

    case BoolLiteral(b) => b.toString

    case Null() => "null"

    case VarExpr(id) => id

diff --git a/Chalice/src/main/scala/Chalice.scala b/Chalice/src/main/scala/Chalice.scala
index 2514d6b1..60f5f443 100644
--- a/Chalice/src/main/scala/Chalice.scala
+++ b/Chalice/src/main/scala/Chalice.scala
@@ -34,11 +34,7 @@ object Chalice {
   private[chalice] var skipDeadlockChecks = false: Boolean;

   private[chalice] var skipTermination = false: Boolean;

   private[chalice] var noFreeAssume = false: Boolean;

-  // percentageSupport 0: use multiplication directly

-  // percentageSupport 1: fix Permission$denominator as constant (possibly unsound for small values of the constant?)

-  // percentageSupport 2: use function and provide some (redundant) axioms

-  // percentageSupport 3: use an uninterpreted function and axiomatize the properties of multiplication

-  private[chalice] var percentageSupport = 2;

+  private[chalice] var percentageSupport = 0;

   private[chalice] var smoke = false;

   private[chalice] var smokeAll = false;

   private[chalice] var timingVerbosity = 1;

@@ -147,10 +143,8 @@ object Chalice {
           "level 2: unfold predicates and functions with receiver this in pre and postconditions\n"+

           "level 3 or above: level 2 + autoMagic"),

       "percentageSupport:<n>" -> ("determin how percentage permissions are translated to Boogie\n"+

-          "0: use multiplication directly (can cause performance problems)\n"+

-          "1: fix Permission$denominator as constant (possibly unsound)\n"+

-          "2: use a function and provide some (redundant) axioms\n"+

-          "3: use an uninterpreted function and axiomatize the properties of multiplication"),

+          "0: use multiplication directly (default)\n"+

+          "1: use a function and provide some (redundant) axioms")+

       "boogieOpt:<arg>, /bo:<arg>" -> "specify additional Boogie options"

     )

     lazy val help = {

@@ -178,7 +172,7 @@ object Chalice {
      else if (a.startsWith("/percentageSupport:") || a.startsWith("-percentageSupport:")) {

        try {

          val in = Integer.parseInt(a.substring(19));

-         if (in < 0 || in > 3) CommandLineError("/percentageSupport takes only values 0, 1, 2 or 3", help)

+         if (in < 0 || in > 1) CommandLineError("/percentageSupport takes only values 0 or 1", help)

          else percentageSupport = in

        } catch { case _ => CommandLineError("/percentageSupport takes integer argument", help); }

      }

@@ -214,9 +208,7 @@ object Chalice {
     

     percentageSupport match {

       case 0 => TranslatorPrelude.addComponent(PercentageStandardPL)

-      case 1 => TranslatorPrelude.addComponent(PercentageStandardPL, PercentageFixedDenominatorPL)

-      case 2 => TranslatorPrelude.addComponent(PercentageFunctionPL)

-      case 3 => TranslatorPrelude.addComponent(PercentageUninterpretedFunctionPL)

+      case 1 => TranslatorPrelude.addComponent(PercentageFunctionPL)

     }

 

     // check that input files exist

diff --git a/Chalice/src/main/scala/Prelude.scala b/Chalice/src/main/scala/Prelude.scala
index fc98a36c..4a333f8e 100644
--- a/Chalice/src/main/scala/Prelude.scala
+++ b/Chalice/src/main/scala/Prelude.scala
@@ -33,7 +33,7 @@ object TranslatorPrelude {
   val predicates: Set[Predicate] = Set()

   

   // default components

-  private val components: Set[PreludeComponent] = Set(CopyrightPL, TypesPL, PermissionTypesAndConstantsPL, CreditsAndMuPL, PermissionFunctionsAndAxiomsPL, IfThenElsePL, ArithmeticPL, StringPL)

+  private val components: Set[PreludeComponent] = Set(CopyrightPL, TypesPL, PermissionTypesAndConstantsPL, CreditsAndMuPL, PermissionFunctionsAndAxiomsPL, IfThenElsePL, StringPL)

 

   // get the prelude (with all components currently included)

   def P: String = {

@@ -53,7 +53,7 @@ object TranslatorPrelude {
 sealed abstract class PreludeComponent {

   // determines the order in which the components are output

   def compare(that: PreludeComponent): Boolean = {

-    val order: List[PreludeComponent] = List(CopyrightPL, TypesPL, PermissionTypesAndConstantsPL, PercentageFixedDenominatorPL, PercentageFunctionPL, PercentageUninterpretedFunctionPL, CreditsAndMuPL, PermissionFunctionsAndAxiomsPL, IfThenElsePL, ArithmeticPL, StringPL, AxiomatizationOfSequencesPL)

+    val order: List[PreludeComponent] = List(CopyrightPL, TypesPL, PermissionTypesAndConstantsPL, PercentageFunctionPL, CreditsAndMuPL, PermissionFunctionsAndAxiomsPL, IfThenElsePL, StringPL, AxiomatizationOfSequencesPL)

     if (!order.contains(this)) false

     else order.indexOf(this) < order.indexOf(that)

   }

@@ -67,7 +67,7 @@ object TypesPL extends PreludeComponent {
   val text = """

 type Field a;

 type HeapType = <a>[ref,Field a]a;

-type MaskType = <a>[ref,Field a][PermissionComponent]int;

+type MaskType = <a>[ref,Field a][PermissionComponent]real;

 type PMaskType = <a>[ref,Field a]bool;

 type CreditsType = [ref]int;

 type ref;

@@ -82,65 +82,47 @@ const unique perm$R: PermissionComponent;
 const unique perm$N: PermissionComponent;

 var Mask: MaskType where IsGoodMask(Mask);

 var SecMask: MaskType where IsGoodMask(SecMask);

-const Permission$denominator: int;

-axiom Permission$denominator > 0;

-const Permission$FullFraction: int;

-const Permission$Zero: [PermissionComponent]int;

-axiom Permission$Zero[perm$R] == 0 && Permission$Zero[perm$N] == 0;

-const Permission$Full: [PermissionComponent]int;

-axiom Permission$Full[perm$R] == Permission$FullFraction && Permission$Full[perm$N] == 0;

+const Permission$denominator: real;

+axiom Permission$denominator == 1.0;

+const Permission$FullFraction: real;

+const Permission$Zero: [PermissionComponent]real;

+axiom Permission$Zero[perm$R] == 0.0 && Permission$Zero[perm$N] == 0.0;

+const Permission$Full: [PermissionComponent]real;

+axiom Permission$Full[perm$R] == Permission$FullFraction && Permission$Full[perm$N] == 0.0;

 const ZeroMask: MaskType;

-axiom (forall<T> o: ref, f: Field T, pc: PermissionComponent :: ZeroMask[o,f][pc] == 0);

+axiom (forall<T> o: ref, f: Field T, pc: PermissionComponent :: ZeroMask[o,f][pc] == 0.0);

 const ZeroPMask: PMaskType;

 axiom (forall<T> o: ref, f: Field T :: ZeroPMask[o,f] == false);

 axiom IsGoodMask(ZeroMask);

 const unique joinable: Field int;

 axiom NonPredicateField(joinable);

 const unique token#t: TypeName;

-const unique forkK: Field int;

+const unique forkK: Field real;

 axiom NonPredicateField(forkK);

-const channelK: int;

-const monitorK: int;

-const predicateK: int;"""

+const channelK: real;

+const monitorK: real;

+const predicateK: real;"""

 }

 object PercentageStandardPL extends PreludeComponent {

   val text = """

-axiom (0 < channelK && 1000*channelK < Permission$denominator);

-axiom (0 < monitorK && 1000*monitorK < Permission$denominator);

-axiom (0 < predicateK && 1000*predicateK < Permission$denominator);

-axiom Permission$FullFraction  == 100*Permission$denominator;

+axiom Permission$FullFraction  == 1.0;

+axiom 0.0 < channelK && 1000.0*channelK < 0.01;

+axiom 0.0 < monitorK && 1000.0*monitorK < 0.01;

+axiom 0.0 < predicateK && 1000.0*predicateK < 0.01;

 axiom predicateK == channelK && channelK == monitorK;"""

 }

-object PercentageFixedDenominatorPL extends PreludeComponent {

-  val text = """

-axiom Permission$denominator == 100000000000;"""

-}

 object PercentageFunctionPL extends PreludeComponent {

   val text = """

-function Fractions(n: int) returns (int)

+function Fractions(n: int) returns (real)

 {

-  n * Permission$denominator

+  n / 100.0

 }

-axiom (forall x,y: int :: 0 <= x && x <= y ==> Fractions(x) <= Fractions(y));

-

-axiom Permission$FullFraction  == Fractions(100);

-axiom 0 < channelK && 1000*channelK < Fractions(1);

-axiom 0 < monitorK && 1000*monitorK < Fractions(1);

-axiom 0 < predicateK && 1000*predicateK < Fractions(1);

-axiom predicateK == channelK && channelK == monitorK;"""

-}

-object PercentageUninterpretedFunctionPL extends PreludeComponent {

-  val text = """

-function Fractions(n: int) returns (int);

-function Fractions'(n: int) returns (int);

-axiom (forall x: int :: { Fractions(x) } Fractions(x) == Fractions'(x));

-axiom (forall x,y: int :: 0 <= x && x <= y ==> Fractions'(x) <= Fractions'(y));

-axiom (forall x,y: int :: { Fractions(x), Fractions(y) } Fractions(x) + Fractions(y) == Fractions'(x+y));

+axiom (forall x,y: int :: 0.0 <= real(x) && real(x) <= real(y) ==> Fractions(x) <= Fractions(y));

 

 axiom Permission$FullFraction  == Fractions(100);

-axiom 0 < channelK && 1000*channelK < Fractions(1);

-axiom 0 < monitorK && 1000*monitorK < Fractions(1);

-axiom 0 < predicateK && 1000*predicateK < Fractions(1);

+axiom 0.0 < channelK && 1000.0*channelK < Fractions(1);

+axiom 0.0 < monitorK && 1000.0*monitorK < Fractions(1);

+axiom 0.0 < predicateK && 1000.0*predicateK < Fractions(1);

 axiom predicateK == channelK && channelK == monitorK;"""

 }

 object CreditsAndMuPL extends PreludeComponent {

@@ -232,49 +214,49 @@ object PermissionFunctionsAndAxiomsPL extends PreludeComponent {
 

 function {:expand false} CanRead<T>(m: MaskType, sm: MaskType, obj: ref, f: Field T) returns (bool)

 {

-  0 < m[obj,f][perm$R] || 0 < m[obj,f][perm$N]

+  0.0 < m[obj,f][perm$R] || 0.0 < m[obj,f][perm$N]

 }

 function {:expand false} CanReadForSure<T>(m: MaskType, obj: ref, f: Field T) returns (bool)

 {

-  0 < m[obj,f][perm$R] || 0 < m[obj,f][perm$N]

+  0.0 < m[obj,f][perm$R] || 0.0 < m[obj,f][perm$N]

 }

 function {:expand false} CanWrite<T>(m: MaskType, obj: ref, f: Field T) returns (bool)

 {

-  m[obj,f][perm$R] == Permission$FullFraction && m[obj,f][perm$N] == 0

+  m[obj,f][perm$R] == Permission$FullFraction && m[obj,f][perm$N] == 0.0

 }

 function {:expand true} IsGoodMask(m: MaskType) returns (bool)

 {

   (forall<T> o: ref, f: Field T ::

-      0 <= m[o,f][perm$R] && 

+      0.0 <= m[o,f][perm$R] && 

       (NonPredicateField(f) ==> 

         (m[o,f][perm$R]<=Permission$FullFraction &&

-        (0 < m[o,f][perm$N] ==> m[o,f][perm$R] < Permission$FullFraction))) &&

-      (m[o,f][perm$N] < 0 ==> 0 < m[o,f][perm$R]))

+        (0.0 < m[o,f][perm$N] ==> m[o,f][perm$R] < Permission$FullFraction))) &&

+      (m[o,f][perm$N] < 0.0 ==> 0.0 < m[o,f][perm$R]))

 }

 

 axiom (forall h: HeapType, m, sm: MaskType, o: ref, q: ref :: {wf(h, m, sm), h[o, mu], h[q, mu]} wf(h, m, sm) && 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);

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

 

-axiom (forall<T,U> m: MaskType, o: ref, f: Field T, howMuch: int, q: ref, g: Field U :: {DecPerm(m, o, f, howMuch)[q, g][perm$R]}

+axiom (forall<T,U> m: MaskType, o: ref, f: Field T, howMuch: real, q: ref, g: Field U :: {DecPerm(m, o, f, howMuch)[q, g][perm$R]}

       DecPerm(m, o, f, howMuch)[q, g][perm$R] == ite(o==q && f ==g, m[q, g][perm$R] - howMuch, m[q, g][perm$R])

 );

 

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

+function DecEpsilons<T>(m: MaskType, o: ref, f: Field T, howMuch: real) returns (MaskType);

 

-axiom (forall<T,U> m: MaskType, o: ref, f: Field T, howMuch: int, q: ref, g: Field U :: {DecPerm(m, o, f, howMuch)[q, g][perm$N]}

+axiom (forall<T,U> m: MaskType, o: ref, f: Field T, howMuch: real, q: ref, g: Field U :: {DecPerm(m, o, f, howMuch)[q, g][perm$N]}

          DecEpsilons(m, o, f, howMuch)[q, g][perm$N] == ite(o==q && f ==g, m[q, g][perm$N] - howMuch, m[q, g][perm$N])

 );

 

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

+function IncPerm<T>(m: MaskType, o: ref, f: Field T, howMuch: real) returns (MaskType);

 

-axiom (forall<T,U> m: MaskType, o: ref, f: Field T, howMuch: int, q: ref, g: Field U :: {IncPerm(m, o, f, howMuch)[q, g][perm$R]}

+axiom (forall<T,U> m: MaskType, o: ref, f: Field T, howMuch: real, q: ref, g: Field U :: {IncPerm(m, o, f, howMuch)[q, g][perm$R]}

          IncPerm(m, o, f, howMuch)[q, g][perm$R] == ite(o==q && f ==g, m[q, g][perm$R] + howMuch, m[q, g][perm$R])

 );

 

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

+function IncEpsilons<T>(m: MaskType, o: ref, f: Field T, howMuch: real) returns (MaskType);

 

-axiom (forall<T,U> m: MaskType, o: ref, f: Field T, howMuch: int, q: ref, g: Field U :: {IncPerm(m, o, f, howMuch)[q, g][perm$N]}

+axiom (forall<T,U> m: MaskType, o: ref, f: Field T, howMuch: real, q: ref, g: Field U :: {IncPerm(m, o, f, howMuch)[q, g][perm$N]}

          IncEpsilons(m, o, f, howMuch)[q, g][perm$N] == ite(o==q && f ==g, m[q, g][perm$N] + howMuch, m[q, g][perm$N])

 );

 

@@ -292,7 +274,7 @@ function Call$Args(int) returns (ArgSeq);
 type ArgSeq = <T>[int]T;

 

 function EmptyMask(m: MaskType) returns (bool);

-axiom (forall m: MaskType :: {EmptyMask(m)} EmptyMask(m) <==> (forall<T> o: ref, f: Field T :: NonPredicateField(f) ==> m[o, f][perm$R]<=0 && m[o, f][perm$N]<=0));

+axiom (forall m: MaskType :: {EmptyMask(m)} EmptyMask(m) <==> (forall<T> o: ref, f: Field T :: NonPredicateField(f) ==> m[o, f][perm$R]<=0.0 && m[o, f][perm$N]<=0.0));

 

 const ZeroCredits: CreditsType;

 axiom (forall o: ref :: ZeroCredits[o] == 0);

@@ -330,23 +312,6 @@ function ite<T>(bool, T, T) returns (T);
 axiom (forall<T> con: bool, a: T, b: T :: {ite(con, a, b)} con ==> ite(con, a, b) == a);

 axiom (forall<T> con: bool, a: T, b: T :: {ite(con, a, b)} ! con ==> ite(con, a, b) == b);"""

 }

-object ArithmeticPL extends PreludeComponent {

-  val text = """

-// ---------------------------------------------------------------

-// -- Arithmetic -------------------------------------------------

-// ---------------------------------------------------------------

-

-// the connection between % and /

-axiom (forall x:int, y:int :: {x % y} {x / y}  x % y == x - x / y * y);

-

-// sign of denominator determines sign of remainder

-axiom (forall x:int, y:int :: {x % y}  0 < y  ==>  0 <= x % y  &&  x % y < y);

-axiom (forall x:int, y:int :: {x % y}  y < 0  ==>  y < x % y  &&  x % y <= 0);

-

-// the following axiom has some unfortunate matching, but it does state a property about % that

-// is sometime useful

-axiom (forall a: int, b: int, d: int :: { a % d, b % d } 2 <= d && a % d == b % d && a < b  ==>  a + d <= b);"""

-}

 object StringPL extends PreludeComponent {

   val text = """

 // ---------------------------------------------------------------

diff --git a/Chalice/src/main/scala/Resolver.scala b/Chalice/src/main/scala/Resolver.scala
index 3acd2499..5dc24662 100644
--- a/Chalice/src/main/scala/Resolver.scala
+++ b/Chalice/src/main/scala/Resolver.scala
@@ -260,10 +260,19 @@ object Resolver {
              }

              def hasAccessibilityPredicate(e: Expression) = {

                var b = false

-               e transform {

-                 case _: PermissionExpr => b = true; None

-                 case ma: MemberAccess => if (ma.isPredicate) b = true; None

-                 case _ => None

+               e visitOpt {

+                 case _: PermissionExpr => b = true; false

+                 case ma: MemberAccess => if (ma.isPredicate) { b = true; false } else { true }

+                 case Unfolding(pred, e) => false

+                 case _ => true

+               }

+               b

+             }

+             def hasUnfoldingExpression(e: Expression) = {

+               var b = false

+               e visit {

+                 case Unfolding(pred, e) => b = true

+                 case _ =>

                }

                b

              }

@@ -275,6 +284,8 @@ object Resolver {
                  ResolveExpr(e, context, false, true)(false)

                  if (hasCredit(e)) context.Error(p.pos, "the specification of functions cannot contain credit expressions") 

                  if (hasAccessibilityPredicate(e)) context.Error(p.pos, "the postcondition of functions cannot contain accessibility predicates (permissions are returned automatically)") 

+                 // The following check is necessary, because the postcondition axiom has the limited function as a trigger.  If we were to allow unfolding expressions, then this might introduce a matching loop.  Since we don't know of any cases where one would use an unfolding expression in the postcondition, we forbid it here.

+                 if (hasUnfoldingExpression(e)) context.Error(p.pos, "the postcondition of functions cannot contain unfolding expressions at the moment") 

                case lc : LockChange => context.Error(lc.pos, "lockchange not allowed on function") 

              }

 

diff --git a/Chalice/src/main/scala/Translator.scala b/Chalice/src/main/scala/Translator.scala
index ccdcf57d..60163a1a 100644
--- a/Chalice/src/main/scala/Translator.scala
+++ b/Chalice/src/main/scala/Translator.scala
@@ -79,8 +79,8 @@ class Translator {
   def translateWhereClause(ch: Channel): List[Decl] = {

     

     // pick new k

-    val (whereKV, whereK) = Boogie.NewBVar("whereK", tint, true)

-    val whereKStmts = BLocal(whereKV) :: bassume(0 < whereK && 1000*whereK < permissionOnePercent)

+    val (whereKV, whereK) = Boogie.NewBVar("whereK", treal, true)

+    val whereKStmts = BLocal(whereKV) :: bassume(0.0 < whereK && 1000.0*whereK < permissionOnePercent)

     

     // check definedness of where clause

     Proc(ch.channelId + "$whereClause$checkDefinedness",

@@ -111,8 +111,8 @@ class Translator {
     val (lkV, lk) = NewBVar("lk", tref, true);

     

     // pick new k

-    val (methodKV, methodK) = Boogie.NewBVar("methodK", tint, true)

-    val methodKStmts = BLocal(methodKV) :: bassume(0 < methodK && 1000*methodK < permissionOnePercent)

+    val (methodKV, methodK) = Boogie.NewBVar("methodK", treal, true)

+    val methodKStmts = BLocal(methodKV) :: bassume(0.0 < methodK && 1000.0*methodK < permissionOnePercent)

     

     val oldTranslator = new ExpressionTranslator(Globals(h1, m1, sm1, c1), Globals(h0, m0, sm0, c0), currentClass);

     Proc(currentClass.id + "$monitorinvariant$checkDefinedness",

@@ -164,8 +164,8 @@ class Translator {
     etran = etran.CheckTermination(false);

     

     // pick new k

-    val (functionKV, functionK) = Boogie.NewBVar("functionK", tint, true)

-    val functionKStmts = BLocal(functionKV) :: bassume(0 < functionK && 1000*functionK < permissionOnePercent)

+    val (functionKV, functionK) = Boogie.NewBVar("functionK", treal, true)

+    val functionKStmts = BLocal(functionKV) :: bassume(0.0 < functionK && 1000.0*functionK < permissionOnePercent)

     

     // Boogie function that represents the Chalice function

     {

@@ -389,7 +389,7 @@ class Translator {
     val inArgs = (f.ins map {i => Boogie.VarExpr(i.UniqueName)});

     val myresult = Boogie.BVar("result", f.out.typ);

     val args = VarExpr("this") :: inArgs;

-    val applyF = FunctionApp(functionName(f), List(VarExpr(HeapName)) ::: args)

+    val applyFLimited = FunctionApp(functionName(f)+"#limited", List(VarExpr(HeapName)) ::: args)

     val canCall = FunctionApp(functionName(f) + "#canCall", args)

     val wellformed = wf(VarExpr(HeapName), VarExpr(MaskName), VarExpr(SecMaskName))

     

@@ -397,7 +397,7 @@ class Translator {
     (Postconditions(f.spec) map { post : Expression =>

       Axiom(new Boogie.Forall(

         BVar(HeapName, theap) :: BVar(MaskName, tmask) :: BVar(SecMaskName, tmask) :: BVar("this", tref) :: (f.ins map Variable2BVar),

-        new Trigger(List(applyF, wellformed)),

+        new Trigger(List(applyFLimited, wellformed)),

         (wellformed && (CanAssumeFunctionDefs || f.height < FunctionContextHeight || canCall))

           ==>

         etran.Tr(SubstResult(post, f.apply(ExplicitThisExpr(), f.ins map { arg => new VariableExpr(arg) })))

@@ -408,8 +408,8 @@ class Translator {
   def translatePredicate(pred: Predicate): List[Decl] = {

     

     // pick new k

-    val (predicateKV, predicateK) = Boogie.NewBVar("predicateK", tint, true)

-    val predicateKStmts = BLocal(predicateKV) :: bassume(0 < predicateK && 1000*predicateK < permissionOnePercent)

+    val (predicateKV, predicateK) = Boogie.NewBVar("predicateK", treal, true)

+    val predicateKStmts = BLocal(predicateKV) :: bassume(0.0 < predicateK && 1000.0*predicateK < permissionOnePercent)

     

     // const unique class.name: HeapType;

     Const(pred.FullName, true, FieldType(tint)) ::

@@ -439,8 +439,8 @@ class Translator {
   def translateMethod(method: Method): List[Decl] = {

     

     // pick new k for this method, that represents the fraction for read permissions

-    val (methodKV, methodK) = Boogie.NewBVar("methodK", tint, true)

-    val methodKStmts = BLocal(methodKV) :: bassume(0 < methodK && 1000*methodK < permissionOnePercent)

+    val (methodKV, methodK) = Boogie.NewBVar("methodK", treal, true)

+    val methodKStmts = BLocal(methodKV) :: bassume(0.0 < methodK && 1000.0*methodK < permissionOnePercent)

     

     // check definedness of the method contract

     Proc(method.FullName + "$checkDefinedness", 

@@ -500,8 +500,8 @@ class Translator {
     val postCI = Postconditions(mt.refines.Spec).map(extractInv)

 

     // pick new k for this method, that represents the fraction for read permissions

-    val (methodKV, methodK) = Boogie.NewBVar("methodK", tint, true)

-    val methodKStmts = BLocal(methodKV) :: bassume(0 < methodK && 1000*methodK < permissionOnePercent)

+    val (methodKV, methodK) = Boogie.NewBVar("methodK", treal, true)

+    val methodKStmts = BLocal(methodKV) :: bassume(0.0 < methodK && 1000.0*methodK < permissionOnePercent)

  

     // check definedness of refinement specifications

     Proc(mt.FullName + "$checkDefinedness",

@@ -767,10 +767,10 @@ class Translator {
         val (flagV, flag) = Boogie.NewBVar("predFlag", tbool, true)

         

         // pick new k

-        val (foldKV, foldK) = Boogie.NewBVar("foldK", tint, true)

+        val (foldKV, foldK) = Boogie.NewBVar("foldK", treal, true)

         val stmts = Comment("fold") ::

         functionTrigger(o, pred.predicate) ::

-        BLocal(foldKV) :: bassume(0 < foldK && 1000*foldK < percentPermission(1) && 1000*foldK < methodK) ::

+        BLocal(foldKV) :: bassume(0.0 < foldK && 1000.0*foldK < percentPermission(1) && 1000.0*foldK < methodK) ::

         isDefined(e) :::

         isDefined(perm) :::

         bassert(nonNull(o), s.pos, "The target of the fold statement might be null.") ::

@@ -792,7 +792,7 @@ class Translator {
         val definition = scaleExpressionByPermission(SubstThis(DefinitionOf(pred.predicate), e), perm, unfld.pos)

         

         // pick new k

-        val (unfoldKV, unfoldK) = Boogie.NewBVar("unfoldK", tint, true)

+        val (unfoldKV, unfoldK) = Boogie.NewBVar("unfoldK", treal, true)

         // record version of unfolded instance

         val (receiverV, receiver) = Boogie.NewBVar("predRec", tref, true)

         val (versionV, version) = Boogie.NewBVar("predVer", tint, true)

@@ -800,7 +800,7 @@ class Translator {
         functionTrigger(o, pred.predicate) ::

         BLocal(receiverV) :: (receiver := o) ::

         BLocal(versionV) :: (version := etran.Heap.select(o, pred.predicate.FullName)) ::

-        BLocal(unfoldKV) :: bassume(0 < unfoldK && unfoldK < percentPermission(1) && 1000*unfoldK < methodK) ::

+        BLocal(unfoldKV) :: bassume(0.0 < unfoldK && unfoldK < percentPermission(1) && 1000.0*unfoldK < methodK) ::

         isDefined(e) :::

         bassert(nonNull(o), s.pos, "The target of the fold statement might be null.") ::

         isDefined(perm) :::

@@ -822,9 +822,9 @@ class Translator {
         val argsSeqLength = 1 + args.length;

         

         // pick new k for this fork

-        val (asyncMethodCallKV, asyncMethodCallK) = Boogie.NewBVar("asyncMethodCallK", tint, true)

+        val (asyncMethodCallKV, asyncMethodCallK) = Boogie.NewBVar("asyncMethodCallK", treal, true)

         BLocal(asyncMethodCallKV) ::

-        bassume(0 < asyncMethodCallK && 1000*asyncMethodCallK < percentPermission(1) && 1000*asyncMethodCallK < methodK) ::

+        bassume(0.0 < asyncMethodCallK && 1000.0*asyncMethodCallK < percentPermission(1) && 1000.0*asyncMethodCallK < methodK) ::

         Comment("call " + id) ::

         // declare the local variable, if needed

         { if (c.local == null)

@@ -858,8 +858,8 @@ class Translator {
         BLocal(tokenV) :: Havoc(tokenId) :: bassume(nonNull(tokenId)) ::

         // the following assumes help in proving that the token is fresh

         bassume(etran.Heap.select(tokenId, "joinable") ==@ 0) ::

-        bassume(new Boogie.MapSelect(etran.Mask, tokenId, "joinable", "perm$N")==@ 0) ::

-        bassume(new Boogie.MapSelect(etran.Mask, tokenId, "joinable", "perm$R")==@ 0) ::

+        bassume(new Boogie.MapSelect(etran.Mask, tokenId, "joinable", "perm$N")==@ 0.0) ::

+        bassume(new Boogie.MapSelect(etran.Mask, tokenId, "joinable", "perm$R")==@ 0.0) ::

         etran.IncPermission(tokenId, "joinable", permissionFull) :::

         // create a fresh value for the joinable field

         BLocal(asyncStateV) :: Boogie.Havoc(asyncState) :: bassume(asyncState !=@ 0) ::

@@ -889,12 +889,12 @@ class Translator {
         val (preCallSecMaskV, preCallSecMask) = NewBVar("preCallSecMask", tmask, true);

         val (preCallCreditsV, preCallCredits) = NewBVar("preCallCredits", tcredits, true);

         val postEtran = new ExpressionTranslator(etran.globals, Globals(preCallHeap, preCallMask, preCallSecMask, preCallCredits), currentClass);

-        val (asyncJoinKV, asyncJoinK) = Boogie.NewBVar("asyncJoinK", tint, true)

+        val (asyncJoinKV, asyncJoinK) = Boogie.NewBVar("asyncJoinK", treal, true)

         

         Comment("join async") :: 

         // pick new k for this join

         BLocal(asyncJoinKV) ::

-        bassume(0 < asyncJoinK) ::

+        bassume(0.0 < asyncJoinK) ::

         // try to use the same k as for the fork

         bassume(asyncJoinK ==@ etran.Heap.select(token, forkK)) :: 

         // check that token is well-defined

@@ -1106,10 +1106,10 @@ class Translator {
     val (preGlobalsV, preGlobals) = etran.FreshGlobals("pre")

 

     // pick new k for the spec stmt

-    val (specKV, specK) = Boogie.NewBVar("specStmtK", tint, true)

+    val (specKV, specK) = Boogie.NewBVar("specStmtK", treal, true)

 

     BLocal(specKV) ::

-    bassume(0 < specK && 1000*specK < percentPermission(1) && 1000*specK < methodK) ::

+    bassume(0.0 < specK && 1000.0*specK < percentPermission(1) && 1000.0*specK < methodK) ::

     // declare new local variables

     s.locals.flatMap(v => translateLocalVarDecl(v, true)) :::

     Comment("spec statement") ::

@@ -1139,9 +1139,9 @@ class Translator {
     val postEtran = etran.FromPreGlobals(preGlobals)

     

     // pick new k for this method call

-    val (methodCallKV, methodCallK) = Boogie.NewBVar("methodCallK", tint, true)

+    val (methodCallKV, methodCallK) = Boogie.NewBVar("methodCallK", treal, true)

     BLocal(methodCallKV) ::

-    bassume(0 < methodCallK && 1000*methodCallK < percentPermission(1) && 1000*methodCallK < methodK) ::

+    bassume(0.0 < methodCallK && 1000.0*methodCallK < percentPermission(1) && 1000.0*methodCallK < methodK) ::

     Comment("call " + id) ::

     // introduce formal parameters and pre-state globals

     (for (v <- formalThisV :: formalInsV ::: formalOutsV) yield BLocal(Variable2BVarWhere(v))) :::

@@ -1189,13 +1189,13 @@ class Translator {
     val oldLocks = lkchOld map (e => loopEtran.oldEtran.Tr(e))

     val iterStartLocks = lkchIterStart map (e => iterStartEtran.oldEtran.Tr(e))

     val newLocks = lkch map (e => loopEtran.Tr(e));

-    val (whileKV, whileK) = Boogie.NewBVar("whileK", tint, true)

+    val (whileKV, whileK) = Boogie.NewBVar("whileK", treal, true)

     val previousEtran = etran // save etran

     

     Comment("while") ::

     // pick new k for this method call

     BLocal(whileKV) ::

-    bassume(0 < whileK && 1000*whileK < percentPermission(1) && 1000*whileK < methodK) ::

+    bassume(0.0 < whileK && 1000.0*whileK < percentPermission(1) && 1000.0*whileK < methodK) ::

     // save globals

     BLocals(preLoopGlobalsV) :::

     copyState(preLoopGlobals, loopEtran) :::

@@ -1426,7 +1426,7 @@ class Translator {
           List(ttV),

           List(Boogie.BVar("$o", tref), Boogie.BVar("$f", FieldType(tt))),

           Nil,

-          (o ==@ bnull) || ((new MapSelect(etran.Mask, o, f, "perm$R") ==@ 0) && (new MapSelect(etran.Mask, o, f, "perm$N") ==@ 0))

+          (o ==@ bnull) || ((new MapSelect(etran.Mask, o, f, "perm$R") ==@ 0.0) && (new MapSelect(etran.Mask, o, f, "perm$N") ==@ 0.0))

         ), pos, msg)

       )

     } else {

@@ -1698,7 +1698,7 @@ class ExpressionTranslator(val globals: Globals, preGlobals: Globals, val fpi: F
         val tmpTranslator = new ExpressionTranslator(tmpGlobals, this.oldEtran.globals, currentClass);

         

         // pick new k

-        val (funcappKV, funcappK) = Boogie.NewBVar("funcappK", tint, true)

+        val (funcappKV, funcappK) = Boogie.NewBVar("funcappK", treal, true)

         

         // check definedness of receiver

         (if (!func.f.isStatic) {

@@ -1712,7 +1712,7 @@ class ExpressionTranslator(val globals: Globals, preGlobals: Globals, val fpi: F
         } else Nil) :::

         // check precondition of the function by exhaling the precondition in tmpHeap/tmpMask/tmpCredits

         Comment("check precondition of call") ::

-        BLocal(funcappKV) :: bassume(0 < funcappK && 1000*funcappK < percentPermission(1)) ::

+        BLocal(funcappKV) :: bassume(0.0 < funcappK && 1000.0*funcappK < percentPermission(1)) ::

         bassume(assumption) ::

         BLocals(tmpGlobalsV) :::

         copyState(tmpGlobals, this) :::

@@ -1731,13 +1731,13 @@ class ExpressionTranslator(val globals: Globals, preGlobals: Globals, val fpi: F
         val definition = scaleExpressionByPermission(SubstThis(DefinitionOf(pred.predicate), obj), perm, unfolding.pos)

         

         // pick new k

-        val (unfoldingKV, unfoldingK) = Boogie.NewBVar("unfoldingK", tint, true)

+        val (unfoldingKV, unfoldingK) = Boogie.NewBVar("unfoldingK", treal, true)

         // record version of unfolded instance

 	val (receiverV, receiver) = Boogie.NewBVar("predRec", tref, true)

 	val (versionV, version) = Boogie.NewBVar("predVer", tint, true)

 	

         val res = Comment("unfolding") ::

-        BLocal(unfoldingKV) :: bassume(0 < unfoldingK && 1000*unfoldingK < percentPermission(1)) ::

+        BLocal(unfoldingKV) :: bassume(0.0 < unfoldingK && 1000.0*unfoldingK < percentPermission(1)) ::

         BLocal(flagV) :: (flag := true) ::

         BLocal(receiverV) :: (receiver := o) ::

         BLocal(versionV) :: (version := etran.Heap.select(o, pred.predicate.FullName)) :::

@@ -2239,14 +2239,14 @@ def buildTriggersCovering(vars : Set[Variable], functs : List[(Boogie.FunctionAp
     stmts :::

     (perm.permissionType match {

       case PermissionType.Mixed =>

-        bassume(f > 0 || (f == 0 && n > 0)) ::

+        bassume(f > 0.0 || (f == 0.0 && n > 0.0)) ::

         IncPermission(obj, memberName, f, m) :::

         IncPermissionEpsilon(obj, memberName, n, m)

       case PermissionType.Epsilons =>

-        bassume(n > 0) ::

+        bassume(n > 0.0) ::

         IncPermissionEpsilon(obj, memberName, n, m)

       case PermissionType.Fraction =>

-        bassume(f > 0) ::

+        bassume(f > 0.0) ::

         IncPermission(obj, memberName, f, m)

     })

   }

@@ -2299,9 +2299,9 @@ def buildTriggersCovering(vars : Set[Variable], functs : List[(Boogie.FunctionAp
       // assume that the permission is positive

       bassume((SeqContains(e, ref) ==>

       (perm.permissionType match {

-        case PermissionType.Fraction => r > 0

-        case PermissionType.Mixed    => r > 0 || (r == 0 && n > 0)

-        case PermissionType.Epsilons => n > 0

+        case PermissionType.Fraction => r > 0.0

+        case PermissionType.Mixed    => r > 0.0 || (r == 0.0 && n > 0.0)

+        case PermissionType.Epsilons => n > 0.0

       })).forall(refV)) ::

       (if (check) isDefined(s)(true) ::: isDefined(perm)(true) else Nil) :::

       {

@@ -2583,15 +2583,15 @@ def buildTriggersCovering(vars : Set[Variable], functs : List[(Boogie.FunctionAp
     val res = stmts :::

     (perm.permissionType match {

       case PermissionType.Mixed =>

-        bassert(f > 0 || (f == 0 && n > 0), error.pos, error.message + " The permission at " + pos + " might not be positive.") ::

+        bassert(f > 0.0 || (f == 0.0 && n > 0.0), error.pos, error.message + " The permission at " + pos + " might not be positive.") ::

         (if (isUpdatingSecMask) DecPermissionBoth2(obj, memberName, f, n, em, error, pos, exactchecking)

         else DecPermissionBoth(obj, memberName, f, n, em, error, pos, exactchecking))

       case PermissionType.Epsilons =>

-        bassert(n > 0, error.pos, error.message + " The permission at " + pos + " might not be positive.") ::

+        bassert(n > 0.0, error.pos, error.message + " The permission at " + pos + " might not be positive.") ::

         (if (isUpdatingSecMask) DecPermissionEpsilon2(obj, memberName, n, em, error, pos)

         else DecPermissionEpsilon(obj, memberName, n, em, error, pos))

       case PermissionType.Fraction =>

-        bassert(f > 0, error.pos, error.message + " The permission at " + pos + " might not be positive.") ::

+        bassert(f > 0.0, error.pos, error.message + " The permission at " + pos + " might not be positive.") ::

         (if (isUpdatingSecMask) DecPermission2(obj, memberName, f, em, error, pos, exactchecking)

         else DecPermission(obj, memberName, f, em, error, pos, exactchecking))

     })

@@ -2643,7 +2643,7 @@ def buildTriggersCovering(vars : Set[Variable], functs : List[(Boogie.FunctionAp
       val ec = needExactChecking(perm, exactchecking)

       if (ec != onlyExactCheckingPermissions) Nil else {

         val memberName = if(e.isPredicate) e.predicate.FullName else e.f.FullName;

-        val (starKV, starK) = NewBVar("starK", tint, true);

+        val (starKV, starK) = NewBVar("starK", treal, true);

         val trE = Tr(e.e)

         

         // check definedness

@@ -2693,19 +2693,19 @@ def buildTriggersCovering(vars : Set[Variable], functs : List[(Boogie.FunctionAp
           // assert that the permission is positive

           bassert((SeqContains(e, ref) ==>

             (perm.permissionType match {

-              case PermissionType.Fraction => r > 0

-              case PermissionType.Mixed    => r > 0 || (r == 0 && n > 0)

-              case PermissionType.Epsilons => n > 0

+              case PermissionType.Fraction => r > 0.0

+              case PermissionType.Mixed    => r > 0.0 || (r == 0.0 && n > 0.0)

+              case PermissionType.Epsilons => n > 0.0

             })).forall(refV), error.pos, error.message + " The permission at " + acc.pos + " might not be positive.") ::

           // make sure enough permission is available

           //  (see comment in front of method exhale for explanation of isUpdatingSecMask)

           (if (!isUpdatingSecMask) bassert((SeqContains(e, ref) ==>

             ((perm,perm.permissionType) match {

-              case _ if !ec     => mr > 0

-              case (Star,_)     => mr > 0

-              case (_,PermissionType.Fraction) => r <= mr && (r ==@ mr ==> 0 <= mn)

+              case _ if !ec     => mr > 0.0

+              case (Star,_)     => mr > 0.0

+              case (_,PermissionType.Fraction) => r <= mr && (r ==@ mr ==> 0.0 <= mn)

               case (_,PermissionType.Mixed)    => r <= mr && (r ==@ mr ==> n <= mn)

-              case (_,PermissionType.Epsilons) => mr ==@ 0 ==> n <= mn

+              case (_,PermissionType.Epsilons) => mr ==@ 0.0 ==> n <= mn

             })).forall(refV), error.pos, error.message + " Insufficient permission at " + acc.pos + " for " + member.f.FullName) :: Nil else Nil) :::

           // additional assumption on k if we have a star permission or use inexact checking

           ( perm match {

@@ -2769,26 +2769,26 @@ def buildTriggersCovering(vars : Set[Variable], functs : List[(Boogie.FunctionAp
   def extractKFromPermission(expr: Permission, currentK: Expr): (Expr, List[Boogie.Stmt]) = expr match {

     case Full => (permissionFull, Nil)

     case Epsilon => (currentK, Nil)

-    case Epsilons(_) => (0, Nil)

+    case Epsilons(_) => (0.0, Nil)

     case PredicateEpsilon(_) => (predicateK, Nil)

     case MonitorEpsilon(_) => (monitorK, Nil)

     case ChannelEpsilon(_) => (channelK, Nil)

     case MethodEpsilon => (currentK, Nil)

     case ForkEpsilon(token) =>

       val fk = etran.Heap.select(Tr(token), forkK)

-      (fk, bassume(0 < fk && fk < percentPermission(1)) /* this is always true for forkK */)

+      (fk, bassume(0.0 < fk && fk < percentPermission(1)) /* this is always true for forkK */)

     case Star =>

-      val (starKV, starK) = NewBVar("starK", tint, true);

-      (starK, BLocal(starKV) :: bassume(starK > 0 /* an upper bound is provided later by DecPermission */) :: Nil)

+      val (starKV, starK) = NewBVar("starK", treal, true);

+      (starK, BLocal(starKV) :: bassume(starK > 0.0 /* an upper bound is provided later by DecPermission */) :: Nil)

     case Frac(p) => (percentPermission(Tr(p)), Nil)

     case IntPermTimes(lhs, rhs) => {

       val (r, rs) = extractKFromPermission(rhs, currentK)

-      (lhs * r, rs)

+      (int2real(lhs) * r, rs)

     }

     case PermTimes(lhs, rhs) => {

       val (l, ls) = extractKFromPermission(lhs, currentK)

       val (r, rs) = extractKFromPermission(rhs, currentK)

-      val (resV, res) = Boogie.NewBVar("productK", tint, true)

+      val (resV, res) = Boogie.NewBVar("productK", treal, true)

       (res, ls ::: rs ::: BLocal(resV) :: bassume(permissionFull * res ==@ l * r) :: Nil)

     }

     case PermPlus(lhs, rhs) => {

@@ -2804,10 +2804,10 @@ def buildTriggersCovering(vars : Set[Variable], functs : List[(Boogie.FunctionAp
   }

   

   def extractEpsilonsFromPermission(expr: Permission): Expr = expr match {

-    case _:Write => 0

-    case Epsilons(n) => Tr(n)

-    case PermTimes(lhs, rhs) => 0 // multiplication cannot give epsilons

-    case IntPermTimes(lhs, rhs) => lhs * extractEpsilonsFromPermission(rhs)

+    case _:Write => 0.0

+    case Epsilons(n) => int2real(Tr(n))

+    case PermTimes(lhs, rhs) => 0.0 // multiplication cannot give epsilons

+    case IntPermTimes(lhs, rhs) => int2real(lhs) * extractEpsilonsFromPermission(rhs)

     case PermPlus(lhs, rhs) => {

       val l = extractEpsilonsFromPermission(lhs)

       val r = extractEpsilonsFromPermission(rhs)

@@ -2877,13 +2877,13 @@ def buildTriggersCovering(vars : Set[Variable], functs : List[(Boogie.FunctionAp
   def CanWrite(obj: Boogie.Expr, field: Boogie.Expr): Boogie.Expr = new Boogie.FunctionApp("CanWrite", Mask, obj, field)

   def CanWrite(obj: Boogie.Expr, field: String): Boogie.Expr = CanWrite(obj, new Boogie.VarExpr(field))

   def HasNoPermission(obj: Boogie.Expr, field: String) =

-    (new Boogie.MapSelect(Mask, obj, field, "perm$R") ==@ Boogie.IntLiteral(0)) &&

-    (new Boogie.MapSelect(Mask, obj, field, "perm$N") ==@ Boogie.IntLiteral(0))

+    (new Boogie.MapSelect(Mask, obj, field, "perm$R") ==@ 0.0) &&

+    (new Boogie.MapSelect(Mask, obj, field, "perm$N") ==@ 0.0)

   def SetNoPermission(obj: Boogie.Expr, field: String, mask: Boogie.Expr) =

     Boogie.Assign(new Boogie.MapSelect(mask, obj, field), Boogie.VarExpr("Permission$Zero"))

   def HasFullPermission(obj: Boogie.Expr, field: String, mask: Boogie.Expr) =

     (new Boogie.MapSelect(mask, obj, field, "perm$R") ==@ permissionFull) &&

-    (new Boogie.MapSelect(mask, obj, field, "perm$N") ==@ Boogie.IntLiteral(0))

+    (new Boogie.MapSelect(mask, obj, field, "perm$N") ==@ 0.0)

   def SetFullPermission(obj: Boogie.Expr, field: String) =

     Boogie.Assign(new Boogie.MapSelect(Mask, obj, field), Boogie.VarExpr("Permission$Full"))

 

@@ -2897,13 +2897,13 @@ def buildTriggersCovering(vars : Set[Variable], functs : List[(Boogie.FunctionAp
   def DecPermission(obj: Boogie.Expr, field: String, howMuch: Boogie.Expr, mask: Boogie.Expr, error: ErrorMessage, pos: Position, exactchecking: Boolean): List[Boogie.Stmt] = {

     val fP: Boogie.Expr = new Boogie.MapSelect(mask, obj, field, "perm$R")

     val fC: Boogie.Expr = new Boogie.MapSelect(mask, obj, field, "perm$N")

-    (if (exactchecking) bassert(howMuch <= fP && (howMuch ==@ fP ==> 0 <= fC), error.pos, error.message + " Insufficient fraction at " + pos + " for " + field + ".") :: Nil

-    else bassert(fP > 0, error.pos, error.message + " Insufficient fraction at " + pos + " for " + field + ".") :: bassume(howMuch < fP)) :::

+    (if (exactchecking) bassert(howMuch <= fP && (howMuch ==@ fP ==> 0.0 <= fC), error.pos, error.message + " Insufficient fraction at " + pos + " for " + field + ".") :: Nil

+    else bassert(fP > 0.0, error.pos, error.message + " Insufficient fraction at " + pos + " for " + field + ".") :: bassume(howMuch < fP)) :::

     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): List[Boogie.Stmt] = {

     val xyz = new Boogie.MapSelect(mask, obj, field, "perm$N")

-    bassert((new Boogie.MapSelect(mask, obj, field, "perm$R") ==@ Boogie.IntLiteral(0)) ==> (epsilons <= xyz), error.pos, error.message + " Insufficient epsilons at " + pos + "  for " + field + ".") ::

+    bassert((new Boogie.MapSelect(mask, obj, field, "perm$R") ==@ 0.0) ==> (epsilons <= xyz), error.pos, error.message + " Insufficient epsilons at " + pos + "  for " + field + ".") ::

     MapUpdate3(mask, obj, field, "perm$N", new Boogie.MapSelect(mask, obj, field, "perm$N") - epsilons) ::

     bassume(wf(Heap, Mask, SecMask)) :: Nil

   }

@@ -2912,30 +2912,30 @@ def buildTriggersCovering(vars : Set[Variable], functs : List[(Boogie.FunctionAp
     val fC: Boogie.Expr = new Boogie.MapSelect(mask, obj, field, "perm$N")

 

     (if (exactchecking) bassert(howMuch <= fP && (howMuch ==@ fP ==> epsilons <= fC), error.pos, error.message + " Insufficient permission at " + pos + " for " + field + ".") :: Nil

-    else bassert(fP > 0, error.pos, error.message + " Insufficient permission at " + pos + " for " + field + ".") :: bassume(howMuch < fP)) :::

+    else bassert(fP > 0.0, error.pos, error.message + " Insufficient permission at " + pos + " for " + field + ".") :: bassume(howMuch < fP)) :::

     MapUpdate3(mask, obj, field, "perm$N", fC - epsilons) ::

     MapUpdate3(mask, obj, field, "perm$R", fP - howMuch) ::

     bassume(wf(Heap, Mask, SecMask)) :: Nil

   }

   def DecPermission2(obj: Boogie.Expr, field: String, howMuch: Boogie.Expr, mask: Boogie.Expr, error: ErrorMessage, pos: Position, exactchecking: Boolean): List[Boogie.Stmt] = {

     DecPermission(obj, field, howMuch, mask, error, pos, exactchecking) :::

-    Boogie.If(new Boogie.MapSelect(mask, obj, field, "perm$R") < 0,

-        MapUpdate3(mask, obj, field, "perm$R", 0),

+    Boogie.If(new Boogie.MapSelect(mask, obj, field, "perm$R") < 0.0,

+        MapUpdate3(mask, obj, field, "perm$R", 0.0),

         Nil)

   }

   def DecPermissionEpsilon2(obj: Boogie.Expr, field: String, epsilons: Boogie.Expr, mask: Boogie.Expr, error: ErrorMessage, pos: Position): List[Boogie.Stmt] = {

     DecPermissionEpsilon(obj, field, epsilons, mask, error, pos) :::

-    Boogie.If(new Boogie.MapSelect(mask, obj, field, "perm$N") < 0,

-        MapUpdate3(mask, obj, field, "perm$N", 0),

+    Boogie.If(new Boogie.MapSelect(mask, obj, field, "perm$N") < 0.0,

+        MapUpdate3(mask, obj, field, "perm$N", 0.0),

         Nil)

   }

   def DecPermissionBoth2(obj: Boogie.Expr, field: String, howMuch: Boogie.Expr, epsilons: Boogie.Expr, mask: Boogie.Expr, error: ErrorMessage, pos: Position, exactchecking: Boolean): List[Boogie.Stmt] = {

     DecPermissionBoth(obj, field, howMuch, epsilons, mask, error, pos, exactchecking) :::

-    Boogie.If(new Boogie.MapSelect(mask, obj, field, "perm$R") < 0,

-        MapUpdate3(mask, obj, field, "perm$R", 0),

+    Boogie.If(new Boogie.MapSelect(mask, obj, field, "perm$R") < 0.0,

+        MapUpdate3(mask, obj, field, "perm$R", 0.0),

         Nil) ::

-    Boogie.If(new Boogie.MapSelect(mask, obj, field, "perm$N") < 0,

-        MapUpdate3(mask, obj, field, "perm$N", 0),

+    Boogie.If(new Boogie.MapSelect(mask, obj, field, "perm$N") < 0.0,

+        MapUpdate3(mask, obj, field, "perm$N", 0.0),

         Nil) :: Nil

   }

 

@@ -3032,6 +3032,7 @@ object TranslationHelper {
   implicit def field2Expr(f: Field) = VarExpr(f.FullName);

   implicit def bool2Bool(b: Boolean): Boogie.BoolLiteral = Boogie.BoolLiteral(b)

   implicit def int2Int(n: Int): Boogie.IntLiteral = Boogie.IntLiteral(n)

+   implicit def real2Real(d: Double): Boogie.RealLiteral = Boogie.RealLiteral(d)

   implicit def lift(s: Boogie.Stmt): List[Boogie.Stmt] = List(s)

   implicit def type2BType(cl: Class): BType = {

     if(cl.IsRef) {

@@ -3074,6 +3075,7 @@ object TranslationHelper {
   def tArgSeq = NamedType("ArgSeq");

   def tref = NamedType("ref");

   def tbool = NamedType("bool");

+  def treal = NamedType("real");

   def tmu  = NamedType("Mu");

   def tint = NamedType("int");

   def tstring = NamedType("string");

@@ -3097,10 +3099,11 @@ object TranslationHelper {
   def permissionOnePercent = percentPermission(1);

   def percentPermission(e: Expr) = {

     Chalice.percentageSupport match {

-      case 0 | 1 => e*VarExpr("Permission$denominator")

-      case 2 | 3 => FunctionApp("Fractions", List(e))

+      case 0 => int2real(e)*0.01

+      case 1 => FunctionApp("Fractions", List(e))

     }

   }

+  def int2real(e: Expr): Expr = FunctionApp("real", List(e))

   def forkK = "forkK";

   def channelK = "channelK";

   def monitorK = "monitorK";