diff options
Diffstat (limited to 'Test/hofs/OneShot.dfy')
-rw-r--r-- | Test/hofs/OneShot.dfy | 25 |
1 files changed, 25 insertions, 0 deletions
diff --git a/Test/hofs/OneShot.dfy b/Test/hofs/OneShot.dfy new file mode 100644 index 00000000..73b08fe2 --- /dev/null +++ b/Test/hofs/OneShot.dfy @@ -0,0 +1,25 @@ +// RUN: %dafny /compile:0 "%s" > "%t" +// RUN: %diff "%s.expect" "%t" + +class Ref<A> { + var val : A; +} + +method OneShot() { + var g : () -> bool; + var i : Ref<int>; + i := new Ref; + + g := () -> true; + + assert g(); + + i.val := i.val + 1; // heap changes + + if * { + assert g(); // should fail + } else { + assert !g(); // should fail + } +} + |