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/CallStmtTests.dfy | 34 +++++++++++++++++++---------------
 1 file changed, 19 insertions(+), 15 deletions(-)

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

diff --git a/Test/dafny0/CallStmtTests.dfy b/Test/dafny0/CallStmtTests.dfy
index 67e66b34..46c466ff 100644
--- a/Test/dafny0/CallStmtTests.dfy
+++ b/Test/dafny0/CallStmtTests.dfy
@@ -1,23 +1,27 @@
 // RUN: %dafny /compile:0 /print:"%t.print" /dprint:"%t.dprint" "%s" > "%t"
 // RUN: %diff "%s.expect" "%t"
 
-method testing1(t: int)
-{
-   t := m(); // error: should be checked at the Dafny level, not fall to Boogie.
-}
+module M0 {
+  method testing1(t: int)
+ {
+    t := m(); // error: should be checked at the Dafny level, not fall to Boogie.
+  }
 
-method m() returns (r: int)
-{
-   return 3;
+  method m() returns (r: int)
+  {
+    return 3;
+  }
 }
 
-method testing2()
-{
-   var v;
-   v := m2(); // error: v needs to be ghost because r is.
-}
+module M1 {
+  method testing2()
+  {
+    var v;
+    v := m2(); // error: v needs to be ghost because r is.
+  }
 
-method m2() returns (ghost r: int)
-{
-   r := 23;
+  method m2() returns (ghost r: int)
+  {
+    r := 23;
+  }
 }
-- 
cgit v1.2.3