From 0c1ec594e68dab4fcd458a00f9f7a1ac6de2e218 Mon Sep 17 00:00:00 2001
From: leino <unknown>
Date: Mon, 28 Sep 2015 13:16:15 -0700
Subject: 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.

---
 Test/dafny0/TypeTests.dfy | 50 ++++++++++++++++++++++++-----------------------
 1 file changed, 26 insertions(+), 24 deletions(-)

(limited to 'Test/dafny0/TypeTests.dfy')

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 ---------
-- 
cgit v1.2.3