blob: 14521adb838ece5ad22b58fd338a9914cdd90e92 (
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
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
|
var glb: int;
procedure calculate();
modifies glb;
implementation calculate()
{
var x: int;
var y: int;
anon0:
y := 5;
call x := increase(y);
return;
}
procedure {:inline 1} increase(i: int) returns (k: int);
modifies glb;
implementation {:inline 1} increase(i: int) returns (k: int)
{
var j: int;
anon0:
j := i;
j := j + 1;
glb := glb + j;
k := j;
return;
}
after inlining procedure calls
procedure calculate();
modifies glb;
implementation calculate()
{
var x: int;
var y: int;
var inline$increase$0$j: int;
var inline$increase$0$i: int;
var inline$increase$0$k: int;
var inline$increase$0$glb: int;
anon0:
y := 5;
goto inline$increase$0$Entry;
inline$increase$0$Entry:
inline$increase$0$i := y;
havoc inline$increase$0$j, inline$increase$0$k;
inline$increase$0$glb := glb;
goto inline$increase$0$anon0;
inline$increase$0$anon0:
inline$increase$0$j := inline$increase$0$i;
inline$increase$0$j := inline$increase$0$j + 1;
glb := glb + inline$increase$0$j;
inline$increase$0$k := inline$increase$0$j;
goto inline$increase$0$Return;
inline$increase$0$Return:
x := inline$increase$0$k;
goto anon0$1;
anon0$1:
return;
}
Boogie program verifier finished with 2 verified, 0 errors
|