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

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