From cf064ddef7b6cb91023d3de7220345fcccc87b9e Mon Sep 17 00:00:00 2001
From: Rustan Leino <leino@microsoft.com>
Date: Sat, 22 Oct 2011 22:48:16 -0700
Subject: Dafny: added translation of Assign case of the parallel statement
 Dafny: discovered and fixed bug in no-overlap check of multi-dimensional
 array update, and changed previously incorrect MatrixFun.dfy test case (the
 new version is also a more efficient program)

---
 Dafny/Resolver.cs | 19 ++++++++++++++++---
 1 file changed, 16 insertions(+), 3 deletions(-)

(limited to 'Dafny/Resolver.cs')

diff --git a/Dafny/Resolver.cs b/Dafny/Resolver.cs
index ca173dbc..f970a7a5 100644
--- a/Dafny/Resolver.cs
+++ b/Dafny/Resolver.cs
@@ -311,8 +311,8 @@ namespace Microsoft.Dafny {
     Function currentFunction;
     readonly Scope<TypeParameter>/*!*/ allTypeParameters = new Scope<TypeParameter>();
     readonly Scope<IVariable>/*!*/ scope = new Scope<IVariable>();
-    readonly Scope<Statement>/*!*/ labeledStatements = new Scope<Statement>();
-    readonly List<Statement> loopStack = new List<Statement>();  // the enclosing loops (from which it is possible to break out)
+    Scope<Statement>/*!*/ labeledStatements = new Scope<Statement>();
+    List<Statement> loopStack = new List<Statement>();  // the enclosing loops (from which it is possible to break out)
     readonly Dictionary<Statement, bool> inSpecOnlyContext = new Dictionary<Statement, bool>();  // invariant: domain contain union of the domains of "labeledStatements" and "loopStack"
 
     /// <summary>
@@ -1558,7 +1558,15 @@ namespace Microsoft.Dafny {
           }
         }
         s.IsGhost = bodyMustBeSpecOnly;
+
+        // clear the labels for the duration of checking the body, because break statements are not allowed to leave a parallel statement 
+        var prevLblStmts = labeledStatements;
+        var prevLoopStack = loopStack;
+        labeledStatements = new Scope<Statement>();
+        loopStack = new List<Statement>();
         ResolveStatement(s.Body, bodyMustBeSpecOnly, method);
+        labeledStatements = prevLblStmts;
+        loopStack = prevLoopStack;
         scope.PopMarker();
 
         if (prevErrorCount == ErrorCount) {
@@ -1577,7 +1585,12 @@ namespace Microsoft.Dafny {
               } else if (lhs is MultiSelectExpr) {
                 // cool
               } else {
-                Error(s0, "unexpected or disallowed assignment LHS in parallel statement");
+                Contract.Assert(false);  // unexpected assignment LHS
+              }
+              var rhs = ((AssignStmt)s0).Rhs;  // ExprRhs and HavocRhs are fine, but TypeRhs is not
+              // TODO: Occurrences of Choose in RHS must also be handled or disallowed (this happen when Choose is treated like a method member of the set type)
+              if (rhs is TypeRhs) {
+                Error(rhs.Tok, "new allocation not supported in parallel statements");
               }
               s.Kind = ParallelStmt.ParBodyKind.Assign;
             } else if (s0 is CallStmt) {
-- 
cgit v1.2.3