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
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131
132
133
134
135
136
137
138
139
140
141
142
143
144
145
146
147
|
[kernel] Parsing share/libc/__fc_builtin_for_normalization.i (no preprocessing)
[kernel] Parsing tests/value/inout_proto.i (no preprocessing)
[value] Analyzing a complete application starting at main_main
[value] Computing initial state
[value] Initial state computed
[value:initial-state] Values of globals at initialization
a ∈ {0}
b ∈ {0}
c ∈ {0}
t[0..9] ∈ {0}
u[0..19] ∈ {0}
[value] computing for function main <- main_main.
Called from tests/value/inout_proto.i:54.
[value] computing for function SendBuffer <- main <- main_main.
Called from tests/value/inout_proto.i:19.
[value] using specification for function SendBuffer
[value] Done for function SendBuffer
[value] Recording results for main
[value] Done for function main
[value] computing for function main2 <- main_main.
Called from tests/value/inout_proto.i:55.
[value] computing for function f <- main2 <- main_main.
Called from tests/value/inout_proto.i:46.
[value] using specification for function f
[value] Done for function f
[value] computing for function g1 <- main2 <- main_main.
Called from tests/value/inout_proto.i:47.
[value] computing for function g <- g1 <- main2 <- main_main.
Called from tests/value/inout_proto.i:34.
[value] using specification for function g
[value] Done for function g
[value] Recording results for g1
[value] Done for function g1
[value] computing for function g2 <- main2 <- main_main.
Called from tests/value/inout_proto.i:48.
[value] computing for function g <- g2 <- main2 <- main_main.
Called from tests/value/inout_proto.i:38.
[value] Done for function g
[value] Recording results for g2
[value] Done for function g2
[value] computing for function g3 <- main2 <- main_main.
Called from tests/value/inout_proto.i:50.
[value] computing for function g <- g3 <- main2 <- main_main.
Called from tests/value/inout_proto.i:42.
[value] Done for function g
[value] Recording results for g3
[value] Done for function g3
[value] Recording results for main2
[value] Done for function main2
[value] Recording results for main_main
[value] done for function main_main
[inout] InOut (internal) for function g1:
Operational inputs:
t[6..7]
Operational inputs on termination:
t[6..7]
Sure outputs:
t[3..5]
[inout] InOut (with formals) for function g1:
Operational inputs:
t[6..7]
Operational inputs on termination:
t[6..7]
Sure outputs:
t[3..5]
[inout] Inputs (with formals) for function g1:
t[6..7]
[inout] InOut (internal) for function g2:
Operational inputs:
t[3..4]
Operational inputs on termination:
t[3..4]
Sure outputs:
t[0..2]
[inout] InOut (with formals) for function g2:
Operational inputs:
t[3..4]
Operational inputs on termination:
t[3..4]
Sure outputs:
t[0..2]
[inout] Inputs (with formals) for function g2:
t[3..4]
[inout] InOut (internal) for function g3:
Operational inputs:
u[8..10]; p
Operational inputs on termination:
u[8..10]; p
Sure outputs:
\nothing
[inout] InOut (with formals) for function g3:
Operational inputs:
u[8..10]; p
Operational inputs on termination:
u[8..10]; p
Sure outputs:
\nothing
[inout] Inputs (with formals) for function g3:
u[8..10]; p
[inout] InOut (internal) for function main:
Operational inputs:
length; msg
Operational inputs on termination:
length; msg
Sure outputs:
ret
[inout] InOut (with formals) for function main:
Operational inputs:
msg
Operational inputs on termination:
msg
Sure outputs:
\nothing
[inout] Inputs (with formals) for function main:
msg
[inout] InOut (internal) for function main2:
Operational inputs:
b; t[6..7]; u[8..10]; i
Operational inputs on termination:
b; t[6..7]; u[8..10]; i
Sure outputs:
a; c; t[0..5]
[inout] InOut (with formals) for function main2:
Operational inputs:
b; t[6..7]; u[8..10]; i
Operational inputs on termination:
b; t[6..7]; u[8..10]; i
Sure outputs:
a; c; t[0..5]
[inout] Inputs (with formals) for function main2:
b; t{[3..4]; [6..7]}; u[8..10]; i
[inout] InOut (internal) for function main_main:
Operational inputs:
length; b; t[6..7]; u[8..10]; msg; i
Operational inputs on termination:
length; b; t[6..7]; u[8..10]; msg; i
Sure outputs:
a; c; t[0..5]
[inout] InOut (with formals) for function main_main:
Operational inputs:
b; t[6..7]; u[8..10]; msg; i
Operational inputs on termination:
b; t[6..7]; u[8..10]; msg; i
Sure outputs:
a; c; t[0..5]
[inout] Inputs (with formals) for function main_main:
b; t{[3..4]; [6..7]}; u[8..10]; msg; i
|
