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