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 ++++-----
 1 file changed, 4 insertions(+), 5 deletions(-)

(limited to 'Test/hofs/Classes.dfy')

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)
-- 
cgit v1.2.3


From e7430a9b1d17ea92e986470e898d6b74fae3cea6 Mon Sep 17 00:00:00 2001
From: leino <unknown>
Date: Tue, 30 Jun 2015 17:27:21 -0700
Subject: Additional test case for instance functions

---
 Test/hofs/Classes.dfy        | 17 +++++++++++++++++
 Test/hofs/Classes.dfy.expect |  5 ++++-
 2 files changed, 21 insertions(+), 1 deletion(-)

(limited to 'Test/hofs/Classes.dfy')

diff --git a/Test/hofs/Classes.dfy b/Test/hofs/Classes.dfy
index 0ceb46f1..9d8044db 100644
--- a/Test/hofs/Classes.dfy
+++ b/Test/hofs/Classes.dfy
@@ -47,3 +47,20 @@ method U(t : T)
   t.h := x => x;
   assert J(t) == 0; // ok
 }
+
+class MyClass {
+  var data: int
+	function method F(): int
+	  reads this
+	{
+	  data
+	}	
+  method M(that: MyClass)
+	  requires that != null
+	{
+	  var fn := that.F;  // "that" is captured into the closure
+	  var d := fn();
+		assert d == that.data;  // yes
+		assert d == this.data;  // error: no reason to believe that this would hold
+	}	
+}
diff --git a/Test/hofs/Classes.dfy.expect b/Test/hofs/Classes.dfy.expect
index e490dbe0..1c9e31f0 100644
--- a/Test/hofs/Classes.dfy.expect
+++ b/Test/hofs/Classes.dfy.expect
@@ -1,7 +1,10 @@
+Classes.dfy(64,12): Error: assertion violation
+Execution trace:
+    (0,0): anon0
 Classes.dfy(40,6): Error: possible violation of function precondition
 Execution trace:
     (0,0): anon0
     (0,0): anon7_Else
     (0,0): anon8_Else
 
-Dafny program verifier finished with 6 verified, 1 error
+Dafny program verifier finished with 8 verified, 2 errors
-- 
cgit v1.2.3