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, 26 insertions, 24 deletions

diff --git a/Test/dafny0/TypeTests.dfy b/Test/dafny0/TypeTests.dfy
index b44f4d68..a9d473f6 100644
--- a/Test/dafny0/TypeTests.dfy
+++ b/Test/dafny0/TypeTests.dfy
@@ -39,7 +39,7 @@ datatype ReverseOrder_TheCounterpart<T> =
 

 // ---------------------

 

-class ArrayTests {

+module ArrayTests {

   ghost method G(a: array<int>)

     requires a != null && 10 <= a.Length;

     modifies a;

@@ -167,31 +167,33 @@ module Expl_Module {
 

 // --------------------- more ghost tests, for assign-such-that statements

 

-method M()

-{

-  ghost var b: bool;

-  ghost var k: int, l: int;

-  var m: int;

-

-  k :| k < 10;

-  k, m :| 0 <= k < m;  // error: LHS has non-ghost and RHS has ghost

-  m :| m < 10;

-

-  // Because of the ghost guard, these 'if' statements are ghost contexts, so only

-  // assignments to ghosts are allowed.

-  if (b) {

-    k :| k < 10;  // should be allowed

-    k, l :| 0 <= k < l;  // ditto

-  }

-  if (b) {

-    m :| m < 10;  // error: not allowed in ghost context

-    k, m :| 0 <= k < m;  // error: not allowed in ghost context

+module MoreGhostTests {

+  method M()

+  {

+    ghost var b: bool;

+    ghost var k: int, l: int;

+    var m: int;

+

+    k :| k < 10;

+    k, m :| 0 <= k < m;  // error: LHS has non-ghost and RHS has ghost

+    m :| m < 10;

+

+    // Because of the ghost guard, these 'if' statements are ghost contexts, so only

+    // assignments to ghosts are allowed.

+    if (b) {

+      k :| k < 10;  // should be allowed

+      k, l :| 0 <= k < l;  // ditto

+    }

+    if (b) {

+      m :| m < 10;  // error: not allowed in ghost context

+      k, m :| 0 <= k < m;  // error: not allowed in ghost context

+    }

   }

-}

 

-ghost method GhostM() returns (x: int)

-{

-  x :| true;  // no problem (but there once was a problem with this case, where an error was generated for no reason)

+  ghost method GhostM() returns (x: int)

+  {

+    x :| true;  // no problem (but there once was a problem with this case, where an error was generated for no reason)

+  }

 }

 

 // ------------------ cycles that could arise from proxy assignments ---------