Chalice: Fix workitem 10191 (escaping method arguments).

1 files changed, 29 insertions, 12 deletions

diff --git a/Chalice/src/Parser.scala b/Chalice/src/Parser.scala
index 1d74d636..4800b552 100644
--- a/Chalice/src/Parser.scala
+++ b/Chalice/src/Parser.scala
@@ -79,23 +79,32 @@ class Parser extends StandardTokenParsers {
    */

 

   def memberDecl = {

-    currentLocalVariables = Set[String]();

     positioned(fieldDecl | invariantDecl | methodDecl | conditionDecl | predicateDecl | functionDecl | couplingDecl | transformDecl) // important that last one is transformDecl

   }

-  def fieldDecl =

-        ( "var" ~> idType <~ Semi ^^ { case (id,t) => Field(id.v, t, false) }

-        | "ghost" ~> "var" ~> idType <~ Semi ^^ { case (id,t) => Field(id.v, t, true) }

-        )

-  def invariantDecl = "invariant" ~> expression <~ Semi ^^ MonitorInvariant

-  def methodDecl =

+  def fieldDecl = {

+    currentLocalVariables = Set[String]();

+    ( "var" ~> idType <~ Semi ^^ { case (id,t) => Field(id.v, t, false) }

+    | "ghost" ~> "var" ~> idType <~ Semi ^^ { case (id,t) => Field(id.v, t, true) }

+    )

+  }

+  def invariantDecl = {

+    currentLocalVariables = Set[String]();

+    "invariant" ~> expression <~ Semi ^^ MonitorInvariant

+  }

+  def methodDecl = {

+    currentLocalVariables = Set[String]();

     "method" ~> ident ~ formalParameters(true) ~ ("returns" ~> formalParameters(false) ?) ~

     (methodSpec*) ~ blockStatement ^^ {

       case id ~ ins ~ outs ~ spec ~ body =>

         Method(id, ins, outs match {case None => Nil; case Some(outs) => outs}, spec, body)

     }

-  def predicateDecl: Parser[Predicate] =

+  }

+  def predicateDecl: Parser[Predicate] = {

+    currentLocalVariables = Set[String]();

     ("predicate" ~> ident) ~ ("{" ~> expression <~ "}") ^^ { case id ~ definition => Predicate(id, definition) }

-  def functionDecl =

+  }

+  def functionDecl = {

+    currentLocalVariables = Set[String]();

     ("unlimited" ?) ~ ("function" ~> ident) ~ formalParameters(true) ~ (":" ~> typeDecl) ~ (methodSpec*) ~ opt("{" ~> expression <~ "}") ^^ {

       case u ~ id ~ ins ~ out ~ specs ~ body => {

         val f = Function(id, ins, out, specs, body);

@@ -103,10 +112,14 @@ class Parser extends StandardTokenParsers {
         f

       }

     }

-  def conditionDecl =

+  }

+  def conditionDecl = {

+    currentLocalVariables = Set[String]();

     "condition" ~> ident ~ ("where" ~> expression ?) <~ Semi ^^ {

       case id ~ optE => Condition(id, optE) }

-  def transformDecl =

+  }

+  def transformDecl = {

+    currentLocalVariables = Set[String]();

     ( "refines" ~> ident ~ formalParameters(true) ~ ("returns" ~> formalParameters(false) ?) ~ (methodSpec*) ~ blockStatement ^^ {

         case id ~ ins ~outs ~ spec ~ body =>

           MethodTransform(id, ins, outs match {case None => Nil; case Some(outs) => outs}, spec, ProgramPat(body)) }).|(

@@ -118,7 +131,11 @@ class Parser extends StandardTokenParsers {
             MethodTransform(id, ins, outs match {case None => Nil; case Some(outs) => outs}, spec, AST.normalize(trans))

         }

       })

-  def couplingDecl = ("replaces" ~> rep1sep(ident, ",") <~ "by") ~ expression <~ Semi ^^ {case ids ~ e => CouplingInvariant(ids, e)}

+  }

+  def couplingDecl = {

+    currentLocalVariables = Set[String]();

+    ("replaces" ~> rep1sep(ident, ",") <~ "by") ~ expression <~ Semi ^^ {case ids ~ e => CouplingInvariant(ids, e)}

+  }

 

   def formalParameters(immutable: Boolean) =

     "(" ~> (formalList(immutable) ?) <~ ")" ^^ {