diff options
Diffstat (limited to 'Test/hofs/Classes.dfy')
-rw-r--r-- | Test/hofs/Classes.dfy | 17 |
1 files changed, 17 insertions, 0 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 + } +} |