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/dafny0/Reads.dfy        | 16 +++++++++++++---
 Test/dafny0/Reads.dfy.expect |  6 ++----
 Test/hofs/Classes.dfy        |  9 ++++-----
 Test/hofs/Classes.dfy.expect |  9 +++------
 4 files changed, 22 insertions(+), 18 deletions(-)

(limited to 'Test')

diff --git a/Test/dafny0/Reads.dfy b/Test/dafny0/Reads.dfy
index 7e0ca1c4..6dedbada 100644
--- a/Test/dafny0/Reads.dfy
+++ b/Test/dafny0/Reads.dfy
@@ -58,7 +58,7 @@ function ok5(r : R):()
 // Reads checking where there are circularities among the expressions
 
 class CircularChecking {
-  var Repr: set<object>
+  ghost var Repr: set<object>
     
   function F(): int
     reads this, Repr
@@ -76,8 +76,8 @@ class CircularChecking {
     requires Repr == {}
 
   function H0(cell: Cell): int
-    reads Repr  // error: reads is not self-framing (unless "this in Repr")
-    requires this in Repr  // lo and behold!  So, reads clause is fine, if we can assume the precondition
+    reads Repr  // by itself, this reads is not self-framing
+    requires this in Repr  // lo and behold!  So, reads clause is fine after all
 
   function H1(cell: Cell): int
     reads this, Repr
@@ -126,3 +126,13 @@ function FunctionInQuantifier2(): int
   var f: int -> int :| f.reads(10) == {} && f.requires(10) && f(10) == 100;  // fine :) :)
   f(10)
 }
+
+class DynamicFramesIdiom {
+  ghost var Repr: set<object>
+  predicate IllFormed_Valid()
+    reads Repr  // error: reads is not self framing (notice the absence of "this")
+  {
+    this in Repr  // this says that the predicate returns true if "this in Repr", but the
+                  // predicate can also be invoked in a state where its body will evaluate to false
+  }
+}
diff --git a/Test/dafny0/Reads.dfy.expect b/Test/dafny0/Reads.dfy.expect
index 0b599f3f..1199797f 100644
--- a/Test/dafny0/Reads.dfy.expect
+++ b/Test/dafny0/Reads.dfy.expect
@@ -1,4 +1,4 @@
-Reads.dfy(79,11): Error: insufficient reads clause to read field
+Reads.dfy(133,11): Error: insufficient reads clause to read field
 Execution trace:
     (0,0): anon0
 Reads.dfy(9,30): Error: insufficient reads clause to read field
@@ -7,8 +7,6 @@ Execution trace:
 Reads.dfy(18,30): Error: insufficient reads clause to read field
 Execution trace:
     (0,0): anon0
-    (0,0): anon10_Then
-    (0,0): anon4
 Reads.dfy(28,50): Error: insufficient reads clause to read field
 Execution trace:
     (0,0): anon0
@@ -32,4 +30,4 @@ Reads.dfy(120,38): Error: insufficient reads clause to invoke function
 Execution trace:
     (0,0): anon0
 
-Dafny program verifier finished with 16 verified, 9 errors
+Dafny program verifier finished with 17 verified, 9 errors
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