blob: 025a3f5f736e196982829cc4d8cd3a7d508f1598 (
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
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
|
procedure {:checksum "P0$proc#0"} P0();
// Action: skip
// Priority: 0
implementation {:checksum "P0$impl#0"} P0()
{
}
procedure {:checksum "P1$proc#0"} P1();
// Action: verify
// Priority: 1
implementation {:checksum "P1$impl#0"} P1()
{
call P2();
}
procedure {:checksum "P3$proc#0"} P3();
// Action: verify
// Priority: 2
implementation {:checksum "P3$impl#1"} P3()
{
assert false;
}
procedure {:checksum "P2$proc#0"} P2();
ensures G();
// Action: verify
// Priority: 3
implementation {:checksum "P2$impl#0"} P2()
{
}
function {:checksum "G#0"} G() : bool
{
F()
}
function {:checksum "F#1"} F() : bool
{
false
}
|