Fix some deprecation warnings from scalac 2.8.0.

Check for Boogie.exe only on Windows.
Fix parser (_ is a keyword, not a delimiter)

5 files changed, 20 insertions, 17 deletions

diff --git a/Chalice/src/Ast.scala b/Chalice/src/Ast.scala
index 7b8dea8a..4b8b9189 100644
--- a/Chalice/src/Ast.scala
+++ b/Chalice/src/Ast.scala
@@ -14,7 +14,7 @@ trait ASTNode extends Positional
  * Classes and types

  */

 

-case class TopLevelDecl(id: String) extends ASTNode

+sealed abstract class TopLevelDecl(val id: String) extends ASTNode

 

 sealed case class Class(classId: String, parameters: List[Class], module: String, members: List[Member]) extends TopLevelDecl(classId) {

   def IsInt: Boolean = false

@@ -241,7 +241,7 @@ case class BlockPat() extends Transform {
 case class SkipPat() extends Transform

 /** Replacement pattern for arbitrary block */

 case class ProgramPat(code: List[Statement]) extends Transform {

-  if (code.size > 0) pos = code.first.pos

+  if (code.size > 0) pos = code.head.pos

 }

 case class IfPat(thn: Transform, els: Option[Transform]) extends Transform

 case class WhilePat(invs: List[Expression], body: Transform) extends Transform

@@ -257,10 +257,10 @@ case class NonDetPat(is: List[String], code: List[Statement]) extends Transform
 case class InsertPat(code: List[Statement]) extends Transform

 case class SeqPat(pats: List[Transform]) extends Transform {

   assert(pats.size > 0)

-  pos = pats.first.pos;

+  pos = pats.head.pos;

 }

 case class RefinementBlock(con: List[Statement], abs: List[Statement]) extends Statement {

-  if (con.size > 0) pos = con.first.pos

+  if (con.size > 0) pos = con.head.pos

   // local variables in context at the beginning of the block

 

   var before: List[Variable] = null

@@ -525,7 +525,7 @@ case class Range(min: Expression, max: Expression /* non-inclusive*/) extends Ex
 case class Append(s0: Expression, s1: Expression) extends SeqAccess(s0, s1) {

   override val OpName = "++"

 }

-sealed abstract case class SeqAccess(e0: Expression, e1: Expression) extends BinaryExpr(e0, e1) {

+sealed abstract class SeqAccess(e0: Expression, e1: Expression) extends BinaryExpr(e0, e1) {

   override val ExpectedLhsType = null

   override val ExpectedRhsType = null

   override val ResultType = null

diff --git a/Chalice/src/Chalice.scala b/Chalice/src/Chalice.scala
index 9fb76972..fff66367 100644
--- a/Chalice/src/Chalice.scala
+++ b/Chalice/src/Chalice.scala
@@ -126,8 +126,10 @@ object Chalice {
          if (doTranslate) {

            // checking if Boogie.exe exists

            val boogieFile = new File(boogiePath);

-           if(! boogieFile.exists() || ! boogieFile.isFile()) {

-             CommandLineError("Boogie.exe not found at " + boogiePath, help); return

+           if (System.getProperty("os.name").toLowerCase.indexOf("win") >= 0) {

+             if(! boogieFile.exists() || ! boogieFile.isFile()) {

+               CommandLineError("Boogie.exe not found at " + boogiePath, help); return

+             }

            }

            // translate program to Boogie

            val translator = new Translator();

diff --git a/Chalice/src/Graph.scala b/Chalice/src/Graph.scala
index e61e482c..f6790911 100644
--- a/Chalice/src/Graph.scala
+++ b/Chalice/src/Graph.scala
@@ -97,9 +97,9 @@ class DiGraph[T] {
       for (w <- v.children) {

         if (w.index == -1) {

           tarjan(w);

-          v.lowlink = Math.min(v.lowlink, w.lowlink);

+          v.lowlink = scala.math.min(v.lowlink, w.lowlink);

         } else if (w.onstack)

-          v.lowlink = Math.min(v.lowlink, w.index);

+          v.lowlink = scala.math.min(v.lowlink, w.index);

       }

 

       if (v.lowlink == v.index) {

diff --git a/Chalice/src/Parser.scala b/Chalice/src/Parser.scala
index 27b4945d..44b8227a 100644
--- a/Chalice/src/Parser.scala
+++ b/Chalice/src/Parser.scala
@@ -31,15 +31,14 @@ class Parser extends StandardTokenParsers {
                        "ite", "fold", "unfold", "unfolding", "in", "forall", "exists",

                        "seq", "nil", "result", "eval", "token",

                        "wait", "signal", "unlimited", 

-                       "refines", "transforms", "replaces", "by", "spec"

+                       "refines", "transforms", "replaces", "by", "spec", "_", "*"

                       )

   // todo: can we remove "nil"?

   lexical.delimiters += ("(", ")", "{", "}", "[[", "]]",

                          "<==>", "==>", "&&", "||",

                          "==", "!=", "<", "<=", ">=", ">", "<<", "in", "!in",

                          "+", "-", "*", "/", "%", "!", ".", "..",

-                         ";", ":", ":=", ",", "?", "|", "[", "]", "++", "::",

-                         "_"

+                         ";", ":", ":=", ",", "?", "|", "[", "]", "++", "::"

                         )

 

   def programUnit = (classDecl | channelDecl)*

diff --git a/Chalice/src/Translator.scala b/Chalice/src/Translator.scala
index 69f82b1f..3b6187cb 100644
--- a/Chalice/src/Translator.scala
+++ b/Chalice/src/Translator.scala
@@ -1250,15 +1250,16 @@ class Translator {
     val (heldV, held) = NewBVar("isHeld", IntClass, true)

     val (rdheldV, rdheld) = NewBVar("isRdHeld", BoolClass, true)

     BLocal(heldV) :: BLocal(rdheldV) ::

-    List.flatten (for (o <- locks) yield {  // todo: somewhere we should worry about Df(l)

+    (for (o <- locks) yield {  // todo: somewhere we should worry about Df(l)

       Havoc(held) :: Havoc(rdheld) ::

       bassume(rdheld ==> (0 < held)) ::

       new MapUpdate(etran.Heap, o, VarExpr("held"), held) ::

       new MapUpdate(etran.Heap, o, VarExpr("rdheld"), rdheld) })

+    .flatten

   }

   def NumberOfLocksHeldIsInvariant(oldLocks: List[Boogie.Expr], newLocks: List[Boogie.Expr],

                                    etran: ExpressionTranslator) = {

-    List.flatten (for ((o,n) <- oldLocks zip newLocks) yield {

+    (for ((o,n) <- oldLocks zip newLocks) yield {

       // oo.held == nn.held && oo.rdheld == nn.rdheld

       (((0 < new Boogie.MapSelect(etran.oldEtran.Heap, o, "held")) ==@

         (0 < new Boogie.MapSelect(etran.Heap, n, "held"))) &&

@@ -1276,6 +1277,7 @@ class Translator {
          (! new Boogie.MapSelect(etran.Heap, o, "rdheld"))))) ::

       Nil

     })

+    .flatten

   }

 

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

@@ -1676,7 +1678,7 @@ class ExpressionTranslator(globals: List[Boogie.Expr], preGlobals: List[Boogie.E
     Comment("inhale (" + occasion + ")") ::

     BLocal(ihV) :: Boogie.Havoc(ih) ::

     bassume(IsGoodInhaleState(ih, Heap, Mask)) ::

-    List.flatten (for (p <- predicates) yield Inhale(p, ih, check)) :::

+    (for (p <- predicates) yield Inhale(p, ih, check)).flatten :::

     bassume(IsGoodMask(Mask)) ::

     bassume(wf(Heap, Mask)) ::

     Comment("end inhale")

@@ -1689,7 +1691,7 @@ class ExpressionTranslator(globals: List[Boogie.Expr], preGlobals: List[Boogie.E
     Comment("inhale (" + occasion + ")") ::

     BLocal(ihV) :: Boogie.Assign(ih, useHeap) ::

     bassume(IsGoodInhaleState(ih, Heap, Mask)) ::

-    List.flatten (for (p <- predicates) yield Inhale(p,ih, check)) :::

+    (for (p <- predicates) yield Inhale(p,ih, check)).flatten :::

     bassume(IsGoodMask(Mask)) ::

     bassume(wf(Heap, Mask)) ::

     Comment("end inhale")

@@ -1830,7 +1832,7 @@ class ExpressionTranslator(globals: List[Boogie.Expr], preGlobals: List[Boogie.E
     val (emV, em) = NewBVar("exhaleMask", tmask, true)

     Comment("begin exhale (" + occasion + ")") ::

     BLocal(emV) :: (em := Mask) ::

-    (List.flatten (for (p <- predicates) yield Exhale(p._1, em, null, p._2, check))) :::

+    (for (p <- predicates) yield Exhale(p._1, em, null, p._2, check)).flatten :::

     (Mask := em) ::

     bassume(wf(Heap, Mask)) ::

     Comment("end exhale")