Additional test case for instance functions

2 files changed, 21 insertions, 1 deletions

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