diff options
| author |  stefanheule <unknown> | 2011-07-07 18:13:56 +0200 |
|---|---|---|
| committer | stefanheule <unknown> | 2011-07-07 18:13:56 +0200 |
| commit | d9ffe3c5bc218f6a0306734f1dafd37672bcf784 (patch) | |
| tree | ad3e1ab78818e5a791c73aa1e8eee6e9352e1ad9 /Chalice | |
| parent | 37b1d69f307247afb237a8f4a6eb4a7555df6e2e (diff) | |
Chalice: Fix workitem 10191 (escaping method arguments).
Diffstat (limited to 'Chalice')
| -rw-r--r-- | Chalice/src/Parser.scala | 41 |
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) ?) <~ ")" ^^ {
|