Matches in value-assignements (V): {{numOfValueMatches}}
Matches in edge-description: {{numOfDescriptionMatches}}
Rank | Scope | |||
-V- |
{{line.bestrank}}
|
{{line.desc}}
|
| Precondition (initial variable assignment): |
|
{{precondition}} |
| {{fault.rank}}. | {{fault.score}} | Details: | ||||
Current values:
|
||||||
1 | extern void abort(void); |
2 | |
3 | extern void __assert_fail (const char *__assertion, const char *__file, |
4 | unsigned int __line, const char *__function) |
5 | __attribute__ ((__nothrow__ , __leaf__)) __attribute__ ((__noreturn__)); |
6 | extern void __assert_perror_fail (int __errnum, const char *__file, |
7 | unsigned int __line, const char *__function) |
8 | __attribute__ ((__nothrow__ , __leaf__)) __attribute__ ((__noreturn__)); |
9 | extern void __assert (const char *__assertion, const char *__file, int __line) |
10 | __attribute__ ((__nothrow__ , __leaf__)) __attribute__ ((__noreturn__)); |
11 | |
12 | void reach_error() { ((void) sizeof ((0) ? 1 : 0), __extension__ ({ if (0) ; else __assert_fail ("0", "bubble_sort-2.c", 3, __extension__ __PRETTY_FUNCTION__); })); } |
13 | |
14 | |
15 | extern void __assert_fail (__const char *__assertion, __const char *__file, |
16 | unsigned int __line, __const char *__function) |
17 | __attribute__ ((__nothrow__ , __leaf__)) __attribute__ ((__noreturn__)); |
18 | extern void __assert_perror_fail (int __errnum, __const char *__file, |
19 | unsigned int __line, |
20 | __const char *__function) |
21 | __attribute__ ((__nothrow__ , __leaf__)) __attribute__ ((__noreturn__)); |
22 | extern void __assert (const char *__assertion, const char *__file, int __line) |
23 | __attribute__ ((__nothrow__ , __leaf__)) __attribute__ ((__noreturn__)); |
24 | |
25 | typedef unsigned int size_t; |
26 | |
27 | |
28 | |
29 | |
30 | struct list_head { |
31 | struct list_head *next ; |
32 | struct list_head *prev ; |
33 | }; |
34 | struct node { |
35 | int value ; |
36 | struct list_head linkage ; |
37 | struct list_head nested ; |
38 | }; |
39 | extern __attribute__((__nothrow__)) void *malloc(size_t __size ) __attribute__((__malloc__)) ; |
40 | extern __attribute__((__nothrow__)) void free(void *__ptr ) ; |
41 | extern __attribute__((__nothrow__, __noreturn__)) void abort(void) ; |
42 | extern int __VERIFIER_nondet_int(void); |
43 | static void fail(void) |
44 | { |
45 | { |
46 | ERROR: {reach_error();abort();}((0) ? (void) (0) : __assert_fail ("0", "test-0180.c", 11, __PRETTY_FUNCTION__)); |
47 | goto ERROR; |
48 | } |
49 | } |
50 | |
51 | |
52 | struct list_head gl_list = {& gl_list, & gl_list}; |
53 | |
54 | static void inspect(struct list_head const *head ) |
55 | { struct node const *node ; |
56 | unsigned int __cil_tmp3 ; |
57 | struct list_head *__cil_tmp4 ; |
58 | unsigned int __cil_tmp5 ; |
59 | int __cil_tmp6 ; |
60 | unsigned int __cil_tmp7 ; |
61 | unsigned int __cil_tmp8 ; |
62 | unsigned int __cil_tmp9 ; |
63 | struct list_head *__cil_tmp10 ; |
64 | unsigned int __cil_tmp11 ; |
65 | int __cil_tmp12 ; |
66 | unsigned int __cil_tmp13 ; |
67 | unsigned int __cil_tmp14 ; |
68 | struct list_head *__cil_tmp15 ; |
69 | unsigned int __cil_tmp16 ; |
70 | struct list_head *__cil_tmp17 ; |
71 | unsigned int __cil_tmp18 ; |
72 | int __cil_tmp19 ; |
73 | unsigned int __cil_tmp20 ; |
74 | unsigned int __cil_tmp21 ; |
75 | unsigned int __cil_tmp22 ; |
76 | struct list_head *__cil_tmp23 ; |
77 | unsigned int __cil_tmp24 ; |
78 | int __cil_tmp25 ; |
79 | struct node *__cil_tmp26 ; |
80 | unsigned int __cil_tmp27 ; |
81 | unsigned int __cil_tmp28 ; |
82 | struct list_head *__cil_tmp29 ; |
83 | unsigned long __cil_tmp30 ; |
84 | char *__cil_tmp31 ; |
85 | char *__cil_tmp32 ; |
86 | struct node *__cil_tmp33 ; |
87 | unsigned int __cil_tmp34 ; |
88 | unsigned int __cil_tmp35 ; |
89 | struct list_head const *__cil_tmp36 ; |
90 | unsigned int __cil_tmp37 ; |
91 | unsigned int __cil_tmp38 ; |
92 | unsigned int __cil_tmp39 ; |
93 | struct list_head *__cil_tmp40 ; |
94 | unsigned int __cil_tmp41 ; |
95 | int __cil_tmp42 ; |
96 | unsigned int __cil_tmp43 ; |
97 | unsigned int __cil_tmp44 ; |
98 | struct list_head const *__cil_tmp45 ; |
99 | unsigned int __cil_tmp46 ; |
100 | unsigned int __cil_tmp47 ; |
101 | unsigned int __cil_tmp48 ; |
102 | unsigned int __cil_tmp49 ; |
103 | struct list_head *__cil_tmp50 ; |
104 | unsigned int __cil_tmp51 ; |
105 | int __cil_tmp52 ; |
106 | unsigned int __cil_tmp53 ; |
107 | unsigned int __cil_tmp54 ; |
108 | struct list_head const *__cil_tmp55 ; |
109 | unsigned int __cil_tmp56 ; |
110 | unsigned int __cil_tmp57 ; |
111 | unsigned int __cil_tmp58 ; |
112 | struct list_head *__cil_tmp59 ; |
113 | unsigned int __cil_tmp60 ; |
114 | int __cil_tmp61 ; |
115 | unsigned int __cil_tmp62 ; |
116 | unsigned int __cil_tmp63 ; |
117 | struct list_head const *__cil_tmp64 ; |
118 | unsigned int __cil_tmp65 ; |
119 | unsigned int __cil_tmp66 ; |
120 | unsigned int __cil_tmp67 ; |
121 | unsigned int __cil_tmp68 ; |
122 | struct list_head *__cil_tmp69 ; |
123 | unsigned int __cil_tmp70 ; |
124 | int __cil_tmp71 ; |
125 | struct node const *__cil_tmp72 ; |
126 | unsigned int __cil_tmp73 ; |
127 | unsigned int __cil_tmp74 ; |
128 | int __cil_tmp75 ; |
129 | unsigned int __cil_tmp76 ; |
130 | unsigned int __cil_tmp77 ; |
131 | struct list_head const *__cil_tmp78 ; |
132 | struct node const *__cil_tmp79 ; |
133 | unsigned int __cil_tmp80 ; |
134 | unsigned int __cil_tmp81 ; |
135 | int __cil_tmp82 ; |
136 | int const *__cil_tmp83 ; |
137 | struct node const *__cil_tmp84 ; |
138 | unsigned int __cil_tmp85 ; |
139 | unsigned int __cil_tmp86 ; |
140 | int __cil_tmp87 ; |
141 | unsigned int __cil_tmp88 ; |
142 | unsigned int __cil_tmp89 ; |
143 | struct list_head *__cil_tmp90 ; |
144 | unsigned int __cil_tmp91 ; |
145 | unsigned int __cil_tmp92 ; |
146 | struct list_head *__cil_tmp93 ; |
147 | unsigned int __cil_tmp94 ; |
148 | unsigned int __cil_tmp95 ; |
149 | int __cil_tmp96 ; |
150 | unsigned int __cil_tmp97 ; |
151 | unsigned int __cil_tmp98 ; |
152 | unsigned int __cil_tmp99 ; |
153 | struct list_head *__cil_tmp100 ; |
154 | struct list_head *__cil_tmp101 ; |
155 | unsigned int __cil_tmp102 ; |
156 | unsigned int __cil_tmp103 ; |
157 | int __cil_tmp104 ; |
158 | struct list_head *__cil_tmp105 ; |
159 | unsigned int __cil_tmp106 ; |
160 | unsigned int __cil_tmp107 ; |
161 | unsigned int __cil_tmp108 ; |
162 | struct list_head const *__cil_tmp109 ; |
163 | unsigned int __cil_tmp110 ; |
164 | struct list_head *__cil_tmp111 ; |
165 | unsigned int __cil_tmp112 ; |
166 | struct node *__cil_tmp113 ; |
167 | unsigned int __cil_tmp114 ; |
168 | unsigned int __cil_tmp115 ; |
169 | struct list_head *__cil_tmp116 ; |
170 | unsigned long __cil_tmp117 ; |
171 | char *__cil_tmp118 ; |
172 | char *__cil_tmp119 ; |
173 | struct node *__cil_tmp120 ; |
174 | unsigned int __cil_tmp121 ; |
175 | int __cil_tmp122 ; |
176 | |
177 | { |
178 | { |
179 | while (1) { |
180 | while_0_continue: ; |
181 | if (! head) { |
182 | { |
183 | fail(); |
184 | } |
185 | } else { |
186 | } |
187 | goto while_0_break; |
188 | } |
189 | while_0_break: ; |
190 | } |
191 | { |
192 | while (1) { |
193 | while_1_continue: ; |
194 | { |
195 | __cil_tmp3 = (unsigned int )head; |
196 | __cil_tmp4 = *((struct list_head * const *)head); |
197 | __cil_tmp5 = (unsigned int )__cil_tmp4; |
198 | __cil_tmp6 = __cil_tmp5 != __cil_tmp3; |
199 | if (! __cil_tmp6) { |
200 | { |
201 | fail(); |
202 | } |
203 | } else { |
204 | } |
205 | } |
206 | goto while_1_break; |
207 | } |
208 | while_1_break: ; |
209 | } |
210 | { |
211 | while (1) { |
212 | while_2_continue: ; |
213 | { |
214 | __cil_tmp7 = (unsigned int )head; |
215 | __cil_tmp8 = (unsigned int )head; |
216 | __cil_tmp9 = __cil_tmp8 + 4; |
217 | __cil_tmp10 = *((struct list_head * const *)__cil_tmp9); |
218 | __cil_tmp11 = (unsigned int )__cil_tmp10; |
219 | __cil_tmp12 = __cil_tmp11 != __cil_tmp7; |
220 | if (! __cil_tmp12) { |
221 | { |
222 | fail(); |
223 | } |
224 | } else { |
225 | } |
226 | } |
227 | goto while_2_break; |
228 | } |
229 | while_2_break: ; |
230 | } |
231 | __cil_tmp13 = (unsigned int )head; |
232 | __cil_tmp14 = __cil_tmp13 + 4; |
233 | __cil_tmp15 = *((struct list_head * const *)__cil_tmp14); |
234 | head = (struct list_head const *)__cil_tmp15; |
235 | { |
236 | while (1) { |
237 | while_3_continue: ; |
238 | if (! head) { |
239 | { |
240 | fail(); |
241 | } |
242 | } else { |
243 | } |
244 | goto while_3_break; |
245 | } |
246 | while_3_break: ; |
247 | } |
248 | { |
249 | while (1) { |
250 | while_4_continue: ; |
251 | { |
252 | __cil_tmp16 = (unsigned int )head; |
253 | __cil_tmp17 = *((struct list_head * const *)head); |
254 | __cil_tmp18 = (unsigned int )__cil_tmp17; |
255 | __cil_tmp19 = __cil_tmp18 != __cil_tmp16; |
256 | if (! __cil_tmp19) { |
257 | { |
258 | fail(); |
259 | } |
260 | } else { |
261 | } |
262 | } |
263 | goto while_4_break; |
264 | } |
265 | while_4_break: ; |
266 | } |
267 | { |
268 | while (1) { |
269 | while_5_continue: ; |
270 | { |
271 | __cil_tmp20 = (unsigned int )head; |
272 | __cil_tmp21 = (unsigned int )head; |
273 | __cil_tmp22 = __cil_tmp21 + 4; |
274 | __cil_tmp23 = *((struct list_head * const *)__cil_tmp22); |
275 | __cil_tmp24 = (unsigned int )__cil_tmp23; |
276 | __cil_tmp25 = __cil_tmp24 != __cil_tmp20; |
277 | if (! __cil_tmp25) { |
278 | { |
279 | fail(); |
280 | } |
281 | } else { |
282 | } |
283 | } |
284 | goto while_5_break; |
285 | } |
286 | while_5_break: ; |
287 | } |
288 | __cil_tmp26 = (struct node *)0; |
289 | __cil_tmp27 = (unsigned int )__cil_tmp26; |
290 | __cil_tmp28 = __cil_tmp27 + 4; |
291 | __cil_tmp29 = (struct list_head *)__cil_tmp28; |
292 | __cil_tmp30 = (unsigned long )__cil_tmp29; |
293 | __cil_tmp31 = (char *)head; |
294 | __cil_tmp32 = __cil_tmp31 - __cil_tmp30; |
295 | __cil_tmp33 = (struct node *)__cil_tmp32; |
296 | node = (struct node const *)__cil_tmp33; |
297 | { |
298 | while (1) { |
299 | while_6_continue: ; |
300 | if (! node) { |
301 | { |
302 | fail(); |
303 | } |
304 | } else { |
305 | } |
306 | goto while_6_break; |
307 | } |
308 | while_6_break: ; |
309 | } |
310 | { |
311 | while (1) { |
312 | while_7_continue: ; |
313 | { |
314 | __cil_tmp34 = (unsigned int )node; |
315 | __cil_tmp35 = __cil_tmp34 + 12; |
316 | __cil_tmp36 = (struct list_head const *)__cil_tmp35; |
317 | __cil_tmp37 = (unsigned int )__cil_tmp36; |
318 | __cil_tmp38 = (unsigned int )node; |
319 | __cil_tmp39 = __cil_tmp38 + 12; |
320 | __cil_tmp40 = *((struct list_head * const *)__cil_tmp39); |
321 | __cil_tmp41 = (unsigned int )__cil_tmp40; |
322 | __cil_tmp42 = __cil_tmp41 == __cil_tmp37; |
323 | if (! __cil_tmp42) { |
324 | { |
325 | fail(); |
326 | } |
327 | } else { |
328 | } |
329 | } |
330 | goto while_7_break; |
331 | } |
332 | while_7_break: ; |
333 | } |
334 | { |
335 | while (1) { |
336 | while_8_continue: ; |
337 | { |
338 | __cil_tmp43 = (unsigned int )node; |
339 | __cil_tmp44 = __cil_tmp43 + 12; |
340 | __cil_tmp45 = (struct list_head const *)__cil_tmp44; |
341 | __cil_tmp46 = (unsigned int )__cil_tmp45; |
342 | __cil_tmp47 = 12 + 4; |
343 | __cil_tmp48 = (unsigned int )node; |
344 | __cil_tmp49 = __cil_tmp48 + __cil_tmp47; |
345 | __cil_tmp50 = *((struct list_head * const *)__cil_tmp49); |
346 | __cil_tmp51 = (unsigned int )__cil_tmp50; |
347 | __cil_tmp52 = __cil_tmp51 == __cil_tmp46; |
348 | if (! __cil_tmp52) { |
349 | { |
350 | fail(); |
351 | } |
352 | } else { |
353 | } |
354 | } |
355 | goto while_8_break; |
356 | } |
357 | while_8_break: ; |
358 | } |
359 | { |
360 | while (1) { |
361 | while_9_continue: ; |
362 | { |
363 | __cil_tmp53 = (unsigned int )node; |
364 | __cil_tmp54 = __cil_tmp53 + 4; |
365 | __cil_tmp55 = (struct list_head const *)__cil_tmp54; |
366 | __cil_tmp56 = (unsigned int )__cil_tmp55; |
367 | __cil_tmp57 = (unsigned int )node; |
368 | __cil_tmp58 = __cil_tmp57 + 12; |
369 | __cil_tmp59 = *((struct list_head * const *)__cil_tmp58); |
370 | __cil_tmp60 = (unsigned int )__cil_tmp59; |
371 | __cil_tmp61 = __cil_tmp60 != __cil_tmp56; |
372 | if (! __cil_tmp61) { |
373 | { |
374 | fail(); |
375 | } |
376 | } else { |
377 | } |
378 | } |
379 | goto while_9_break; |
380 | } |
381 | while_9_break: ; |
382 | } |
383 | { |
384 | while (1) { |
385 | while_10_continue: ; |
386 | { |
387 | __cil_tmp62 = (unsigned int )node; |
388 | __cil_tmp63 = __cil_tmp62 + 4; |
389 | __cil_tmp64 = (struct list_head const *)__cil_tmp63; |
390 | __cil_tmp65 = (unsigned int )__cil_tmp64; |
391 | __cil_tmp66 = 12 + 4; |
392 | __cil_tmp67 = (unsigned int )node; |
393 | __cil_tmp68 = __cil_tmp67 + __cil_tmp66; |
394 | __cil_tmp69 = *((struct list_head * const *)__cil_tmp68); |
395 | __cil_tmp70 = (unsigned int )__cil_tmp69; |
396 | __cil_tmp71 = __cil_tmp70 != __cil_tmp65; |
397 | if (! __cil_tmp71) { |
398 | { |
399 | fail(); |
400 | } |
401 | } else { |
402 | } |
403 | } |
404 | goto while_10_break; |
405 | } |
406 | while_10_break: ; |
407 | } |
408 | { |
409 | while (1) { |
410 | while_11_continue: ; |
411 | { |
412 | __cil_tmp72 = (struct node const *)head; |
413 | __cil_tmp73 = (unsigned int )__cil_tmp72; |
414 | __cil_tmp74 = (unsigned int )node; |
415 | __cil_tmp75 = __cil_tmp74 != __cil_tmp73; |
416 | if (! __cil_tmp75) { |
417 | { |
418 | fail(); |
419 | } |
420 | } else { |
421 | } |
422 | } |
423 | goto while_11_break; |
424 | } |
425 | while_11_break: ; |
426 | } |
427 | { |
428 | while (1) { |
429 | while_12_continue: ; |
430 | { |
431 | __cil_tmp76 = (unsigned int )node; |
432 | __cil_tmp77 = __cil_tmp76 + 4; |
433 | __cil_tmp78 = (struct list_head const *)__cil_tmp77; |
434 | __cil_tmp79 = (struct node const *)__cil_tmp78; |
435 | __cil_tmp80 = (unsigned int )__cil_tmp79; |
436 | __cil_tmp81 = (unsigned int )node; |
437 | __cil_tmp82 = __cil_tmp81 != __cil_tmp80; |
438 | if (! __cil_tmp82) { |
439 | { |
440 | fail(); |
441 | } |
442 | } else { |
443 | } |
444 | } |
445 | goto while_12_break; |
446 | } |
447 | while_12_break: ; |
448 | } |
449 | { |
450 | while (1) { |
451 | while_13_continue: ; |
452 | { |
453 | __cil_tmp83 = (int const *)node; |
454 | __cil_tmp84 = (struct node const *)__cil_tmp83; |
455 | __cil_tmp85 = (unsigned int )__cil_tmp84; |
456 | __cil_tmp86 = (unsigned int )node; |
457 | __cil_tmp87 = __cil_tmp86 == __cil_tmp85; |
458 | if (! __cil_tmp87) { |
459 | { |
460 | fail(); |
461 | } |
462 | } else { |
463 | } |
464 | } |
465 | goto while_13_break; |
466 | } |
467 | while_13_break: ; |
468 | } |
469 | { |
470 | while (1) { |
471 | while_14_continue: ; |
472 | { |
473 | __cil_tmp88 = (unsigned int )node; |
474 | __cil_tmp89 = __cil_tmp88 + 4; |
475 | __cil_tmp90 = *((struct list_head * const *)__cil_tmp89); |
476 | __cil_tmp91 = (unsigned int )__cil_tmp90; |
477 | __cil_tmp92 = __cil_tmp91 + 4; |
478 | __cil_tmp93 = *((struct list_head **)__cil_tmp92); |
479 | __cil_tmp94 = (unsigned int )__cil_tmp93; |
480 | __cil_tmp95 = (unsigned int )head; |
481 | __cil_tmp96 = __cil_tmp95 == __cil_tmp94; |
482 | if (! __cil_tmp96) { |
483 | { |
484 | fail(); |
485 | } |
486 | } else { |
487 | } |
488 | } |
489 | goto while_14_break; |
490 | } |
491 | while_14_break: ; |
492 | } |
493 | { |
494 | while (1) { |
495 | while_15_continue: ; |
496 | { |
497 | __cil_tmp97 = 4 + 4; |
498 | __cil_tmp98 = (unsigned int )node; |
499 | __cil_tmp99 = __cil_tmp98 + __cil_tmp97; |
500 | __cil_tmp100 = *((struct list_head * const *)__cil_tmp99); |
501 | __cil_tmp101 = *((struct list_head **)__cil_tmp100); |
502 | __cil_tmp102 = (unsigned int )__cil_tmp101; |
503 | __cil_tmp103 = (unsigned int )head; |
504 | __cil_tmp104 = __cil_tmp103 == __cil_tmp102; |
505 | if (! __cil_tmp104) { |
506 | { |
507 | fail(); |
508 | } |
509 | } else { |
510 | } |
511 | } |
512 | goto while_15_break; |
513 | } |
514 | while_15_break: ; |
515 | } |
516 | __cil_tmp105 = *((struct list_head * const *)head); |
517 | head = (struct list_head const *)__cil_tmp105; |
518 | { |
519 | while (1) { |
520 | while_16_continue: ; |
521 | { |
522 | __cil_tmp106 = (unsigned int )head; |
523 | __cil_tmp107 = (unsigned int )node; |
524 | __cil_tmp108 = __cil_tmp107 + 4; |
525 | __cil_tmp109 = (struct list_head const *)__cil_tmp108; |
526 | __cil_tmp110 = (unsigned int )__cil_tmp109; |
527 | if (__cil_tmp110 != __cil_tmp106) { |
528 | } else { |
529 | goto while_16_break; |
530 | } |
531 | } |
532 | __cil_tmp111 = *((struct list_head * const *)head); |
533 | head = (struct list_head const *)__cil_tmp111; |
534 | } |
535 | while_16_break: ; |
536 | } |
537 | { |
538 | while (1) { |
539 | while_17_continue: ; |
540 | { |
541 | __cil_tmp112 = (unsigned int )node; |
542 | __cil_tmp113 = (struct node *)0; |
543 | __cil_tmp114 = (unsigned int )__cil_tmp113; |
544 | __cil_tmp115 = __cil_tmp114 + 4; |
545 | __cil_tmp116 = (struct list_head *)__cil_tmp115; |
546 | __cil_tmp117 = (unsigned long )__cil_tmp116; |
547 | __cil_tmp118 = (char *)head; |
548 | __cil_tmp119 = __cil_tmp118 - __cil_tmp117; |
549 | __cil_tmp120 = (struct node *)__cil_tmp119; |
550 | __cil_tmp121 = (unsigned int )__cil_tmp120; |
551 | __cil_tmp122 = __cil_tmp121 == __cil_tmp112; |
552 | if (! __cil_tmp122) { |
553 | { |
554 | fail(); |
555 | } |
556 | } else { |
557 | } |
558 | } |
559 | goto while_17_break; |
560 | } |
561 | while_17_break: ; |
562 | } |
563 | return; |
564 | } |
565 | } |
566 | __inline static void __list_add(struct list_head *new , struct list_head *prev , struct list_head *next ) |
567 | { unsigned int __cil_tmp4 ; |
568 | unsigned int __cil_tmp5 ; |
569 | unsigned int __cil_tmp6 ; |
570 | unsigned int __cil_tmp7 ; |
571 | { |
572 | __cil_tmp4 = (unsigned int )next; |
573 | __cil_tmp5 = __cil_tmp4 + 4; |
574 | *((struct list_head **)__cil_tmp5) = new; |
575 | *((struct list_head **)new) = next; |
576 | __cil_tmp6 = (unsigned int )new; |
577 | __cil_tmp7 = __cil_tmp6 + 4; |
578 | *((struct list_head **)__cil_tmp7) = prev; |
579 | *((struct list_head **)prev) = new; |
580 | return; |
581 | } |
582 | } |
583 | __inline static void __list_del(struct list_head *prev , struct list_head *next ) |
584 | { unsigned int __cil_tmp3 ; |
585 | unsigned int __cil_tmp4 ; |
586 | { |
587 | __cil_tmp3 = (unsigned int )next; |
588 | __cil_tmp4 = __cil_tmp3 + 4; |
589 | *((struct list_head **)__cil_tmp4) = prev; |
590 | *((struct list_head **)prev) = next; |
591 | return; |
592 | } |
593 | } |
594 | __inline static void list_add(struct list_head *new , struct list_head *head ) |
595 | { struct list_head *__cil_tmp3 ; |
596 | { |
597 | { |
598 | __cil_tmp3 = *((struct list_head **)head); |
599 | __list_add(new, head, __cil_tmp3); |
600 | } |
601 | return; |
602 | } |
603 | } |
604 | __inline static void list_move(struct list_head *list , struct list_head *head ) |
605 | { unsigned int __cil_tmp3 ; |
606 | unsigned int __cil_tmp4 ; |
607 | struct list_head *__cil_tmp5 ; |
608 | struct list_head *__cil_tmp6 ; |
609 | { |
610 | { |
611 | __cil_tmp3 = (unsigned int )list; |
612 | __cil_tmp4 = __cil_tmp3 + 4; |
613 | __cil_tmp5 = *((struct list_head **)__cil_tmp4); |
614 | __cil_tmp6 = *((struct list_head **)list); |
615 | __list_del(__cil_tmp5, __cil_tmp6); |
616 | list_add(list, head); |
617 | } |
618 | return; |
619 | } |
620 | } |
621 | static void gl_insert(int value ) |
622 | { struct node *node ; |
623 | void *tmp ; |
624 | unsigned int __cil_tmp4 ; |
625 | unsigned int __cil_tmp5 ; |
626 | unsigned int __cil_tmp6 ; |
627 | struct list_head *__cil_tmp7 ; |
628 | unsigned int __cil_tmp8 ; |
629 | unsigned int __cil_tmp9 ; |
630 | unsigned int __cil_tmp10 ; |
631 | unsigned int __cil_tmp11 ; |
632 | unsigned int __cil_tmp12 ; |
633 | unsigned int __cil_tmp13 ; |
634 | unsigned int __cil_tmp14 ; |
635 | unsigned int __cil_tmp15 ; |
636 | { |
637 | { |
638 | __cil_tmp4 = (unsigned int )20UL; |
639 | tmp = malloc(__cil_tmp4); |
640 | node = (struct node *)tmp; |
641 | } |
642 | if (! node) { |
643 | { |
644 | abort(); |
645 | } |
646 | } else { |
647 | } |
648 | { |
649 | *((int *)node) = value; |
650 | __cil_tmp5 = (unsigned int )node; |
651 | __cil_tmp6 = __cil_tmp5 + 4; |
652 | __cil_tmp7 = (struct list_head *)__cil_tmp6; |
653 | list_add(__cil_tmp7, & gl_list); |
654 | } |
655 | { |
656 | while (1) { |
657 | while_18_continue: ; |
658 | __cil_tmp8 = (unsigned int )node; |
659 | __cil_tmp9 = __cil_tmp8 + 12; |
660 | __cil_tmp10 = (unsigned int )node; |
661 | __cil_tmp11 = __cil_tmp10 + 12; |
662 | *((struct list_head **)__cil_tmp9) = (struct list_head *)__cil_tmp11; |
663 | __cil_tmp12 = (unsigned int )node; |
664 | __cil_tmp13 = __cil_tmp12 + 12; |
665 | __cil_tmp14 = (unsigned int )node; |
666 | __cil_tmp15 = __cil_tmp14 + 12; |
667 | *((struct list_head **)__cil_tmp13) = (struct list_head *)__cil_tmp15; |
668 | goto while_18_break; |
669 | } |
670 | while_18_break: ; |
671 | } |
672 | return; |
673 | } |
674 | } |
675 | static void gl_read(void) |
676 | { int tmp ; |
677 | int tmp___0 ; |
678 | { |
679 | { |
680 | while (1) { |
681 | while_19_continue: ; |
682 | { |
683 | tmp = __VERIFIER_nondet_int(); |
684 | gl_insert(tmp); |
685 | tmp___0 = __VERIFIER_nondet_int(); |
686 | } |
687 | if (tmp___0) { |
688 | } else { |
689 | goto while_19_break; |
690 | } |
691 | } |
692 | while_19_break: ; |
693 | } |
694 | return; |
695 | } |
696 | } |
697 | static void gl_destroy(void) |
698 | { struct list_head *next ; |
699 | struct list_head *__cil_tmp2 ; |
700 | unsigned int __cil_tmp3 ; |
701 | unsigned int __cil_tmp4 ; |
702 | struct list_head *__cil_tmp5 ; |
703 | struct node *__cil_tmp6 ; |
704 | unsigned int __cil_tmp7 ; |
705 | unsigned int __cil_tmp8 ; |
706 | struct list_head *__cil_tmp9 ; |
707 | unsigned long __cil_tmp10 ; |
708 | char *__cil_tmp11 ; |
709 | char *__cil_tmp12 ; |
710 | struct node *__cil_tmp13 ; |
711 | void *__cil_tmp14 ; |
712 | { |
713 | { |
714 | while (1) { |
715 | while_20_continue: ; |
716 | __cil_tmp2 = & gl_list; |
717 | next = *((struct list_head **)__cil_tmp2); |
718 | { |
719 | __cil_tmp3 = (unsigned int )next; |
720 | __cil_tmp4 = (unsigned int )(& gl_list); |
721 | if (__cil_tmp4 != __cil_tmp3) { |
722 | } else { |
723 | goto while_20_break; |
724 | } |
725 | } |
726 | { |
727 | __cil_tmp5 = & gl_list; |
728 | *((struct list_head **)__cil_tmp5) = *((struct list_head **)next); |
729 | __cil_tmp6 = (struct node *)0; |
730 | __cil_tmp7 = (unsigned int )__cil_tmp6; |
731 | __cil_tmp8 = __cil_tmp7 + 4; |
732 | __cil_tmp9 = (struct list_head *)__cil_tmp8; |
733 | __cil_tmp10 = (unsigned long )__cil_tmp9; |
734 | __cil_tmp11 = (char *)next; |
735 | __cil_tmp12 = __cil_tmp11 - __cil_tmp10; |
736 | __cil_tmp13 = (struct node *)__cil_tmp12; |
737 | __cil_tmp14 = (void *)__cil_tmp13; |
738 | free(__cil_tmp14); |
739 | } |
740 | } |
741 | while_20_break: ; |
742 | } |
743 | return; |
744 | } |
745 | } |
746 | static int val_from_node(struct list_head *head ) |
747 | { struct node *entry ; |
748 | struct node *__cil_tmp3 ; |
749 | unsigned int __cil_tmp4 ; |
750 | unsigned int __cil_tmp5 ; |
751 | struct list_head *__cil_tmp6 ; |
752 | unsigned long __cil_tmp7 ; |
753 | char *__cil_tmp8 ; |
754 | char *__cil_tmp9 ; |
755 | { |
756 | __cil_tmp3 = (struct node *)0; |
757 | __cil_tmp4 = (unsigned int )__cil_tmp3; |
758 | __cil_tmp5 = __cil_tmp4 + 4; |
759 | __cil_tmp6 = (struct list_head *)__cil_tmp5; |
760 | __cil_tmp7 = (unsigned long )__cil_tmp6; |
761 | __cil_tmp8 = (char *)head; |
762 | __cil_tmp9 = __cil_tmp8 - __cil_tmp7; |
763 | entry = (struct node *)__cil_tmp9; |
764 | return (*((int *)entry)); |
765 | } |
766 | } |
767 | static _Bool gl_sort_pass(void) |
768 | { _Bool any_change ; |
769 | struct list_head *pos0 ; |
770 | struct list_head *pos1 ; |
771 | int val0 ; |
772 | int tmp ; |
773 | int val1 ; |
774 | int tmp___0 ; |
775 | struct list_head *__cil_tmp8 ; |
776 | unsigned int __cil_tmp9 ; |
777 | unsigned int __cil_tmp10 ; |
778 | { |
779 | any_change = (_Bool)0; |
780 | __cil_tmp8 = & gl_list; |
781 | pos0 = *((struct list_head **)__cil_tmp8); |
782 | { |
783 | while (1) { |
784 | while_21_continue: ; |
785 | pos1 = *((struct list_head **)pos0); |
786 | { |
787 | __cil_tmp9 = (unsigned int )pos1; |
788 | __cil_tmp10 = (unsigned int )(& gl_list); |
789 | if (__cil_tmp10 != __cil_tmp9) { |
790 | } else { |
791 | goto while_21_break; |
792 | } |
793 | } |
794 | { |
795 | tmp = val_from_node(pos0); |
796 | val0 = tmp; |
797 | tmp___0 = val_from_node(pos1); |
798 | val1 = tmp___0; |
799 | } |
800 | if (val0 <= val1) { |
801 | pos0 = pos1; |
802 | goto while_21_continue; |
803 | } else { |
804 | } |
805 | { |
806 | any_change = (_Bool)1; |
807 | list_move(pos0, pos1); |
808 | } |
809 | } |
810 | while_21_break: ; |
811 | } |
812 | return (any_change); |
813 | } |
814 | } |
815 | static void gl_sort(void) |
816 | { _Bool tmp ; |
817 | { |
818 | { |
819 | while (1) { |
820 | while_22_continue: ; |
821 | { |
822 | tmp = gl_sort_pass(); |
823 | } |
824 | if (tmp) { |
825 | } else { |
826 | goto while_22_break; |
827 | } |
828 | } |
829 | while_22_break: ; |
830 | } |
831 | return; |
832 | } |
833 | } |
834 | int main(void) |
835 | { struct list_head const *__cil_tmp1 ; |
836 | struct list_head const *__cil_tmp2 ; |
837 | { |
838 | { |
839 | gl_read(); |
840 | __cil_tmp1 = (struct list_head const *)(& gl_list); |
841 | inspect(__cil_tmp1); |
842 | gl_sort(); |
843 | __cil_tmp2 = (struct list_head const *)(& gl_list); |
844 | inspect(__cil_tmp2); |
845 | gl_destroy(); |
846 | } |
847 | return (0); |
848 | } |
849 | } |
| Date | Time | Level | Component | Message |
|---|---|---|---|---|
| 2021-11-23 | 11:33:44:501 | INFO | CPAMain.detectFrontendLanguageIfNecessary | Language C detected and set for analysis |
| 2021-11-23 | 11:33:44:513 | INFO | ResourceLimitChecker.fromConfiguration | Using the following resource limits: CPU-time limit of 900s |
| 2021-11-23 | 11:33:44:563 | INFO | CPAchecker.run | CPAchecker 2.1 / predicateAnalysis (OpenJDK 64-Bit Server VM 11.0.11) started |
| 2021-11-23 | 11:33:44:574 | INFO | CPAchecker.parse | Parsing CFA from file(s) "test/programs/benchmarks/loops/bubble_sort-2.i" |
| 2021-11-23 | 11:33:45:714 | INFO | PredicateCPA PredicateCPA.<init> | Using predicate analysis with MathSAT5 version 5.6.6 (218275631c24) (Apr 23 2021 08:35:29, gmp 6.1.2, gcc 7.5.0, 64-bit, reentrant) and JFactory 1.21. |
| 2021-11-23 | 11:33:45:804 | INFO | PredicateCPA PredicateCPARefiner.<init> | Using refinement for predicate analysis with PredicateAbstractionRefinementStrategy strategy. |
| 2021-11-23 | 11:33:45:825 | INFO | CPAchecker.runAlgorithm | Starting analysis ... |
| 2021-11-23 | 11:33:46:599 | INFO | CPAchecker.runAlgorithm | Stopping analysis ... |
| Statistics Name | Statistics Value | Additional Value |
|---|---|---|
| PredicateCPA statistics | ||
| Number of abstractions | 11 | 1% of all post computations |
| Times abstraction was reused | 0 | |
| Because of function entry/exit | 0 | 0% |
| Because of loop head | 11 | 100% |
| Because of join nodes | 0 | 0% |
| Because of threshold | 0 | 0% |
| Because of target state | 0 | 0% |
| Times precision was empty | 6 | 55% |
| Times precision was {false} | 3 | 27% |
| Times result was cached | 0 | 0% |
| Times cartesian abs was used | 0 | 0% |
| Times boolean abs was used | 2 | 18% |
| Times result was 'false' | 2 | 18% |
| Number of strengthen sat checks | 0 | |
| Number of coverage checks | 6 | |
| BDD entailment checks | 6 | |
| Number of SMT sat checks | 0 | |
| trivial | 0 | |
| cached | 0 | |
| Max ABE block size | 188 | |
| Avg ABE block size | 97.09 | sum: 1068, count: 11, min: 5, max: 188 |
| Number of predicates discovered | 19 | |
| Number of abstraction locations | 2 | |
| Max number of predicates per location | 2 | |
| Avg number of predicates per location | 1 | |
| Total predicates per abstraction | 7 | |
| Max number of predicates per abstraction | 2 | |
| Avg number of predicates per abstraction | 1.40 | |
| Number of irrelevant predicates | 3 | 43% |
| Number of preds handled by boolean abs | 4 | 57% |
| Total number of models for allsat | 2 | |
| Max number of models for allsat | 1 | |
| Avg number of models for allsat | 1.00 | |
| Time for post operator | 0.185s | |
| Time for path formula creation | 0.173s | |
| Time for strengthen operator | 0.006s | |
| Time for prec operator | 0.094s | |
| Time for abstraction | 0.094s | Max: 0.040s, Count: 11 |
| Boolean abstraction | 0.007s | |
| Solving time | 0.049s | Max: 0.034s |
| Model enumeration time | 0.001s | |
| Time for BDD construction | 0.001s | Max: 0.001s |
| Time for coverage checks | 0.003s | |
| Time for BDD entailment checks | 0.003s | |
| Total time for SMT solver (w/o itp) | 0.050s | |
| Number of path formula cache hits | 496 | 49% |
| Inside post operator | ||
| Inside path formula creation | ||
| Time for path formula computation | 0.195s | |
| Total number of created targets for pointer analysis | 0 | |
| Number of BDD nodes | 203 | |
| Size of BDD node table | 62921 | |
| Size of BDD cache | 6299 | |
| Size of BDD node cleanup queue | 0.09 | sum: 10, count: 114, min: 0, max: 10 |
| Time for BDD node cleanup | 0.001s | |
| Time for BDD garbage collection | 0.000s | in 0 runs |
| KeyValue statistics | ||
| Init. function predicates | 0 | |
| Init. global predicates | 0 | |
| Init. location predicates | 0 | |
| Invariant Generation statistics | ||
| AutomatonAnalysis (AssertionAutomaton) statistics | ||
| Number of states | 1 | |
| Total time for successor computation | 0.017s | |
| Automaton transfers with branching | 0 | |
| Automaton transfer successors | 1.00 | sum: 734, count: 734, min: 1, max: 1 [1 x 734] |
| Number of states with assumption transitions | 0 | |
| AutomatonAnalysis (ErrorLabelAutomaton) statistics | ||
| Number of states | 1 | |
| Total time for successor computation | 0.003s | |
| Automaton transfers with branching | 0 | |
| Automaton transfer successors | 1.00 | sum: 734, count: 734, min: 1, max: 1 [1 x 734] |
| Number of states with assumption transitions | 0 | |
| AutomatonAnalysis (TerminatingFunctions) statistics | ||
| Number of states | 1 | |
| Total time for successor computation | 0.002s | |
| Automaton transfers with branching | 0 | |
| Automaton transfer successors | 1.00 | sum: 731, count: 734, min: 0, max: 1 [0 x 3, 1 x 731] |
| Number of states with assumption transitions | 0 | |
| CPA algorithm statistics | ||
| Number of iterations | 152 | |
| Max size of waitlist | 2 | |
| Average size of waitlist | 1 | |
| ReversePostorderSortedWaitlist | 0.00 | sum: 0, count: 130, min: 0, max: 0 |
| CallstackSortedWaitlist | 13.33 | sum: 40, count: 3, min: 6, max: 22 |
| Number of computed successors | 160 | |
| Max successors for one state | 2 | |
| Number of times merged | 0 | |
| Number of times stopped | 3 | |
| Number of times breaked | 3 | |
| Total time for CPA algorithm | 0.394s | Max: 0.244s |
| Time for choose from waitlist | 0.007s | |
| Time for precision adjustment | 0.101s | |
| Time for transfer relation | 0.275s | |
| Time for merge operator | 0.004s | |
| Time for stop operator | 0.002s | |
| Time for adding to reached set | 0.004s | |
| Static Predicate Refiner statistics | ||
| Number of predicates found statically | 16 | count: 1, min: 16, max: 16, avg: 16.00 |
| Total time for static refinement | 0.047s | |
| Time for path feasibility check | 0.009s | |
| Time for predicate extraction from CFA | 0.028s | |
| Time for ARG update | 0.007s | |
| PredicateCPARefiner statistics | ||
| Number of predicate refinements | 2 | |
| Avg. length of target path (in blocks) | 2.00 | sum: 4, count: 2, min: 2, max: 2 |
| Number of infeasible sliced prefixes | 0 | count: 0, min: 0, max: 0, avg: 0.00 |
| Time for refinement | 0.312s | |
| Counterexample analysis | 0.193s | Max: 0.146s, Calls: 3 |
| Refinement sat check | 0.165s | |
| Interpolant computation | 0.003s | |
| Path-formulas extraction | 0.000s | |
| Error path post-processing | 0.122s | |
| Predicate-Abstraction Refiner statistics | ||
| Predicate creation | 0.001s | |
| Precision update | 0.003s | |
| ARG update | 0.001s | |
| Length of refined path (in blocks) | 2.00 | sum: 2, count: 1, min: 2, max: 2 |
| Number of affected states | 1 | count: 1, min: 1, max: 1, avg: 1.00 |
| Length (states) of path with itp 'true' | 0 | count: 1, min: 0, max: 0, avg: 0.00 |
| Length (states) of path with itp non-trivial itp | 1 | count: 1, min: 1, max: 1, avg: 1.00 |
| Length (states) of path with itp 'false' | 0 | count: 1, min: 0, max: 0, avg: 0.00 |
| Different non-trivial interpolants along paths | 0 | count: 1, min: 0, max: 0, avg: 0.00 |
| Equal non-trivial interpolants along paths | 0 | count: 1, min: 0, max: 0, avg: 0.00 |
| Number of refs with location-based cutoff | 0 | |
| CEGAR algorithm statistics | ||
| Number of CEGAR refinements | 3 | |
| Number of successful refinements | 2 | |
| Number of failed refinements | 0 | |
| Max. size of reached set before ref. | 66 | |
| Max. size of reached set after ref. | 5 | |
| Avg. size of reached set before ref. | 54.00 | |
| Avg. size of reached set after ref. | 3.00 | |
| Total time for CEGAR algorithm | 0.773s | |
| Time for refinements | 0.379s | |
| Average time for refinement | 0.126s | |
| Max time for refinement | 0.269s | |
| Code Coverage | ||
| Function coverage | 0.500 | |
| Visited lines | 230 | |
| Total lines | 554 | |
| Line coverage | 0.415 | |
| Visited conditions | 10 | |
| Total conditions | 48 | |
| Condition coverage | 0.208 | |
| CPAchecker general statistics | ||
| Number of program locations | 673 | |
| Number of CFA edges (per node) | 682 | count: 673, min: 0, max: 2, avg: 1.01 |
| Number of relevant variables | 198 | |
| Number of functions | 14 | |
| Number of loops (and loop nodes) | 6 | sum: 69, min: 4, max: 21, avg: 11.50 |
| Size of reached set | 66 | |
| Number of reached locations | 62 | 9% |
| Avg states per location | 1 | |
| Max states per location | 3 | at node N9 |
| Number of reached functions | 7 | 50% |
| Number of partitions | 66 | |
| Avg size of partitions | 1 | |
| Max size of partitions | 1 | |
| Number of target states | 1 | |
| Size of final wait list | 2 | |
| Time for analysis setup | 1.251s | |
| Time for loading CPAs | 0.386s | |
| Time for loading parser | 0.171s | |
| Time for CFA construction | 0.622s | |
| Time for parsing file(s) | 0.259s | |
| Time for AST to CFA | 0.182s | |
| Time for CFA sanity check | 0.018s | |
| Time for post-processing | 0.131s | |
| Time for CFA export | 1.141s | |
| Time for function pointers resolving | 0.004s | |
| Function calls via function pointers | 0 | count: 1, min: 0, max: 0, avg: 0.00 |
| Instrumented function pointer calls | 0 | count: 1, min: 0, max: 0, avg: 0.00 |
| Function calls with function pointer arguments | 0 | count: 1, min: 0, max: 0, avg: 0.00 |
| Instrumented function pointer arguments | 0 | count: 1, min: 0, max: 0, avg: 0.00 |
| Time for classifying variables | 0.078s | |
| Time for collecting variables | 0.035s | |
| Time for solving dependencies | 0.000s | |
| Time for building hierarchy | 0.001s | |
| Time for building classification | 0.029s | |
| Time for exporting data | 0.013s | |
| Time for Analysis | 0.774s | |
| CPU time for analysis | 2.690s | |
| Time for analyzing result | 0.001s | |
| Total time for CPAchecker | 2.026s | |
| Total CPU time for CPAchecker | 6.710s | |
| Time for statistics | 0.045s | |
| Time for Garbage Collector | 0.057s | in 5 runs |
| Garbage Collector(s) used | G1 Old Generation, G1 Young Generation | |
| Used heap memory | 59MB ( 56 MiB) max; 35MB ( 33 MiB) avg; 71MB ( 68 MiB) peak | |
| Used non-heap memory | 44MB ( 42 MiB) max; 30MB ( 29 MiB) avg; 45MB ( 42 MiB) peak | |
| Used in G1 Old Gen pool | 18MB ( 17 MiB) max; 11MB ( 10 MiB) avg; 18MB ( 17 MiB) peak | |
| Allocated heap memory | 526MB ( 502 MiB) max; 526MB ( 501 MiB) avg | |
| Allocated non-heap memory | 47MB ( 45 MiB) max; 34MB ( 33 MiB) avg | |
| Total process virtual memory | 4704MB ( 4486 MiB) max; 4565MB ( 4354 MiB) avg |
| # | Configuration Name | Configuration Value |
|---|---|---|
| 1 | analysis.algorithm.CEGAR | true |
| 2 | analysis.name | predicateAnalysis |
| 3 | analysis.programNames | test/programs/benchmarks/loops/bubble_sort-2.i |
| 4 | analysis.traversal.order | bfs |
| 5 | analysis.traversal.useCallstack | true |
| 6 | analysis.traversal.useReversePostorder | true |
| 7 | ARGCPA.cpa | cpa.composite.CompositeCPA |
| 8 | cegar.refiner | cpa.predicate.PredicateRefiner |
| 9 | CompositeCPA.cpas | cpa.location.LocationCPA, cpa.callstack.CallstackCPA, cpa.functionpointer.FunctionPointerCPA, cpa.predicate.PredicateCPA, $specification |
| 10 | cpa | cpa.arg.ARGCPA |
| 11 | cpa.composite.aggregateBasicBlocks | true |
| 12 | cpa.predicate.blk.alwaysAtFunctions | false |
| 13 | cpa.predicate.blk.alwaysAtLoops | true |
| 14 | cpa.predicate.refinement.performInitialStaticRefinement | true |
| 15 | language | C |
| 16 | limits.time.cpu | 900s |
| 17 | log.level | INFO |
| 18 | specification | specification/default.spc |
This table was generated by CPAchecker. For feedback, questions, and bug reports please use our issue tracker.
License: Apache 2.0 License
Source: {{dependency.repository}}
{{dependency.copyright}}
License:
Full text of license
{{dependencies.licenses[dependency.licenseId]}}