Merge commit 'df5c5f5'

1 files changed, 14 insertions, 3 deletions

diff --git a/Test/dafny0/ParallelResolveErrors.dfy b/Test/dafny0/ParallelResolveErrors.dfy
index 5e01f019..8c48487d 100644
--- a/Test/dafny0/ParallelResolveErrors.dfy
+++ b/Test/dafny0/ParallelResolveErrors.dfy
@@ -7,7 +7,6 @@ class C {
   ghost method Init_ModifyNothing() { }

   ghost method Init_ModifyThis() modifies this;

   {

-    data := 6;  // error: assignment to a non-ghost field

     gdata := 7;

   }

   ghost method Init_ModifyStuff(c: C) modifies this, c; { }

@@ -40,8 +39,8 @@ method M0(IS: set<int>)
   {

     var x := i;

     x := x + 1;

-    y := 18;  // (this statement is not allowed, since y is declared outside the forall, but that check happens only if the first resolution pass of the forall statement passes, which it doesn't in this case because of the next line)

-    z := 20;  // error: assigning to a non-ghost variable inside a ghost forall block

+    y := 18;  // error: assigning to a (ghost) variable inside a ghost forall block

+    z := 20;  // error: assigning to a (non-ghost) variable inside a ghost forall block

   }

 

   forall (i | 0 <= i)

@@ -120,3 +119,15 @@ method M3(c: C)
     c.GhostMethodWithModifies(x);  // error: not allowed to call method with nonempty modifies clause

   }

 }

+

+module AnotherModule {

+  class C {

+    var data: int;

+    ghost var gdata: int;

+    ghost method Init_ModifyThis() modifies this;

+    {

+      data := 6;  // error: assignment to a non-ghost field

+      gdata := 7;

+    }

+  }

+}