From cc0a7cae53c068993e3b3004049629dd396cb649 Mon Sep 17 00:00:00 2001
From: Rustan Leino <unknown>
Date: Mon, 15 Jun 2015 17:00:04 -0700
Subject: Changed logical order of requires and reads clauses on functions. 
 Reads clauses can now assume the precondition (as had also been the case back
 in the days when reads clauses had to be self framing).

---
 Test/hofs/Classes.dfy        | 9 ++++-----
 Test/hofs/Classes.dfy.expect | 9 +++------
 2 files changed, 7 insertions(+), 11 deletions(-)

(limited to 'Test/hofs')

diff --git a/Test/hofs/Classes.dfy b/Test/hofs/Classes.dfy
index 2b892b35..0ceb46f1 100644
--- a/Test/hofs/Classes.dfy
+++ b/Test/hofs/Classes.dfy
@@ -30,15 +30,14 @@ function B(t : T) : int -> int
 }
 
 function J(t : T) : int
-  requires t != null;
-  requires t.h.reads(0) == {};
-  reads t;
-  reads if t != null then t.h.reads(0) else {};
+  requires t != null
+  reads t
+  reads t.h.reads(0)
 {
   if t.h.requires(0) then
     B(t)(0)
   else
-    B(t)(0)  // fail
+    B(t)(0)  // error: precondition violation
 }
 
 method U(t : T)
diff --git a/Test/hofs/Classes.dfy.expect b/Test/hofs/Classes.dfy.expect
index 21188d62..e490dbe0 100644
--- a/Test/hofs/Classes.dfy.expect
+++ b/Test/hofs/Classes.dfy.expect
@@ -1,10 +1,7 @@
-Classes.dfy(41,6): Error: possible violation of function precondition
+Classes.dfy(40,6): Error: possible violation of function precondition
 Execution trace:
     (0,0): anon0
-    (0,0): anon13_Then
-    (0,0): anon4
-    (0,0): anon14_Then
-    (0,0): anon15_Else
-    (0,0): anon16_Else
+    (0,0): anon7_Else
+    (0,0): anon8_Else
 
 Dafny program verifier finished with 6 verified, 1 error
-- 
cgit v1.2.3