Changed computation of ghosts until pass 2 of resolution.

Other clean-up in resolution passes, like:
Include everything of type "char" into bounds that are discovered, and likewise for reference types.
Allow more set comprehensions, determining if they are finite based on their argument type.
Changed CalcExpr.SubExpressions to not include computed expressions.

1 files changed, 12 insertions, 1 deletions

diff --git a/Test/dafny0/ParallelResolveErrors.dfy b/Test/dafny0/ParallelResolveErrors.dfy
index 61956651..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; { }

@@ -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;

+    }

+  }

+}