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 15 "dll_of_dll_BUG.c"
7struct slave_item {
8 struct slave_item *next ;
9 struct slave_item *prev ;
10};
11#line 31 "dll_of_dll_BUG.c"
12struct master_item {
13 struct master_item *next ;
14 struct master_item *prev ;
15 struct slave_item *slave ;
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 3 "dll_of_dll_BUG.c"
24extern int __VERIFIER_nondet_int(void) ;
25#line 5 "dll_of_dll_BUG.c"
26static void fail(void)
27{
28
29 {
30 ERROR:
31 goto ERROR;
32}
33}
34#line 20 "dll_of_dll_BUG.c"
35struct slave_item *alloc_or_die_slave(void)
36{ struct slave_item *ptr ;
37 void *tmp ;
38 unsigned int __cil_tmp3 ;
39 void *__cil_tmp4 ;
40 void *__cil_tmp5 ;
41
42 {
43 {
44#line 22
45 __cil_tmp3 = (unsigned int )8UL;
46#line 22
47 tmp = malloc(__cil_tmp3);
48#line 22
49 ptr = (struct slave_item *)tmp;
50 }
51#line 23
52 if (! ptr) {
53 {
54#line 24
55 abort();
56 }
57 } else {
58
59 }
60#line 26
61 __cil_tmp4 = (void *)0;
62#line 26
63 *((struct slave_item **)ptr) = (struct slave_item *)__cil_tmp4;
64#line 27
65 __cil_tmp5 = (void *)0;
66#line 27
67 *((struct slave_item **)ptr) = (struct slave_item *)__cil_tmp5;
68#line 28
69 return (ptr);
70}
71}
72#line 37 "dll_of_dll_BUG.c"
73struct master_item *alloc_or_die_master(void)
74{ struct master_item *ptr ;
75 void *tmp ;
76 unsigned int __cil_tmp3 ;
77 void *__cil_tmp4 ;
78 unsigned int __cil_tmp5 ;
79 unsigned int __cil_tmp6 ;
80 void *__cil_tmp7 ;
81 unsigned int __cil_tmp8 ;
82 unsigned int __cil_tmp9 ;
83 void *__cil_tmp10 ;
84
85 {
86 {
87#line 39
88 __cil_tmp3 = (unsigned int )12UL;
89#line 39
90 tmp = malloc(__cil_tmp3);
91#line 39
92 ptr = (struct master_item *)tmp;
93 }
94#line 40
95 if (! ptr) {
96 {
97#line 41
98 abort();
99 }
100 } else {
101
102 }
103#line 43
104 __cil_tmp4 = (void *)0;
105#line 43
106 *((struct master_item **)ptr) = (struct master_item *)__cil_tmp4;
107#line 44
108 __cil_tmp5 = (unsigned int )ptr;
109#line 44
110 __cil_tmp6 = __cil_tmp5 + 4;
111#line 44
112 __cil_tmp7 = (void *)0;
113#line 44
114 *((struct master_item **)__cil_tmp6) = (struct master_item *)__cil_tmp7;
115#line 45
116 __cil_tmp8 = (unsigned int )ptr;
117#line 45
118 __cil_tmp9 = __cil_tmp8 + 8;
119#line 45
120 __cil_tmp10 = (void *)0;
121#line 45
122 *((struct slave_item **)__cil_tmp9) = (struct slave_item *)__cil_tmp10;
123#line 46
124 return (ptr);
125}
126}
127#line 49 "dll_of_dll_BUG.c"
128void dll_insert_slave(struct slave_item **dll )
129{ struct slave_item *item ;
130 struct slave_item *tmp ;
131 struct slave_item *next ;
132 unsigned int __cil_tmp5 ;
133 unsigned int __cil_tmp6 ;
134
135 {
136 {
137#line 51
138 tmp = alloc_or_die_slave();
139#line 51
140 item = tmp;
141#line 52
142 next = *dll;
143#line 53
144 *((struct slave_item **)item) = next;
145 }
146#line 54
147 if (next) {
148#line 55
149 __cil_tmp5 = (unsigned int )next;
150#line 55
151 __cil_tmp6 = __cil_tmp5 + 4;
152#line 55
153 *((struct slave_item **)__cil_tmp6) = item;
154 } else {
155
156 }
157#line 57
158 *dll = item;
159#line 58
160 return;
161}
162}
163#line 60 "dll_of_dll_BUG.c"
164void *dll_create_generic(void (*insert_fnc)() )
165{ void *dll ;
166 int tmp ;
167 void **__cil_tmp4 ;
168 void **__cil_tmp5 ;
169
170 {
171 {
172#line 62
173 __cil_tmp4 = & dll;
174#line 62
175 *__cil_tmp4 = (void *)0;
176#line 63
177 (*insert_fnc)(& dll);
178#line 64
179 (*insert_fnc)(& dll);
180 }
181 {
182#line 66
183 while (1) {
184 while_0_continue: ;
185 {
186#line 66
187 tmp = __VERIFIER_nondet_int();
188 }
189#line 66
190 if (tmp) {
191
192 } else {
193 goto while_0_break;
194 }
195 {
196#line 67
197 (*insert_fnc)(& dll);
198 }
199 }
200 while_0_break: ;
201 }
202 {
203#line 69
204 __cil_tmp5 = & dll;
205#line 69
206 return (*__cil_tmp5);
207 }
208}
209}
210#line 72 "dll_of_dll_BUG.c"
211struct slave_item *dll_create_slave(void)
212{ void *tmp ;
213 void (*__cil_tmp2)() ;
214
215 {
216 {
217#line 74
218 __cil_tmp2 = (void (*)())(& dll_insert_slave);
219#line 74
220 tmp = dll_create_generic(__cil_tmp2);
221 }
222#line 74
223 return ((struct slave_item *)tmp);
224}
225}
226#line 77 "dll_of_dll_BUG.c"
227void dll_destroy_slave(struct slave_item *dll )
228{ struct slave_item *next ;
229 void *__cil_tmp3 ;
230
231 {
232 {
233#line 79
234 while (1) {
235 while_1_continue: ;
236#line 79
237 if (dll) {
238
239 } else {
240 goto while_1_break;
241 }
242 {
243#line 80
244 next = *((struct slave_item **)dll);
245#line 81
246 __cil_tmp3 = (void *)dll;
247#line 81
248 free(__cil_tmp3);
249#line 82
250 dll = next;
251 }
252 }
253 while_1_break: ;
254 }
255#line 84
256 return;
257}
258}
259#line 86 "dll_of_dll_BUG.c"
260void dll_destroy_nested_lists(struct master_item *dll )
261{ unsigned int __cil_tmp2 ;
262 unsigned int __cil_tmp3 ;
263 struct slave_item *__cil_tmp4 ;
264
265 {
266 {
267#line 88
268 while (1) {
269 while_2_continue: ;
270#line 88
271 if (dll) {
272
273 } else {
274 goto while_2_break;
275 }
276 {
277#line 89
278 __cil_tmp2 = (unsigned int )dll;
279#line 89
280 __cil_tmp3 = __cil_tmp2 + 8;
281#line 89
282 __cil_tmp4 = *((struct slave_item **)__cil_tmp3);
283#line 89
284 dll_destroy_slave(__cil_tmp4);
285#line 90
286 dll = *((struct master_item **)dll);
287 }
288 }
289 while_2_break: ;
290 }
291#line 92
292 return;
293}
294}
295#line 94 "dll_of_dll_BUG.c"
296void dll_reinit_nested_lists(struct master_item *dll )
297{ unsigned int __cil_tmp2 ;
298 unsigned int __cil_tmp3 ;
299 void *__cil_tmp4 ;
300
301 {
302 {
303#line 96
304 while (1) {
305 while_3_continue: ;
306#line 96
307 if (dll) {
308
309 } else {
310 goto while_3_break;
311 }
312#line 97
313 __cil_tmp2 = (unsigned int )dll;
314#line 97
315 __cil_tmp3 = __cil_tmp2 + 8;
316#line 97
317 __cil_tmp4 = (void *)0;
318#line 97
319 *((struct slave_item **)__cil_tmp3) = (struct slave_item *)__cil_tmp4;
320#line 98
321 dll = *((struct master_item **)dll);
322 }
323 while_3_break: ;
324 }
325#line 100
326 return;
327}
328}
329#line 102 "dll_of_dll_BUG.c"
330void dll_destroy_master(struct master_item *dll )
331{ struct master_item *next ;
332 void *__cil_tmp3 ;
333
334 {
335 {
336#line 104
337 while (1) {
338 while_4_continue: ;
339#line 104
340 if (dll) {
341
342 } else {
343 goto while_4_break;
344 }
345 {
346#line 105
347 next = *((struct master_item **)dll);
348#line 106
349 __cil_tmp3 = (void *)dll;
350#line 106
351 free(__cil_tmp3);
352#line 107
353 dll = next;
354 }
355 }
356 while_4_break: ;
357 }
358#line 109
359 return;
360}
361}
362#line 111 "dll_of_dll_BUG.c"
363void dll_insert_master(struct master_item **dll )
364{ struct master_item *item ;
365 struct master_item *tmp ;
366 struct master_item *next ;
367 unsigned int __cil_tmp5 ;
368 unsigned int __cil_tmp6 ;
369 unsigned int __cil_tmp7 ;
370 unsigned int __cil_tmp8 ;
371
372 {
373 {
374#line 113
375 tmp = alloc_or_die_master();
376#line 113
377 item = tmp;
378#line 114
379 next = *dll;
380#line 115
381 *((struct master_item **)item) = next;
382 }
383#line 116
384 if (next) {
385#line 117
386 __cil_tmp5 = (unsigned int )next;
387#line 117
388 __cil_tmp6 = __cil_tmp5 + 4;
389#line 117
390 *((struct master_item **)__cil_tmp6) = item;
391 } else {
392
393 }
394 {
395#line 119
396 __cil_tmp7 = (unsigned int )item;
397#line 119
398 __cil_tmp8 = __cil_tmp7 + 8;
399#line 119
400 *((struct slave_item **)__cil_tmp8) = dll_create_slave();
401#line 120
402 *dll = item;
403 }
404#line 121
405 return;
406}
407}
408#line 123 "dll_of_dll_BUG.c"
409struct master_item *dll_create_master(void)
410{ void *tmp ;
411 void (*__cil_tmp2)() ;
412
413 {
414 {
415#line 125
416 __cil_tmp2 = (void (*)())(& dll_insert_master);
417#line 125
418 tmp = dll_create_generic(__cil_tmp2);
419 }
420#line 125
421 return ((struct master_item *)tmp);
422}
423}
424#line 128 "dll_of_dll_BUG.c"
425void inspect_base(struct master_item *dll )
426{ struct master_item *__cil_tmp2 ;
427 unsigned int __cil_tmp3 ;
428 unsigned int __cil_tmp4 ;
429 struct master_item *__cil_tmp5 ;
430 int __cil_tmp6 ;
431 unsigned int __cil_tmp7 ;
432 unsigned int __cil_tmp8 ;
433 struct master_item *__cil_tmp9 ;
434 unsigned int __cil_tmp10 ;
435 unsigned int __cil_tmp11 ;
436 struct master_item *__cil_tmp12 ;
437 struct master_item *__cil_tmp13 ;
438 unsigned int __cil_tmp14 ;
439 unsigned int __cil_tmp15 ;
440 unsigned int __cil_tmp16 ;
441 struct master_item *__cil_tmp17 ;
442 struct master_item *__cil_tmp18 ;
443 unsigned int __cil_tmp19 ;
444 int __cil_tmp20 ;
445
446 {
447 {
448#line 130
449 while (1) {
450 while_5_continue: ;
451#line 130
452 if (! dll) {
453 {
454#line 130
455 fail();
456 }
457 } else {
458
459 }
460 goto while_5_break;
461 }
462 while_5_break: ;
463 }
464 {
465#line 131
466 while (1) {
467 while_6_continue: ;
468 {
469#line 131
470 __cil_tmp2 = *((struct master_item **)dll);
471#line 131
472 if (! __cil_tmp2) {
473 {
474#line 131
475 fail();
476 }
477 } else {
478
479 }
480 }
481 goto while_6_break;
482 }
483 while_6_break: ;
484 }
485 {
486#line 132
487 while (1) {
488 while_7_continue: ;
489 {
490#line 132
491 __cil_tmp3 = (unsigned int )dll;
492#line 132
493 __cil_tmp4 = __cil_tmp3 + 4;
494#line 132
495 __cil_tmp5 = *((struct master_item **)__cil_tmp4);
496#line 132
497 __cil_tmp6 = ! __cil_tmp5;
498#line 132
499 if (! __cil_tmp6) {
500 {
501#line 132
502 fail();
503 }
504 } else {
505
506 }
507 }
508 goto while_7_break;
509 }
510 while_7_break: ;
511 }
512#line 134
513 dll = *((struct master_item **)dll);
514 {
515#line 134
516 while (1) {
517 while_8_continue: ;
518#line 134
519 if (dll) {
520
521 } else {
522 goto while_8_break;
523 }
524 {
525#line 135
526 while (1) {
527 while_9_continue: ;
528 {
529#line 135
530 __cil_tmp7 = (unsigned int )dll;
531#line 135
532 __cil_tmp8 = __cil_tmp7 + 4;
533#line 135
534 __cil_tmp9 = *((struct master_item **)__cil_tmp8);
535#line 135
536 if (! __cil_tmp9) {
537 {
538#line 135
539 fail();
540 }
541 } else {
542
543 }
544 }
545 goto while_9_break;
546 }
547 while_9_break: ;
548 }
549 {
550#line 136
551 while (1) {
552 while_10_continue: ;
553 {
554#line 136
555 __cil_tmp10 = (unsigned int )dll;
556#line 136
557 __cil_tmp11 = __cil_tmp10 + 4;
558#line 136
559 __cil_tmp12 = *((struct master_item **)__cil_tmp11);
560#line 136
561 __cil_tmp13 = *((struct master_item **)__cil_tmp12);
562#line 136
563 if (! __cil_tmp13) {
564 {
565#line 136
566 fail();
567 }
568 } else {
569
570 }
571 }
572 goto while_10_break;
573 }
574 while_10_break: ;
575 }
576 {
577#line 137
578 while (1) {
579 while_11_continue: ;
580 {
581#line 137
582 __cil_tmp14 = (unsigned int )dll;
583#line 137
584 __cil_tmp15 = (unsigned int )dll;
585#line 137
586 __cil_tmp16 = __cil_tmp15 + 4;
587#line 137
588 __cil_tmp17 = *((struct master_item **)__cil_tmp16);
589#line 137
590 __cil_tmp18 = *((struct master_item **)__cil_tmp17);
591#line 137
592 __cil_tmp19 = (unsigned int )__cil_tmp18;
593#line 137
594 __cil_tmp20 = __cil_tmp19 == __cil_tmp14;
595#line 137
596 if (! __cil_tmp20) {
597 {
598#line 137
599 fail();
600 }
601 } else {
602
603 }
604 }
605 goto while_11_break;
606 }
607 while_11_break: ;
608 }
609#line 134
610 dll = *((struct master_item **)dll);
611 }
612 while_8_break: ;
613 }
614#line 139
615 return;
616}
617}
618#line 141 "dll_of_dll_BUG.c"
619void inspect_full(struct master_item *dll )
620{ struct slave_item *pos ;
621 unsigned int __cil_tmp3 ;
622 unsigned int __cil_tmp4 ;
623 struct slave_item *__cil_tmp5 ;
624 unsigned int __cil_tmp6 ;
625 unsigned int __cil_tmp7 ;
626 struct slave_item *__cil_tmp8 ;
627 int __cil_tmp9 ;
628 unsigned int __cil_tmp10 ;
629 unsigned int __cil_tmp11 ;
630 struct slave_item *__cil_tmp12 ;
631 unsigned int __cil_tmp13 ;
632 unsigned int __cil_tmp14 ;
633 struct slave_item *__cil_tmp15 ;
634 struct slave_item *__cil_tmp16 ;
635 unsigned int __cil_tmp17 ;
636 unsigned int __cil_tmp18 ;
637 unsigned int __cil_tmp19 ;
638 struct slave_item *__cil_tmp20 ;
639 struct slave_item *__cil_tmp21 ;
640 unsigned int __cil_tmp22 ;
641 int __cil_tmp23 ;
642
643 {
644 {
645#line 143
646 inspect_base(dll);
647 }
648 {
649#line 145
650 while (1) {
651 while_12_continue: ;
652#line 145
653 if (dll) {
654
655 } else {
656 goto while_12_break;
657 }
658#line 146
659 __cil_tmp3 = (unsigned int )dll;
660#line 146
661 __cil_tmp4 = __cil_tmp3 + 8;
662#line 146
663 pos = *((struct slave_item **)__cil_tmp4);
664 {
665#line 147
666 while (1) {
667 while_13_continue: ;
668#line 147
669 if (! pos) {
670 {
671#line 147
672 fail();
673 }
674 } else {
675
676 }
677 goto while_13_break;
678 }
679 while_13_break: ;
680 }
681 {
682#line 148
683 while (1) {
684 while_14_continue: ;
685 {
686#line 148
687 __cil_tmp5 = *((struct slave_item **)pos);
688#line 148
689 if (! __cil_tmp5) {
690 {
691#line 148
692 fail();
693 }
694 } else {
695
696 }
697 }
698 goto while_14_break;
699 }
700 while_14_break: ;
701 }
702 {
703#line 149
704 while (1) {
705 while_15_continue: ;
706 {
707#line 149
708 __cil_tmp6 = (unsigned int )pos;
709#line 149
710 __cil_tmp7 = __cil_tmp6 + 4;
711#line 149
712 __cil_tmp8 = *((struct slave_item **)__cil_tmp7);
713#line 149
714 __cil_tmp9 = ! __cil_tmp8;
715#line 149
716 if (! __cil_tmp9) {
717 {
718#line 149
719 fail();
720 }
721 } else {
722
723 }
724 }
725 goto while_15_break;
726 }
727 while_15_break: ;
728 }
729#line 151
730 pos = *((struct slave_item **)pos);
731 {
732#line 151
733 while (1) {
734 while_16_continue: ;
735#line 151
736 if (pos) {
737
738 } else {
739 goto while_16_break;
740 }
741 {
742#line 152
743 while (1) {
744 while_17_continue: ;
745 {
746#line 152
747 __cil_tmp10 = (unsigned int )pos;
748#line 152
749 __cil_tmp11 = __cil_tmp10 + 4;
750#line 152
751 __cil_tmp12 = *((struct slave_item **)__cil_tmp11);
752#line 152
753 if (! __cil_tmp12) {
754 {
755#line 152
756 fail();
757 }
758 } else {
759
760 }
761 }
762 goto while_17_break;
763 }
764 while_17_break: ;
765 }
766 {
767#line 153
768 while (1) {
769 while_18_continue: ;
770 {
771#line 153
772 __cil_tmp13 = (unsigned int )pos;
773#line 153
774 __cil_tmp14 = __cil_tmp13 + 4;
775#line 153
776 __cil_tmp15 = *((struct slave_item **)__cil_tmp14);
777#line 153
778 __cil_tmp16 = *((struct slave_item **)__cil_tmp15);
779#line 153
780 if (! __cil_tmp16) {
781 {
782#line 153
783 fail();
784 }
785 } else {
786
787 }
788 }
789 goto while_18_break;
790 }
791 while_18_break: ;
792 }
793 {
794#line 154
795 while (1) {
796 while_19_continue: ;
797 {
798#line 154
799 __cil_tmp17 = (unsigned int )pos;
800#line 154
801 __cil_tmp18 = (unsigned int )pos;
802#line 154
803 __cil_tmp19 = __cil_tmp18 + 4;
804#line 154
805 __cil_tmp20 = *((struct slave_item **)__cil_tmp19);
806#line 154
807 __cil_tmp21 = *((struct slave_item **)__cil_tmp20);
808#line 154
809 __cil_tmp22 = (unsigned int )__cil_tmp21;
810#line 154
811 __cil_tmp23 = __cil_tmp22 == __cil_tmp17;
812#line 154
813 if (! __cil_tmp23) {
814 {
815#line 154
816 fail();
817 }
818 } else {
819
820 }
821 }
822 goto while_19_break;
823 }
824 while_19_break: ;
825 }
826#line 151
827 pos = *((struct slave_item **)pos);
828 }
829 while_16_break: ;
830 }
831#line 145
832 dll = *((struct master_item **)dll);
833 }
834 while_12_break: ;
835 }
836#line 157
837 return;
838}
839}
840#line 159 "dll_of_dll_BUG.c"
841void inspect_dangling(struct master_item *dll )
842{ unsigned int __cil_tmp2 ;
843 unsigned int __cil_tmp3 ;
844 struct slave_item *__cil_tmp4 ;
845
846 {
847 {
848#line 161
849 inspect_base(dll);
850 }
851 {
852#line 163
853 while (1) {
854 while_20_continue: ;
855#line 163
856 if (dll) {
857
858 } else {
859 goto while_20_break;
860 }
861 {
862#line 164
863 while (1) {
864 while_21_continue: ;
865 {
866#line 164
867 __cil_tmp2 = (unsigned int )dll;
868#line 164
869 __cil_tmp3 = __cil_tmp2 + 8;
870#line 164
871 __cil_tmp4 = *((struct slave_item **)__cil_tmp3);
872#line 164
873 if (! __cil_tmp4) {
874 {
875#line 164
876 fail();
877 }
878 } else {
879
880 }
881 }
882 goto while_21_break;
883 }
884 while_21_break: ;
885 }
886#line 163
887 dll = *((struct master_item **)dll);
888 }
889 while_20_break: ;
890 }
891#line 165
892 return;
893}
894}
895#line 167 "dll_of_dll_BUG.c"
896void inspect_init(struct master_item *dll )
897{ unsigned int __cil_tmp2 ;
898 unsigned int __cil_tmp3 ;
899 struct slave_item *__cil_tmp4 ;
900 int __cil_tmp5 ;
901
902 {
903 {
904#line 169
905 inspect_base(dll);
906 }
907 {
908#line 171
909 while (1) {
910 while_22_continue: ;
911#line 171
912 if (dll) {
913
914 } else {
915 goto while_22_break;
916 }
917 {
918#line 172
919 while (1) {
920 while_23_continue: ;
921 {
922#line 172
923 __cil_tmp2 = (unsigned int )dll;
924#line 172
925 __cil_tmp3 = __cil_tmp2 + 8;
926#line 172
927 __cil_tmp4 = *((struct slave_item **)__cil_tmp3);
928#line 172
929 __cil_tmp5 = ! __cil_tmp4;
930#line 172
931 if (! __cil_tmp5) {
932 {
933#line 172
934 fail();
935 }
936 } else {
937
938 }
939 }
940 goto while_23_break;
941 }
942 while_23_break: ;
943 }
944#line 171
945 dll = *((struct master_item **)dll);
946 }
947 while_22_break: ;
948 }
949#line 173
950 return;
951}
952}
953#line 175 "dll_of_dll_BUG.c"
954int main(void)
955{ struct master_item *dll ;
956 struct master_item *tmp ;
957
958 {
959 {
960#line 177
961 tmp = dll_create_master();
962#line 177
963 dll = tmp;
964#line 178
965 inspect_full(dll);
966#line 180
967 dll_destroy_nested_lists(dll);
968#line 181
969 inspect_dangling(dll);
970#line 183
971 dll_reinit_nested_lists(dll);
972#line 184
973 inspect_init(dll);
974#line 187
975 dll_destroy_master(dll);
976 }
977#line 188
978 return (0);
979}
980}