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
148
149
150
151
152
153
154
155
156
157
158
159
160
161
162
163
164
165
166
167
168
169
170
171
172
173
174
175
176
177
178
179
180
181
182
183
184
185
186
187
188
189
190
191
192
193
194
195
|
[kernel] Parsing share/libc/__fc_builtin_for_normalization.i (no preprocessing)
[kernel] Parsing tests/value/relations2.i (no preprocessing)
[value] Analyzing a complete application starting at main
[value] Computing initial state
[value] Initial state computed
[value:initial-state] Values of globals at initialization
sv ∈ [--..--]
a[0..513] ∈ [--..--]
T[0] ∈ {0}
[1] ∈ {1}
[2] ∈ {42}
[3] ∈ {5}
[4] ∈ {6}
[5] ∈ {41}
[6] ∈ {42}
[value] computing for function bts2166 <- main.
Called from tests/value/relations2.i:63.
tests/value/relations2.i:6:[value] warning: function bts2166: precondition got status unknown.
tests/value/relations2.i:7:[value] warning: function bts2166: precondition got status unknown.
[value] DUMPING STATE of file tests/value/relations2.i line 15
sv ∈ [--..--]
len ∈ [--..--]
n ∈ [1..64]
a[0..513] ∈ [--..--]
T[0] ∈ {0}
[1] ∈ {1}
[2] ∈ {42}
[3] ∈ {5}
[4] ∈ {6}
[5] ∈ {41}
[6] ∈ {42}
=END OF DUMP==
[value] Called Frama_C_show_each_end([0..4294967295], [0..64])
[value] Recording results for bts2166
[value] Done for function bts2166
[value] computing for function main2 <- main.
Called from tests/value/relations2.i:64.
[value] computing for function unsigned_interval <- main2 <- main.
Called from tests/value/relations2.i:29.
[value] using specification for function unsigned_interval
[value] Done for function unsigned_interval
[value] computing for function unsigned_interval <- main2 <- main.
Called from tests/value/relations2.i:30.
[value] Done for function unsigned_interval
[value] computing for function unsigned_interval <- main2 <- main.
Called from tests/value/relations2.i:31.
[value] Done for function unsigned_interval
tests/value/relations2.i:32:[value] entering loop for the first time
[value] DUMPING STATE of file tests/value/relations2.i line 33
sv ∈ [--..--]
a[0..513] ∈ [--..--]
i ∈ [1..512]
t ∈ [0..511]
n ∈ [0..512]
s ∈ {0}
b3 ∈ UNINITIALIZED
T[0] ∈ {0}
[1] ∈ {1}
[2] ∈ {42}
[3] ∈ {5}
[4] ∈ {6}
[5] ∈ {41}
[6] ∈ {42}
=END OF DUMP==
tests/value/relations2.i:34:[value] warning: accessing out of bounds index.
assert (unsigned int)(i - (unsigned int)(t + 1)) < 514;
[value] DUMPING STATE of file tests/value/relations2.i line 33
sv ∈ [--..--]
a[0..513] ∈ [--..--]
i ∈ [1..512]
t ∈ [0..511]
n ∈ [0..512]
s ∈ {0; 1}
b3 ∈ UNINITIALIZED
T[0] ∈ {0}
[1] ∈ {1}
[2] ∈ {42}
[3] ∈ {5}
[4] ∈ {6}
[5] ∈ {41}
[6] ∈ {42}
=END OF DUMP==
[value] DUMPING STATE of file tests/value/relations2.i line 33
sv ∈ [--..--]
a[0..513] ∈ [--..--]
i ∈ [1..512]
t ∈ [0..511]
n ∈ [0..512]
s ∈ {0; 1; 2}
b3 ∈ UNINITIALIZED
T[0] ∈ {0}
[1] ∈ {1}
[2] ∈ {42}
[3] ∈ {5}
[4] ∈ {6}
[5] ∈ {41}
[6] ∈ {42}
=END OF DUMP==
[value] DUMPING STATE of file tests/value/relations2.i line 33
sv ∈ [--..--]
a[0..513] ∈ [--..--]
i ∈ [1..512]
t ∈ [0..511]
n ∈ [0..512]
s ∈ [0..2147483647]
b3 ∈ UNINITIALIZED
T[0] ∈ {0}
[1] ∈ {1}
[2] ∈ {42}
[3] ∈ {5}
[4] ∈ {6}
[5] ∈ {41}
[6] ∈ {42}
=END OF DUMP==
tests/value/relations2.i:35:[value] warning: signed overflow. assert s + b3 ≤ 2147483647;
[value] Recording results for main2
[value] Done for function main2
[value] computing for function main3 <- main.
Called from tests/value/relations2.i:65.
[value] Called Frama_C_show_each_NO1()
[value] Called Frama_C_show_each_OK1()
[value] Called Frama_C_show_each_OK2()
[value] Called Frama_C_show_each_NO2()
[value] Recording results for main3
[value] Done for function main3
[value] Recording results for main
[value] done for function main
[value] ====== VALUES COMPUTED ======
[value:final-states] Values at end of function bts2166:
len ∈ [--..--]
n ∈ [0..64]
[value:final-states] Values at end of function main3:
T[0] ∈ {0; 2}
[1] ∈ {1; 2}
[2] ∈ {42}
[3] ∈ {5}
[4] ∈ {6}
[5] ∈ {17; 41}
[6] ∈ {17; 42}
[value:final-states] Values at end of function main2:
i ∈ [0..512]
t ∈ [0..512]
n ∈ [0..512]
s ∈ [0..2147483647]
[value:final-states] Values at end of function main:
T[0] ∈ {0; 2}
[1] ∈ {1; 2}
[2] ∈ {42}
[3] ∈ {5}
[4] ∈ {6}
[5] ∈ {17; 41}
[6] ∈ {17; 42}
[from] Computing for function bts2166
[from] Computing for function Frama_C_dump_each <-bts2166
[from] Done for function Frama_C_dump_each
[from] Done for function bts2166
[from] Computing for function main3
[from] Done for function main3
[from] Computing for function main2
[from] Computing for function unsigned_interval <-main2
[from] Done for function unsigned_interval
[from] Done for function main2
[from] Computing for function main
[from] Done for function main
[from] ====== DEPENDENCIES COMPUTED ======
These dependencies hold at termination for the executions that terminate:
[from] Function bts2166:
NO EFFECTS
[from] Function main3:
T[0..1] FROM T[0..1]; i (and SELF)
[5..6] FROM T[3..4]; i (and SELF)
[from] Function unsigned_interval:
\result FROM i1; i2
[from] Function main2:
\result FROM a[0..513]
[from] Function main:
T[0..1] FROM sv; T[0..1] (and SELF)
[5..6] FROM sv; T[3..4] (and SELF)
[from] ====== END OF DEPENDENCIES ======
[inout] Out (internal) for function bts2166:
len; n
[inout] Inputs for function bts2166:
\nothing
[inout] Out (internal) for function main3:
T{[0..1]; [5..6]}
[inout] Inputs for function main3:
T[0..6]
[inout] Out (internal) for function main2:
i; t; n; s; b3
[inout] Inputs for function main2:
a[0..513]
[inout] Out (internal) for function main:
T{[0..1]; [5..6]}
[inout] Inputs for function main:
sv; a[0..513]; T[0..6]
|
