Chalice: fix in refinement loop target resolution; added "spec" as a keyword synonym to "var"

4 files changed, 5 insertions, 2 deletions

diff --git a/Chalice/src/Ast.scala b/Chalice/src/Ast.scala
index 7beba704..edeb52ba 100644
--- a/Chalice/src/Ast.scala
+++ b/Chalice/src/Ast.scala
@@ -268,6 +268,7 @@ case class RefinementBlock(con: List[Statement], abs: List[Statement]) extends S
     (a,c)

   }         

   override def Declares = con flatMap {_.Declares}

+  override def Targets = (con ++ abs :\ Set[Variable]()) { (s, vars) => vars ++ s.Targets}

 }

 

 /**

diff --git a/Chalice/src/Parser.scala b/Chalice/src/Parser.scala
index f086487d..2d3f99fc 100644
--- a/Chalice/src/Parser.scala
+++ b/Chalice/src/Parser.scala
@@ -31,7 +31,7 @@ class Parser extends StandardTokenParsers {
                        "ite", "fold", "unfold", "unfolding", "in", "forall", "exists",

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

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

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

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

                       )

   // todo: can we remove "nil"?

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

@@ -158,6 +158,7 @@ class Parser extends StandardTokenParsers {
     | "assume" ~> expression <~ Semi ^^ Assume

     | blockStatement ^^ BlockStmt

     | "var" ~> localVarStmt(false, false)

+    | "spec" ~> localVarStmt(false, false)

     | "const" ~> localVarStmt(true, false)

     | "ghost" ~> "const" ~> localVarStmt(true, true)

     | "ghost" ~> "var" ~> localVarStmt(false, true)

diff --git a/Chalice/src/PrettyPrinter.scala b/Chalice/src/PrettyPrinter.scala
index 236e74cc..17e81923 100644
--- a/Chalice/src/PrettyPrinter.scala
+++ b/Chalice/src/PrettyPrinter.scala
@@ -321,7 +321,7 @@ object PrintProgram {
     case ExplicitSeq(es) =>

       print("["); ExprList(es); print("]");

     case Range(min, max) =>

-      print("("); Expr(min); print(":"); Expr(max); print(")");

+      print("["); Expr(min); print(":"); Expr(max); print("]");

     case Length(e)=>

       print("|"); Expr(e); print("|");

     case At(s, n) =>

diff --git a/Chalice/src/Resolver.scala b/Chalice/src/Resolver.scala
index 2729a0d5..7ccfe7e3 100644
--- a/Chalice/src/Resolver.scala
+++ b/Chalice/src/Resolver.scala
@@ -1109,6 +1109,7 @@ object Resolver {
              if (!inv.typ.IsBool) ctx.Error(inv.pos, "loop invariant must be boolean (found " + inv.typ.FullName + ")")

            }

            resolveBody(body.ss, ctx, locals)

+           w.LoopTargets = body.Targets.filter(ctx.IsVariablePresent).toList

          case IfStmt(_, thn, None) =>

            resolveBody(thn.ss, ctx, locals)

          case IfStmt(_, thn, Some(els)) =>