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/NonGhostQuantifiers.dfy | 7 +++++++
 1 file changed, 7 insertions(+)

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

diff --git a/Test/dafny0/NonGhostQuantifiers.dfy b/Test/dafny0/NonGhostQuantifiers.dfy
index bff1d65b..e522d0fc 100644
--- a/Test/dafny0/NonGhostQuantifiers.dfy
+++ b/Test/dafny0/NonGhostQuantifiers.dfy
@@ -181,6 +181,12 @@ module DependencyOnAllAllocatedObjects {
     forall c: SomeClass :: true  // error: not allowed to dependend on which objects are allocated
   }
 
+  class SomeClass {
+    var f: int;
+  }
+}
+
+module DependencyOnAllAllocatedObjects_More {
   method M()
   {
     var b := forall c: SomeClass :: c != null ==> c.f == 0;  // error: non-ghost code requires bounds
@@ -192,3 +198,4 @@ module DependencyOnAllAllocatedObjects {
     var f: int;
   }
 }
+
-- 
cgit v1.2.3