Newer
Older
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
196
197
198
199
200
201
202
203
204
205
206
207
208
209
210
211
212
213
214
215
216
217
218
219
220
221
222
223
224
225
226
227
228
229
230
231
232
233
234
[kernel] Parsing tests/libc/stdlib_h.c (with preprocessing)
[eva] Analyzing a complete application starting at main
[eva] Computing initial state
[eva] Initial state computed
[eva:initial-state] Values of globals at initialization
nondet ∈ [--..--]
[eva] computing for function strtol <- main.
Called from tests/libc/stdlib_h.c:20.
[eva] using specification for function strtol
[eva] tests/libc/stdlib_h.c:20:
function strtol: precondition 'valid_nptr' got status valid.
[eva] tests/libc/stdlib_h.c:20:
function strtol: precondition 'separation' got status valid.
[eva] tests/libc/stdlib_h.c:20:
function strtol: precondition 'base_range' got status valid.
[eva] tests/libc/stdlib_h.c:20:
function strtol, behavior store_position: precondition 'valid_endptr' got status valid.
[eva] Done for function strtol
[eva] computing for function strtol <- main.
Called from tests/libc/stdlib_h.c:21.
[eva:alarm] tests/libc/stdlib_h.c:21: Warning:
function strtol: precondition 'valid_nptr' got status unknown.
[eva] tests/libc/stdlib_h.c:21:
function strtol: precondition 'separation' got status valid.
[eva] tests/libc/stdlib_h.c:21:
function strtol: precondition 'base_range' got status valid.
[eva] tests/libc/stdlib_h.c:21:
function strtol, behavior store_position: precondition 'valid_endptr' got status valid.
[eva] Done for function strtol
[eva] computing for function strtol <- main.
Called from tests/libc/stdlib_h.c:22.
[eva:alarm] tests/libc/stdlib_h.c:22: Warning:
function strtol: precondition 'valid_nptr' got status unknown.
[eva] tests/libc/stdlib_h.c:22:
function strtol: precondition 'separation' got status valid.
[eva] tests/libc/stdlib_h.c:22:
function strtol: precondition 'base_range' got status valid.
[eva] Done for function strtol
[eva] computing for function strtol <- main.
Called from tests/libc/stdlib_h.c:23.
[eva] tests/libc/stdlib_h.c:23:
function strtol: precondition 'valid_nptr' got status valid.
[eva] tests/libc/stdlib_h.c:23:
function strtol: precondition 'separation' got status valid.
[eva] tests/libc/stdlib_h.c:23:
function strtol: precondition 'base_range' got status valid.
[eva] Done for function strtol
[eva] computing for function strtoll <- main.
Called from tests/libc/stdlib_h.c:27.
[eva] using specification for function strtoll
[eva] tests/libc/stdlib_h.c:27:
function strtoll: precondition 'valid_nptr' got status valid.
[eva] tests/libc/stdlib_h.c:27:
function strtoll: precondition 'separation' got status valid.
[eva] tests/libc/stdlib_h.c:27:
function strtoll: precondition 'base_range' got status valid.
[eva] tests/libc/stdlib_h.c:27:
function strtoll, behavior store_position: precondition 'valid_endptr' got status valid.
[eva] Done for function strtoll
[eva] computing for function strtoll <- main.
Called from tests/libc/stdlib_h.c:28.
[eva:alarm] tests/libc/stdlib_h.c:28: Warning:
function strtoll: precondition 'valid_nptr' got status unknown.
[eva] tests/libc/stdlib_h.c:28:
function strtoll: precondition 'separation' got status valid.
[eva] tests/libc/stdlib_h.c:28:
function strtoll: precondition 'base_range' got status valid.
[eva] tests/libc/stdlib_h.c:28:
function strtoll, behavior store_position: precondition 'valid_endptr' got status valid.
[eva] Done for function strtoll
[eva] computing for function strtoll <- main.
Called from tests/libc/stdlib_h.c:29.
[eva:alarm] tests/libc/stdlib_h.c:29: Warning:
function strtoll: precondition 'valid_nptr' got status unknown.
[eva] tests/libc/stdlib_h.c:29:
function strtoll: precondition 'separation' got status valid.
[eva] tests/libc/stdlib_h.c:29:
function strtoll: precondition 'base_range' got status valid.
[eva] Done for function strtoll
[eva] computing for function strtoul <- main.
Called from tests/libc/stdlib_h.c:33.
[eva] using specification for function strtoul
[eva] tests/libc/stdlib_h.c:33:
function strtoul: precondition 'valid_nptr' got status valid.
[eva] tests/libc/stdlib_h.c:33:
function strtoul: precondition 'separation' got status valid.
[eva] tests/libc/stdlib_h.c:33:
function strtoul: precondition 'base_range' got status valid.
[eva] tests/libc/stdlib_h.c:33:
function strtoul, behavior store_position: precondition 'valid_endptr' got status valid.
[eva] Done for function strtoul
[eva] computing for function strtoul <- main.
Called from tests/libc/stdlib_h.c:34.
[eva:alarm] tests/libc/stdlib_h.c:34: Warning:
function strtoul: precondition 'valid_nptr' got status unknown.
[eva] tests/libc/stdlib_h.c:34:
function strtoul: precondition 'separation' got status valid.
[eva] tests/libc/stdlib_h.c:34:
function strtoul: precondition 'base_range' got status valid.
[eva] tests/libc/stdlib_h.c:34:
function strtoul, behavior store_position: precondition 'valid_endptr' got status valid.
[eva] Done for function strtoul
[eva] computing for function strtoul <- main.
Called from tests/libc/stdlib_h.c:35.
[eva:alarm] tests/libc/stdlib_h.c:35: Warning:
function strtoul: precondition 'valid_nptr' got status unknown.
[eva] tests/libc/stdlib_h.c:35:
function strtoul: precondition 'separation' got status valid.
[eva] tests/libc/stdlib_h.c:35:
function strtoul: precondition 'base_range' got status valid.
[eva] Done for function strtoul
[eva] computing for function strtoull <- main.
Called from tests/libc/stdlib_h.c:39.
[eva] using specification for function strtoull
[eva] tests/libc/stdlib_h.c:39:
function strtoull: precondition 'valid_nptr' got status valid.
[eva] tests/libc/stdlib_h.c:39:
function strtoull: precondition 'separation' got status valid.
[eva] tests/libc/stdlib_h.c:39:
function strtoull: precondition 'base_range' got status valid.
[eva] tests/libc/stdlib_h.c:39:
function strtoull, behavior store_position: precondition 'valid_endptr' got status valid.
[eva] Done for function strtoull
[eva] computing for function strtoull <- main.
Called from tests/libc/stdlib_h.c:40.
[eva:alarm] tests/libc/stdlib_h.c:40: Warning:
function strtoull: precondition 'valid_nptr' got status unknown.
[eva] tests/libc/stdlib_h.c:40:
function strtoull: precondition 'separation' got status valid.
[eva] tests/libc/stdlib_h.c:40:
function strtoull: precondition 'base_range' got status valid.
[eva] tests/libc/stdlib_h.c:40:
function strtoull, behavior store_position: precondition 'valid_endptr' got status valid.
[eva] Done for function strtoull
[eva] computing for function strtoull <- main.
Called from tests/libc/stdlib_h.c:41.
[eva:alarm] tests/libc/stdlib_h.c:41: Warning:
function strtoull: precondition 'valid_nptr' got status unknown.
[eva] tests/libc/stdlib_h.c:41:
function strtoull: precondition 'separation' got status valid.
[eva] tests/libc/stdlib_h.c:41:
function strtoull: precondition 'base_range' got status valid.
[eva] Done for function strtoull
[eva] computing for function strtod <- main.
Called from tests/libc/stdlib_h.c:46.
[eva] using specification for function strtod
[eva] tests/libc/stdlib_h.c:46:
function strtod: precondition 'valid_nptr' got status valid.
[eva] tests/libc/stdlib_h.c:46:
function strtod: precondition 'separation' got status valid.
[eva] tests/libc/stdlib_h.c:46:
function strtod, behavior store_position: precondition 'valid_endptr' got status valid.
[eva] Done for function strtod
[eva] computing for function strtod <- main.
Called from tests/libc/stdlib_h.c:47.
[eva:alarm] tests/libc/stdlib_h.c:47: Warning:
function strtod: precondition 'valid_nptr' got status unknown.
[eva] tests/libc/stdlib_h.c:47:
function strtod: precondition 'separation' got status valid.
[eva] tests/libc/stdlib_h.c:47:
function strtod, behavior store_position: precondition 'valid_endptr' got status valid.
[eva] Done for function strtod
[eva] computing for function strtod <- main.
Called from tests/libc/stdlib_h.c:48.
[eva:alarm] tests/libc/stdlib_h.c:48: Warning:
function strtod: precondition 'valid_nptr' got status unknown.
[eva] tests/libc/stdlib_h.c:48:
function strtod: precondition 'separation' got status valid.
[eva] Done for function strtod
[eva] computing for function strtold <- main.
Called from tests/libc/stdlib_h.c:52.
[eva] using specification for function strtold
[eva] tests/libc/stdlib_h.c:52:
function strtold: precondition 'valid_nptr' got status valid.
[eva] tests/libc/stdlib_h.c:52:
function strtold: precondition 'separation' got status valid.
[eva] tests/libc/stdlib_h.c:52:
function strtold, behavior store_position: precondition 'valid_endptr' got status valid.
[eva] Done for function strtold
[eva] computing for function strtold <- main.
Called from tests/libc/stdlib_h.c:53.
[eva:alarm] tests/libc/stdlib_h.c:53: Warning:
function strtold: precondition 'valid_nptr' got status unknown.
[eva] tests/libc/stdlib_h.c:53:
function strtold: precondition 'separation' got status valid.
[eva] tests/libc/stdlib_h.c:53:
function strtold, behavior store_position: precondition 'valid_endptr' got status valid.
[eva] Done for function strtold
[eva] computing for function strtold <- main.
Called from tests/libc/stdlib_h.c:54.
[eva:alarm] tests/libc/stdlib_h.c:54: Warning:
function strtold: precondition 'valid_nptr' got status unknown.
[eva] tests/libc/stdlib_h.c:54:
function strtold: precondition 'separation' got status valid.
[eva] Done for function strtold
[eva] computing for function strtof <- main.
Called from tests/libc/stdlib_h.c:58.
[eva] using specification for function strtof
[eva] tests/libc/stdlib_h.c:58:
function strtof: precondition 'valid_nptr' got status valid.
[eva] tests/libc/stdlib_h.c:58:
function strtof: precondition 'separation' got status valid.
[eva] tests/libc/stdlib_h.c:58:
function strtof, behavior store_position: precondition 'valid_endptr' got status valid.
[eva] Done for function strtof
[eva] computing for function strtof <- main.
Called from tests/libc/stdlib_h.c:59.
[eva:alarm] tests/libc/stdlib_h.c:59: Warning:
function strtof: precondition 'valid_nptr' got status unknown.
[eva] tests/libc/stdlib_h.c:59:
function strtof: precondition 'separation' got status valid.
[eva] tests/libc/stdlib_h.c:59:
function strtof, behavior store_position: precondition 'valid_endptr' got status valid.
[eva] Done for function strtof
[eva] computing for function strtof <- main.
Called from tests/libc/stdlib_h.c:60.
[eva:alarm] tests/libc/stdlib_h.c:60: Warning:
function strtof: precondition 'valid_nptr' got status unknown.
[eva] tests/libc/stdlib_h.c:60:
function strtof: precondition 'separation' got status valid.
[eva] Done for function strtof
[eva] computing for function bsearch <- main.
Called from tests/libc/stdlib_h.c:64.
[eva] using specification for function bsearch
[eva] tests/libc/stdlib_h.c:64:
function bsearch: precondition 'valid_function_compar' got status valid.
[eva] Done for function bsearch
[eva:alarm] tests/libc/stdlib_h.c:65: Warning: assertion got status unknown.
[eva] computing for function bsearch <- main.
Called from tests/libc/stdlib_h.c:67.
[eva] tests/libc/stdlib_h.c:67:
function bsearch: precondition 'valid_function_compar' got status valid.
[eva] Done for function bsearch
[eva:alarm] tests/libc/stdlib_h.c:68: Warning: assertion got status unknown.
[eva] computing for function mkstemp <- main.
Called from tests/libc/stdlib_h.c:82.
[eva] using specification for function mkstemp
[eva] tests/libc/stdlib_h.c:82:
function mkstemp: precondition 'valid_template' got status valid.
[eva] Done for function mkstemp
241
242
243
244
245
246
247
248
249
250
251
252
253
254
255
256
257
258
259
260
261
262
263
264
265
266
267
268
269
[eva] Recording results for main
[eva] done for function main
[eva] ====== VALUES COMPUTED ======
[eva:final-states] Values at end of function main:
base ∈ {0; 2; 36}
sl ∈ {{ "12 34 -56" }}
s ∈ {{ " 3.14 0x1.2p2" }}
pl ∈ {{ "12 34 -56" + [0..--] }}
q ∈ {{ " 3.14 0x1.2p2" + [0..--] }}
l ∈ [--..--]
pll ∈ {{ "12 34 -56" + [0..--] }}
ll ∈ [--..--]
pul ∈ {{ "12 34 -56" + [0..--] }}
ul ∈ [--..--]
pull ∈ {{ "12 34 -56" + [0..--] }}
ull ∈ [--..--]
sd ∈ {{ " 3.14 0x1.2p2" }}
pd ∈ {{ " 3.14 0x1.2p2" + [0..--] }}
d ∈ [-inf .. inf] ∪ {NaN}
pld ∈ {{ " 3.14 0x1.2p2" + [0..--] }}
ld ∈ [-inf .. inf] ∪ {NaN}
pf ∈ {{ " 3.14 0x1.2p2" + [0..--] }}
f ∈ [-inf .. inf] ∪ {NaN}
ai[0] ∈ {1}
[1] ∈ {-1}
[2] ∈ {50000}
[3] ∈ {20}
key ∈ {-1}
p ∈ {{ &ai[1] }}
tempFilename[0..9] ∈ [--..--]
r ∈ [-1..19]
__retres ∈ {0}