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).

2 files changed, 7 insertions, 11 deletions

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