blob: 73b08fe2f7d4c71c4ec9955ba8072175a6121e58 (
plain)
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
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
}
}
|