1
2
3
4#line 211 "/usr/lib/gcc/x86_64-pc-linux-gnu/4.5.3/include/stddef.h"
5typedef unsigned int size_t;
6#line 17 "test-0180.c"
7struct list_head {
8 struct list_head *next ;
9 struct list_head *prev ;
10};
11#line 33 "test-0180.c"
12struct node {
13 int value ;
14 struct list_head linkage ;
15 struct list_head nested ;
16};
17#line 471 "/usr/include/stdlib.h"
18extern __attribute__((__nothrow__)) void *malloc(size_t __size ) __attribute__((__malloc__)) ;
19#line 488
20extern __attribute__((__nothrow__)) void free(void *__ptr ) ;
21#line 514
22extern __attribute__((__nothrow__, __noreturn__)) void abort(void) ;
23#line 5 "test-0180.c"
24extern int __VERIFIER_nondet_int(void) ;
25#line 7 "test-0180.c"
26static void fail(void)
27{
28
29 {
30 ERROR:
31 goto ERROR;
32}
33}
34#line 39 "test-0180.c"
35struct list_head gl_list = {& gl_list, & gl_list};
36#line 41 "test-0180.c"
37static void inspect(struct list_head const *head )
38{ struct node const *node ;
39 unsigned int __cil_tmp3 ;
40 struct list_head *__cil_tmp4 ;
41 unsigned int __cil_tmp5 ;
42 int __cil_tmp6 ;
43 unsigned int __cil_tmp7 ;
44 unsigned int __cil_tmp8 ;
45 unsigned int __cil_tmp9 ;
46 struct list_head *__cil_tmp10 ;
47 unsigned int __cil_tmp11 ;
48 int __cil_tmp12 ;
49 unsigned int __cil_tmp13 ;
50 unsigned int __cil_tmp14 ;
51 struct list_head *__cil_tmp15 ;
52 unsigned int __cil_tmp16 ;
53 struct list_head *__cil_tmp17 ;
54 unsigned int __cil_tmp18 ;
55 int __cil_tmp19 ;
56 unsigned int __cil_tmp20 ;
57 unsigned int __cil_tmp21 ;
58 unsigned int __cil_tmp22 ;
59 struct list_head *__cil_tmp23 ;
60 unsigned int __cil_tmp24 ;
61 int __cil_tmp25 ;
62 struct node *__cil_tmp26 ;
63 unsigned int __cil_tmp27 ;
64 unsigned int __cil_tmp28 ;
65 struct list_head *__cil_tmp29 ;
66 unsigned long __cil_tmp30 ;
67 char *__cil_tmp31 ;
68 char *__cil_tmp32 ;
69 struct node *__cil_tmp33 ;
70 unsigned int __cil_tmp34 ;
71 unsigned int __cil_tmp35 ;
72 struct list_head const *__cil_tmp36 ;
73 unsigned int __cil_tmp37 ;
74 unsigned int __cil_tmp38 ;
75 unsigned int __cil_tmp39 ;
76 struct list_head *__cil_tmp40 ;
77 unsigned int __cil_tmp41 ;
78 int __cil_tmp42 ;
79 unsigned int __cil_tmp43 ;
80 unsigned int __cil_tmp44 ;
81 struct list_head const *__cil_tmp45 ;
82 unsigned int __cil_tmp46 ;
83 unsigned int __cil_tmp47 ;
84 unsigned int __cil_tmp48 ;
85 unsigned int __cil_tmp49 ;
86 struct list_head *__cil_tmp50 ;
87 unsigned int __cil_tmp51 ;
88 int __cil_tmp52 ;
89 unsigned int __cil_tmp53 ;
90 unsigned int __cil_tmp54 ;
91 struct list_head const *__cil_tmp55 ;
92 unsigned int __cil_tmp56 ;
93 unsigned int __cil_tmp57 ;
94 unsigned int __cil_tmp58 ;
95 struct list_head *__cil_tmp59 ;
96 unsigned int __cil_tmp60 ;
97 int __cil_tmp61 ;
98 unsigned int __cil_tmp62 ;
99 unsigned int __cil_tmp63 ;
100 struct list_head const *__cil_tmp64 ;
101 unsigned int __cil_tmp65 ;
102 unsigned int __cil_tmp66 ;
103 unsigned int __cil_tmp67 ;
104 unsigned int __cil_tmp68 ;
105 struct list_head *__cil_tmp69 ;
106 unsigned int __cil_tmp70 ;
107 int __cil_tmp71 ;
108 struct node const *__cil_tmp72 ;
109 unsigned int __cil_tmp73 ;
110 unsigned int __cil_tmp74 ;
111 int __cil_tmp75 ;
112 unsigned int __cil_tmp76 ;
113 unsigned int __cil_tmp77 ;
114 struct list_head const *__cil_tmp78 ;
115 struct node const *__cil_tmp79 ;
116 unsigned int __cil_tmp80 ;
117 unsigned int __cil_tmp81 ;
118 int __cil_tmp82 ;
119 int const *__cil_tmp83 ;
120 struct node const *__cil_tmp84 ;
121 unsigned int __cil_tmp85 ;
122 unsigned int __cil_tmp86 ;
123 int __cil_tmp87 ;
124 unsigned int __cil_tmp88 ;
125 unsigned int __cil_tmp89 ;
126 struct list_head *__cil_tmp90 ;
127 unsigned int __cil_tmp91 ;
128 unsigned int __cil_tmp92 ;
129 struct list_head *__cil_tmp93 ;
130 unsigned int __cil_tmp94 ;
131 unsigned int __cil_tmp95 ;
132 int __cil_tmp96 ;
133 unsigned int __cil_tmp97 ;
134 unsigned int __cil_tmp98 ;
135 unsigned int __cil_tmp99 ;
136 struct list_head *__cil_tmp100 ;
137 struct list_head *__cil_tmp101 ;
138 unsigned int __cil_tmp102 ;
139 unsigned int __cil_tmp103 ;
140 int __cil_tmp104 ;
141 struct list_head *__cil_tmp105 ;
142 unsigned int __cil_tmp106 ;
143 unsigned int __cil_tmp107 ;
144 unsigned int __cil_tmp108 ;
145 struct list_head const *__cil_tmp109 ;
146 unsigned int __cil_tmp110 ;
147 struct list_head *__cil_tmp111 ;
148 unsigned int __cil_tmp112 ;
149 struct node *__cil_tmp113 ;
150 unsigned int __cil_tmp114 ;
151 unsigned int __cil_tmp115 ;
152 struct list_head *__cil_tmp116 ;
153 unsigned long __cil_tmp117 ;
154 char *__cil_tmp118 ;
155 char *__cil_tmp119 ;
156 struct node *__cil_tmp120 ;
157 unsigned int __cil_tmp121 ;
158 int __cil_tmp122 ;
159
160 {
161 {
162#line 44
163 while (1) {
164 while_0_continue: ;
165#line 44
166 if (! head) {
167 {
168#line 44
169 fail();
170 }
171 } else {
172
173 }
174 goto while_0_break;
175 }
176 while_0_break: ;
177 }
178 {
179#line 45
180 while (1) {
181 while_1_continue: ;
182 {
183#line 45
184 __cil_tmp3 = (unsigned int )head;
185#line 45
186 __cil_tmp4 = *((struct list_head * const *)head);
187#line 45
188 __cil_tmp5 = (unsigned int )__cil_tmp4;
189#line 45
190 __cil_tmp6 = __cil_tmp5 != __cil_tmp3;
191#line 45
192 if (! __cil_tmp6) {
193 {
194#line 45
195 fail();
196 }
197 } else {
198
199 }
200 }
201 goto while_1_break;
202 }
203 while_1_break: ;
204 }
205 {
206#line 46
207 while (1) {
208 while_2_continue: ;
209 {
210#line 46
211 __cil_tmp7 = (unsigned int )head;
212#line 46
213 __cil_tmp8 = (unsigned int )head;
214#line 46
215 __cil_tmp9 = __cil_tmp8 + 4;
216#line 46
217 __cil_tmp10 = *((struct list_head * const *)__cil_tmp9);
218#line 46
219 __cil_tmp11 = (unsigned int )__cil_tmp10;
220#line 46
221 __cil_tmp12 = __cil_tmp11 != __cil_tmp7;
222#line 46
223 if (! __cil_tmp12) {
224 {
225#line 46
226 fail();
227 }
228 } else {
229
230 }
231 }
232 goto while_2_break;
233 }
234 while_2_break: ;
235 }
236#line 49
237 __cil_tmp13 = (unsigned int )head;
238#line 49
239 __cil_tmp14 = __cil_tmp13 + 4;
240#line 49
241 __cil_tmp15 = *((struct list_head * const *)__cil_tmp14);
242#line 49
243 head = (struct list_head const *)__cil_tmp15;
244 {
245#line 50
246 while (1) {
247 while_3_continue: ;
248#line 50
249 if (! head) {
250 {
251#line 50
252 fail();
253 }
254 } else {
255
256 }
257 goto while_3_break;
258 }
259 while_3_break: ;
260 }
261 {
262#line 51
263 while (1) {
264 while_4_continue: ;
265 {
266#line 51
267 __cil_tmp16 = (unsigned int )head;
268#line 51
269 __cil_tmp17 = *((struct list_head * const *)head);
270#line 51
271 __cil_tmp18 = (unsigned int )__cil_tmp17;
272#line 51
273 __cil_tmp19 = __cil_tmp18 != __cil_tmp16;
274#line 51
275 if (! __cil_tmp19) {
276 {
277#line 51
278 fail();
279 }
280 } else {
281
282 }
283 }
284 goto while_4_break;
285 }
286 while_4_break: ;
287 }
288 {
289#line 52
290 while (1) {
291 while_5_continue: ;
292 {
293#line 52
294 __cil_tmp20 = (unsigned int )head;
295#line 52
296 __cil_tmp21 = (unsigned int )head;
297#line 52
298 __cil_tmp22 = __cil_tmp21 + 4;
299#line 52
300 __cil_tmp23 = *((struct list_head * const *)__cil_tmp22);
301#line 52
302 __cil_tmp24 = (unsigned int )__cil_tmp23;
303#line 52
304 __cil_tmp25 = __cil_tmp24 != __cil_tmp20;
305#line 52
306 if (! __cil_tmp25) {
307 {
308#line 52
309 fail();
310 }
311 } else {
312
313 }
314 }
315 goto while_5_break;
316 }
317 while_5_break: ;
318 }
319#line 55
320 __cil_tmp26 = (struct node *)0;
321#line 55
322 __cil_tmp27 = (unsigned int )__cil_tmp26;
323#line 55
324 __cil_tmp28 = __cil_tmp27 + 4;
325#line 55
326 __cil_tmp29 = (struct list_head *)__cil_tmp28;
327#line 55
328 __cil_tmp30 = (unsigned long )__cil_tmp29;
329#line 55
330 __cil_tmp31 = (char *)head;
331#line 55
332 __cil_tmp32 = __cil_tmp31 - __cil_tmp30;
333#line 55
334 __cil_tmp33 = (struct node *)__cil_tmp32;
335#line 55
336 node = (struct node const *)__cil_tmp33;
337 {
338#line 56
339 while (1) {
340 while_6_continue: ;
341#line 56
342 if (! node) {
343 {
344#line 56
345 fail();
346 }
347 } else {
348
349 }
350 goto while_6_break;
351 }
352 while_6_break: ;
353 }
354 {
355#line 57
356 while (1) {
357 while_7_continue: ;
358 {
359#line 57
360 __cil_tmp34 = (unsigned int )node;
361#line 57
362 __cil_tmp35 = __cil_tmp34 + 12;
363#line 57
364 __cil_tmp36 = (struct list_head const *)__cil_tmp35;
365#line 57
366 __cil_tmp37 = (unsigned int )__cil_tmp36;
367#line 57
368 __cil_tmp38 = (unsigned int )node;
369#line 57
370 __cil_tmp39 = __cil_tmp38 + 12;
371#line 57
372 __cil_tmp40 = *((struct list_head * const *)__cil_tmp39);
373#line 57
374 __cil_tmp41 = (unsigned int )__cil_tmp40;
375#line 57
376 __cil_tmp42 = __cil_tmp41 == __cil_tmp37;
377#line 57
378 if (! __cil_tmp42) {
379 {
380#line 57
381 fail();
382 }
383 } else {
384
385 }
386 }
387 goto while_7_break;
388 }
389 while_7_break: ;
390 }
391 {
392#line 58
393 while (1) {
394 while_8_continue: ;
395 {
396#line 58
397 __cil_tmp43 = (unsigned int )node;
398#line 58
399 __cil_tmp44 = __cil_tmp43 + 12;
400#line 58
401 __cil_tmp45 = (struct list_head const *)__cil_tmp44;
402#line 58
403 __cil_tmp46 = (unsigned int )__cil_tmp45;
404#line 58
405 __cil_tmp47 = 12 + 4;
406#line 58
407 __cil_tmp48 = (unsigned int )node;
408#line 58
409 __cil_tmp49 = __cil_tmp48 + __cil_tmp47;
410#line 58
411 __cil_tmp50 = *((struct list_head * const *)__cil_tmp49);
412#line 58
413 __cil_tmp51 = (unsigned int )__cil_tmp50;
414#line 58
415 __cil_tmp52 = __cil_tmp51 == __cil_tmp46;
416#line 58
417 if (! __cil_tmp52) {
418 {
419#line 58
420 fail();
421 }
422 } else {
423
424 }
425 }
426 goto while_8_break;
427 }
428 while_8_break: ;
429 }
430 {
431#line 59
432 while (1) {
433 while_9_continue: ;
434 {
435#line 59
436 __cil_tmp53 = (unsigned int )node;
437#line 59
438 __cil_tmp54 = __cil_tmp53 + 4;
439#line 59
440 __cil_tmp55 = (struct list_head const *)__cil_tmp54;
441#line 59
442 __cil_tmp56 = (unsigned int )__cil_tmp55;
443#line 59
444 __cil_tmp57 = (unsigned int )node;
445#line 59
446 __cil_tmp58 = __cil_tmp57 + 12;
447#line 59
448 __cil_tmp59 = *((struct list_head * const *)__cil_tmp58);
449#line 59
450 __cil_tmp60 = (unsigned int )__cil_tmp59;
451#line 59
452 __cil_tmp61 = __cil_tmp60 != __cil_tmp56;
453#line 59
454 if (! __cil_tmp61) {
455 {
456#line 59
457 fail();
458 }
459 } else {
460
461 }
462 }
463 goto while_9_break;
464 }
465 while_9_break: ;
466 }
467 {
468#line 60
469 while (1) {
470 while_10_continue: ;
471 {
472#line 60
473 __cil_tmp62 = (unsigned int )node;
474#line 60
475 __cil_tmp63 = __cil_tmp62 + 4;
476#line 60
477 __cil_tmp64 = (struct list_head const *)__cil_tmp63;
478#line 60
479 __cil_tmp65 = (unsigned int )__cil_tmp64;
480#line 60
481 __cil_tmp66 = 12 + 4;
482#line 60
483 __cil_tmp67 = (unsigned int )node;
484#line 60
485 __cil_tmp68 = __cil_tmp67 + __cil_tmp66;
486#line 60
487 __cil_tmp69 = *((struct list_head * const *)__cil_tmp68);
488#line 60
489 __cil_tmp70 = (unsigned int )__cil_tmp69;
490#line 60
491 __cil_tmp71 = __cil_tmp70 != __cil_tmp65;
492#line 60
493 if (! __cil_tmp71) {
494 {
495#line 60
496 fail();
497 }
498 } else {
499
500 }
501 }
502 goto while_10_break;
503 }
504 while_10_break: ;
505 }
506 {
507#line 63
508 while (1) {
509 while_11_continue: ;
510 {
511#line 63
512 __cil_tmp72 = (struct node const *)head;
513#line 63
514 __cil_tmp73 = (unsigned int )__cil_tmp72;
515#line 63
516 __cil_tmp74 = (unsigned int )node;
517#line 63
518 __cil_tmp75 = __cil_tmp74 != __cil_tmp73;
519#line 63
520 if (! __cil_tmp75) {
521 {
522#line 63
523 fail();
524 }
525 } else {
526
527 }
528 }
529 goto while_11_break;
530 }
531 while_11_break: ;
532 }
533 {
534#line 64
535 while (1) {
536 while_12_continue: ;
537 {
538#line 64
539 __cil_tmp76 = (unsigned int )node;
540#line 64
541 __cil_tmp77 = __cil_tmp76 + 4;
542#line 64
543 __cil_tmp78 = (struct list_head const *)__cil_tmp77;
544#line 64
545 __cil_tmp79 = (struct node const *)__cil_tmp78;
546#line 64
547 __cil_tmp80 = (unsigned int )__cil_tmp79;
548#line 64
549 __cil_tmp81 = (unsigned int )node;
550#line 64
551 __cil_tmp82 = __cil_tmp81 != __cil_tmp80;
552#line 64
553 if (! __cil_tmp82) {
554 {
555#line 64
556 fail();
557 }
558 } else {
559
560 }
561 }
562 goto while_12_break;
563 }
564 while_12_break: ;
565 }
566 {
567#line 65
568 while (1) {
569 while_13_continue: ;
570 {
571#line 65
572 __cil_tmp83 = (int const *)node;
573#line 65
574 __cil_tmp84 = (struct node const *)__cil_tmp83;
575#line 65
576 __cil_tmp85 = (unsigned int )__cil_tmp84;
577#line 65
578 __cil_tmp86 = (unsigned int )node;
579#line 65
580 __cil_tmp87 = __cil_tmp86 == __cil_tmp85;
581#line 65
582 if (! __cil_tmp87) {
583 {
584#line 65
585 fail();
586 }
587 } else {
588
589 }
590 }
591 goto while_13_break;
592 }
593 while_13_break: ;
594 }
595 {
596#line 66
597 while (1) {
598 while_14_continue: ;
599 {
600#line 66
601 __cil_tmp88 = (unsigned int )node;
602#line 66
603 __cil_tmp89 = __cil_tmp88 + 4;
604#line 66
605 __cil_tmp90 = *((struct list_head * const *)__cil_tmp89);
606#line 66
607 __cil_tmp91 = (unsigned int )__cil_tmp90;
608#line 66
609 __cil_tmp92 = __cil_tmp91 + 4;
610#line 66
611 __cil_tmp93 = *((struct list_head **)__cil_tmp92);
612#line 66
613 __cil_tmp94 = (unsigned int )__cil_tmp93;
614#line 66
615 __cil_tmp95 = (unsigned int )head;
616#line 66
617 __cil_tmp96 = __cil_tmp95 == __cil_tmp94;
618#line 66
619 if (! __cil_tmp96) {
620 {
621#line 66
622 fail();
623 }
624 } else {
625
626 }
627 }
628 goto while_14_break;
629 }
630 while_14_break: ;
631 }
632 {
633#line 67
634 while (1) {
635 while_15_continue: ;
636 {
637#line 67
638 __cil_tmp97 = 4 + 4;
639#line 67
640 __cil_tmp98 = (unsigned int )node;
641#line 67
642 __cil_tmp99 = __cil_tmp98 + __cil_tmp97;
643#line 67
644 __cil_tmp100 = *((struct list_head * const *)__cil_tmp99);
645#line 67
646 __cil_tmp101 = *((struct list_head **)__cil_tmp100);
647#line 67
648 __cil_tmp102 = (unsigned int )__cil_tmp101;
649#line 67
650 __cil_tmp103 = (unsigned int )head;
651#line 67
652 __cil_tmp104 = __cil_tmp103 == __cil_tmp102;
653#line 67
654 if (! __cil_tmp104) {
655 {
656#line 67
657 fail();
658 }
659 } else {
660
661 }
662 }
663 goto while_15_break;
664 }
665 while_15_break: ;
666 }
667#line 70
668 __cil_tmp105 = *((struct list_head * const *)head);
669#line 70
670 head = (struct list_head const *)__cil_tmp105;
671 {
672#line 70
673 while (1) {
674 while_16_continue: ;
675 {
676#line 70
677 __cil_tmp106 = (unsigned int )head;
678#line 70
679 __cil_tmp107 = (unsigned int )node;
680#line 70
681 __cil_tmp108 = __cil_tmp107 + 4;
682#line 70
683 __cil_tmp109 = (struct list_head const *)__cil_tmp108;
684#line 70
685 __cil_tmp110 = (unsigned int )__cil_tmp109;
686#line 70
687 if (__cil_tmp110 != __cil_tmp106) {
688
689 } else {
690 goto while_16_break;
691 }
692 }
693#line 70
694 __cil_tmp111 = *((struct list_head * const *)head);
695#line 70
696 head = (struct list_head const *)__cil_tmp111;
697 }
698 while_16_break: ;
699 }
700 {
701#line 71
702 while (1) {
703 while_17_continue: ;
704 {
705#line 71
706 __cil_tmp112 = (unsigned int )node;
707#line 71
708 __cil_tmp113 = (struct node *)0;
709#line 71
710 __cil_tmp114 = (unsigned int )__cil_tmp113;
711#line 71
712 __cil_tmp115 = __cil_tmp114 + 4;
713#line 71
714 __cil_tmp116 = (struct list_head *)__cil_tmp115;
715#line 71
716 __cil_tmp117 = (unsigned long )__cil_tmp116;
717#line 71
718 __cil_tmp118 = (char *)head;
719#line 71
720 __cil_tmp119 = __cil_tmp118 - __cil_tmp117;
721#line 71
722 __cil_tmp120 = (struct node *)__cil_tmp119;
723#line 71
724 __cil_tmp121 = (unsigned int )__cil_tmp120;
725#line 71
726 __cil_tmp122 = __cil_tmp121 == __cil_tmp112;
727#line 71
728 if (! __cil_tmp122) {
729 {
730#line 71
731 fail();
732 }
733 } else {
734
735 }
736 }
737 goto while_17_break;
738 }
739 while_17_break: ;
740 }
741#line 72
742 return;
743}
744}
745#line 74 "test-0180.c"
746__inline static void __list_add(struct list_head *new , struct list_head *prev , struct list_head *next )
747{ unsigned int __cil_tmp4 ;
748 unsigned int __cil_tmp5 ;
749 unsigned int __cil_tmp6 ;
750 unsigned int __cil_tmp7 ;
751
752 {
753#line 78
754 __cil_tmp4 = (unsigned int )next;
755#line 78
756 __cil_tmp5 = __cil_tmp4 + 4;
757#line 78
758 *((struct list_head **)__cil_tmp5) = new;
759#line 79
760 *((struct list_head **)new) = next;
761#line 80
762 __cil_tmp6 = (unsigned int )new;
763#line 80
764 __cil_tmp7 = __cil_tmp6 + 4;
765#line 80
766 *((struct list_head **)__cil_tmp7) = prev;
767#line 81
768 *((struct list_head **)prev) = new;
769#line 82
770 return;
771}
772}
773#line 84 "test-0180.c"
774__inline static void __list_del(struct list_head *prev , struct list_head *next )
775{ unsigned int __cil_tmp3 ;
776 unsigned int __cil_tmp4 ;
777
778 {
779#line 86
780 __cil_tmp3 = (unsigned int )next;
781#line 86
782 __cil_tmp4 = __cil_tmp3 + 4;
783#line 86
784 *((struct list_head **)__cil_tmp4) = prev;
785#line 87
786 *((struct list_head **)prev) = next;
787#line 88
788 return;
789}
790}
791#line 90 "test-0180.c"
792__inline static void list_add(struct list_head *new , struct list_head *head )
793{ struct list_head *__cil_tmp3 ;
794
795 {
796 {
797#line 92
798 __cil_tmp3 = *((struct list_head **)head);
799#line 92
800 __list_add(new, head, __cil_tmp3);
801 }
802#line 93
803 return;
804}
805}
806#line 95 "test-0180.c"
807__inline static void list_move(struct list_head *list , struct list_head *head )
808{ unsigned int __cil_tmp3 ;
809 unsigned int __cil_tmp4 ;
810 struct list_head *__cil_tmp5 ;
811 struct list_head *__cil_tmp6 ;
812
813 {
814 {
815#line 97
816 __cil_tmp3 = (unsigned int )list;
817#line 97
818 __cil_tmp4 = __cil_tmp3 + 4;
819#line 97
820 __cil_tmp5 = *((struct list_head **)__cil_tmp4);
821#line 97
822 __cil_tmp6 = *((struct list_head **)list);
823#line 97
824 __list_del(__cil_tmp5, __cil_tmp6);
825#line 98
826 list_add(list, head);
827 }
828#line 99
829 return;
830}
831}
832#line 101 "test-0180.c"
833static void gl_insert(int value )
834{ struct node *node ;
835 void *tmp ;
836 unsigned int __cil_tmp4 ;
837 unsigned int __cil_tmp5 ;
838 unsigned int __cil_tmp6 ;
839 struct list_head *__cil_tmp7 ;
840 unsigned int __cil_tmp8 ;
841 unsigned int __cil_tmp9 ;
842 unsigned int __cil_tmp10 ;
843 unsigned int __cil_tmp11 ;
844 unsigned int __cil_tmp12 ;
845 unsigned int __cil_tmp13 ;
846 unsigned int __cil_tmp14 ;
847 unsigned int __cil_tmp15 ;
848
849 {
850 {
851#line 103
852 __cil_tmp4 = (unsigned int )20UL;
853#line 103
854 tmp = malloc(__cil_tmp4);
855#line 103
856 node = (struct node *)tmp;
857 }
858#line 104
859 if (! node) {
860 {
861#line 105
862 abort();
863 }
864 } else {
865
866 }
867 {
868#line 107
869 *((int *)node) = value;
870#line 108
871 __cil_tmp5 = (unsigned int )node;
872#line 108
873 __cil_tmp6 = __cil_tmp5 + 4;
874#line 108
875 __cil_tmp7 = (struct list_head *)__cil_tmp6;
876#line 108
877 list_add(__cil_tmp7, & gl_list);
878 }
879 {
880#line 109
881 while (1) {
882 while_18_continue: ;
883#line 109
884 __cil_tmp8 = (unsigned int )node;
885#line 109
886 __cil_tmp9 = __cil_tmp8 + 12;
887#line 109
888 __cil_tmp10 = (unsigned int )node;
889#line 109
890 __cil_tmp11 = __cil_tmp10 + 12;
891#line 109
892 *((struct list_head **)__cil_tmp9) = (struct list_head *)__cil_tmp11;
893#line 109
894 __cil_tmp12 = (unsigned int )node;
895#line 109
896 __cil_tmp13 = __cil_tmp12 + 12;
897#line 109
898 __cil_tmp14 = (unsigned int )node;
899#line 109
900 __cil_tmp15 = __cil_tmp14 + 12;
901#line 109
902 *((struct list_head **)__cil_tmp13) = (struct list_head *)__cil_tmp15;
903 goto while_18_break;
904 }
905 while_18_break: ;
906 }
907#line 110
908 return;
909}
910}
911#line 112 "test-0180.c"
912static void gl_read(void)
913{ int tmp ;
914 int tmp___0 ;
915
916 {
917 {
918#line 114
919 while (1) {
920 while_19_continue: ;
921 {
922#line 115
923 tmp = __VERIFIER_nondet_int();
924#line 115
925 gl_insert(tmp);
926#line 114
927 tmp___0 = __VERIFIER_nondet_int();
928 }
929#line 114
930 if (tmp___0) {
931
932 } else {
933 goto while_19_break;
934 }
935 }
936 while_19_break: ;
937 }
938#line 118
939 return;
940}
941}
942#line 120 "test-0180.c"
943static void gl_destroy(void)
944{ struct list_head *next ;
945 struct list_head *__cil_tmp2 ;
946 unsigned int __cil_tmp3 ;
947 unsigned int __cil_tmp4 ;
948 struct list_head *__cil_tmp5 ;
949 struct node *__cil_tmp6 ;
950 unsigned int __cil_tmp7 ;
951 unsigned int __cil_tmp8 ;
952 struct list_head *__cil_tmp9 ;
953 unsigned long __cil_tmp10 ;
954 char *__cil_tmp11 ;
955 char *__cil_tmp12 ;
956 struct node *__cil_tmp13 ;
957 void *__cil_tmp14 ;
958
959 {
960 {
961#line 123
962 while (1) {
963 while_20_continue: ;
964#line 123
965 __cil_tmp2 = & gl_list;
966#line 123
967 next = *((struct list_head **)__cil_tmp2);
968 {
969#line 123
970 __cil_tmp3 = (unsigned int )next;
971#line 123
972 __cil_tmp4 = (unsigned int )(& gl_list);
973#line 123
974 if (__cil_tmp4 != __cil_tmp3) {
975
976 } else {
977 goto while_20_break;
978 }
979 }
980 {
981#line 124
982 __cil_tmp5 = & gl_list;
983#line 124
984 *((struct list_head **)__cil_tmp5) = *((struct list_head **)next);
985#line 125
986 __cil_tmp6 = (struct node *)0;
987#line 125
988 __cil_tmp7 = (unsigned int )__cil_tmp6;
989#line 125
990 __cil_tmp8 = __cil_tmp7 + 4;
991#line 125
992 __cil_tmp9 = (struct list_head *)__cil_tmp8;
993#line 125
994 __cil_tmp10 = (unsigned long )__cil_tmp9;
995#line 125
996 __cil_tmp11 = (char *)next;
997#line 125
998 __cil_tmp12 = __cil_tmp11 - __cil_tmp10;
999#line 125
1000 __cil_tmp13 = (struct node *)__cil_tmp12;
1001#line 125
1002 __cil_tmp14 = (void *)__cil_tmp13;
1003#line 125
1004 free(__cil_tmp14);
1005 }
1006 }
1007 while_20_break: ;
1008 }
1009#line 127
1010 return;
1011}
1012}
1013#line 129 "test-0180.c"
1014static int val_from_node(struct list_head *head )
1015{ struct node *entry ;
1016 struct node *__cil_tmp3 ;
1017 unsigned int __cil_tmp4 ;
1018 unsigned int __cil_tmp5 ;
1019 struct list_head *__cil_tmp6 ;
1020 unsigned long __cil_tmp7 ;
1021 char *__cil_tmp8 ;
1022 char *__cil_tmp9 ;
1023
1024 {
1025#line 130
1026 __cil_tmp3 = (struct node *)0;
1027#line 130
1028 __cil_tmp4 = (unsigned int )__cil_tmp3;
1029#line 130
1030 __cil_tmp5 = __cil_tmp4 + 4;
1031#line 130
1032 __cil_tmp6 = (struct list_head *)__cil_tmp5;
1033#line 130
1034 __cil_tmp7 = (unsigned long )__cil_tmp6;
1035#line 130
1036 __cil_tmp8 = (char *)head;
1037#line 130
1038 __cil_tmp9 = __cil_tmp8 - __cil_tmp7;
1039#line 130
1040 entry = (struct node *)__cil_tmp9;
1041#line 131
1042 return (*((int *)entry));
1043}
1044}
1045#line 134 "test-0180.c"
1046static _Bool gl_sort_pass(void)
1047{ _Bool any_change ;
1048 struct list_head *pos0 ;
1049 struct list_head *pos1 ;
1050 int val0 ;
1051 int tmp ;
1052 int val1 ;
1053 int tmp___0 ;
1054 struct list_head *__cil_tmp8 ;
1055 unsigned int __cil_tmp9 ;
1056 unsigned int __cil_tmp10 ;
1057
1058 {
1059#line 136
1060 any_change = (_Bool)0;
1061#line 138
1062 __cil_tmp8 = & gl_list;
1063#line 138
1064 pos0 = *((struct list_head **)__cil_tmp8);
1065 {
1066#line 140
1067 while (1) {
1068 while_21_continue: ;
1069#line 140
1070 pos1 = *((struct list_head **)pos0);
1071 {
1072#line 140
1073 __cil_tmp9 = (unsigned int )pos1;
1074#line 140
1075 __cil_tmp10 = (unsigned int )(& gl_list);
1076#line 140
1077 if (__cil_tmp10 != __cil_tmp9) {
1078
1079 } else {
1080 goto while_21_break;
1081 }
1082 }
1083 {
1084#line 141
1085 tmp = val_from_node(pos0);
1086#line 141
1087 val0 = tmp;
1088#line 142
1089 tmp___0 = val_from_node(pos1);
1090#line 142
1091 val1 = tmp___0;
1092 }
1093#line 143
1094 if (val0 <= val1) {
1095#line 145
1096 pos0 = pos1;
1097 goto while_21_continue;
1098 } else {
1099
1100 }
1101 {
1102#line 149
1103 any_change = (_Bool)1;
1104#line 150
1105 list_move(pos0, pos1);
1106 }
1107 }
1108 while_21_break: ;
1109 }
1110#line 153
1111 return (any_change);
1112}
1113}
1114#line 156 "test-0180.c"
1115static void gl_sort(void)
1116{ _Bool tmp ;
1117
1118 {
1119 {
1120#line 158
1121 while (1) {
1122 while_22_continue: ;
1123 {
1124#line 158
1125 tmp = gl_sort_pass();
1126 }
1127#line 158
1128 if (tmp) {
1129
1130 } else {
1131 goto while_22_break;
1132 }
1133 }
1134 while_22_break: ;
1135 }
1136#line 160
1137 return;
1138}
1139}
1140#line 162 "test-0180.c"
1141int main(void)
1142{ struct list_head const *__cil_tmp1 ;
1143 struct list_head const *__cil_tmp2 ;
1144
1145 {
1146 {
1147#line 164
1148 gl_read();
1149#line 165
1150 __cil_tmp1 = (struct list_head const *)(& gl_list);
1151#line 165
1152 inspect(__cil_tmp1);
1153#line 167
1154 gl_sort();
1155#line 168
1156 __cil_tmp2 = (struct list_head const *)(& gl_list);
1157#line 168
1158 inspect(__cil_tmp2);
1159#line 170
1160 gl_destroy();
1161 }
1162#line 172
1163 return (0);
1164}
1165}