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 19 "sll_to_dll_rev_BUG.c"
7struct node {
8 struct node *next ;
9 struct node *prev ;
10};
11#line 471 "/usr/include/stdlib.h"
12extern __attribute__((__nothrow__)) void *malloc(size_t __size ) __attribute__((__malloc__)) ;
13#line 488
14extern __attribute__((__nothrow__)) void free(void *__ptr ) ;
15#line 514
16extern __attribute__((__nothrow__, __noreturn__)) void abort(void) ;
17#line 3 "sll_to_dll_rev_BUG.c"
18extern int __VERIFIER_nondet_int(void) ;
19#line 5 "sll_to_dll_rev_BUG.c"
20static void fail(void)
21{
22
23 {
24 ERROR:
25 goto ERROR;
26}
27}
28#line 24 "sll_to_dll_rev_BUG.c"
29static struct node *alloc_node(void)
30{ struct node *ptr ;
31 void *tmp ;
32 unsigned int __cil_tmp3 ;
33 void *__cil_tmp4 ;
34 unsigned int __cil_tmp5 ;
35 unsigned int __cil_tmp6 ;
36 void *__cil_tmp7 ;
37
38 {
39 {
40#line 26
41 __cil_tmp3 = (unsigned int )8UL;
42#line 26
43 tmp = malloc(__cil_tmp3);
44#line 26
45 ptr = (struct node *)tmp;
46 }
47#line 27
48 if (! ptr) {
49 {
50#line 28
51 abort();
52 }
53 } else {
54
55 }
56#line 30
57 __cil_tmp4 = (void *)0;
58#line 30
59 *((struct node **)ptr) = (struct node *)__cil_tmp4;
60#line 31
61 __cil_tmp5 = (unsigned int )ptr;
62#line 31
63 __cil_tmp6 = __cil_tmp5 + 4;
64#line 31
65 __cil_tmp7 = (void *)0;
66#line 31
67 *((struct node **)__cil_tmp6) = (struct node *)__cil_tmp7;
68#line 32
69 return (ptr);
70}
71}
72#line 35 "sll_to_dll_rev_BUG.c"
73static void chain_node(struct node **ppnode )
74{ struct node *node ;
75 struct node *tmp ;
76
77 {
78 {
79#line 37
80 tmp = alloc_node();
81#line 37
82 node = tmp;
83#line 38
84 *((struct node **)node) = *ppnode;
85#line 39
86 *ppnode = node;
87 }
88#line 40
89 return;
90}
91}
92#line 42 "sll_to_dll_rev_BUG.c"
93static struct node *create_sll(struct node const **pp1 , struct node const **pp2 )
94{ struct node *list ;
95 int tmp ;
96 int tmp___0 ;
97 int tmp___1 ;
98 struct node **__cil_tmp7 ;
99 void *__cil_tmp8 ;
100 struct node **__cil_tmp9 ;
101 struct node *__cil_tmp10 ;
102 struct node **__cil_tmp11 ;
103 struct node *__cil_tmp12 ;
104 struct node **__cil_tmp13 ;
105
106 {
107#line 44
108 __cil_tmp7 = & list;
109#line 44
110 __cil_tmp8 = (void *)0;
111#line 44
112 *__cil_tmp7 = (struct node *)__cil_tmp8;
113 {
114#line 46
115 while (1) {
116 while_0_continue: ;
117 {
118#line 47
119 chain_node(& list);
120#line 46
121 tmp = __VERIFIER_nondet_int();
122 }
123#line 46
124 if (tmp) {
125
126 } else {
127 goto while_0_break;
128 }
129 }
130 while_0_break: ;
131 }
132#line 50
133 __cil_tmp9 = & list;
134#line 50
135 __cil_tmp10 = *__cil_tmp9;
136#line 50
137 *pp2 = (struct node const *)__cil_tmp10;
138 {
139#line 52
140 while (1) {
141 while_1_continue: ;
142 {
143#line 52
144 tmp___0 = __VERIFIER_nondet_int();
145 }
146#line 52
147 if (tmp___0) {
148
149 } else {
150 goto while_1_break;
151 }
152 {
153#line 53
154 chain_node(& list);
155 }
156 }
157 while_1_break: ;
158 }
159#line 55
160 __cil_tmp11 = & list;
161#line 55
162 __cil_tmp12 = *__cil_tmp11;
163#line 55
164 *pp1 = (struct node const *)__cil_tmp12;
165 {
166#line 57
167 while (1) {
168 while_2_continue: ;
169 {
170#line 58
171 chain_node(& list);
172#line 57
173 tmp___1 = __VERIFIER_nondet_int();
174 }
175#line 57
176 if (tmp___1) {
177
178 } else {
179 goto while_2_break;
180 }
181 }
182 while_2_break: ;
183 }
184 {
185#line 61
186 __cil_tmp13 = & list;
187#line 61
188 return (*__cil_tmp13);
189 }
190}
191}
192#line 64 "sll_to_dll_rev_BUG.c"
193void init_back_link(struct node *list )
194{ struct node *next ;
195 unsigned int __cil_tmp3 ;
196 unsigned int __cil_tmp4 ;
197
198 {
199 {
200#line 65
201 while (1) {
202 while_3_continue: ;
203#line 66
204 next = *((struct node **)list);
205#line 67
206 if (! next) {
207#line 68
208 return;
209 } else {
210
211 }
212#line 70
213 __cil_tmp3 = (unsigned int )next;
214#line 70
215 __cil_tmp4 = __cil_tmp3 + 4;
216#line 70
217 *((struct node **)__cil_tmp4) = list;
218#line 71
219 list = next;
220 }
221 while_3_break: ;
222 }
223}
224}
225#line 75 "sll_to_dll_rev_BUG.c"
226void reverse_dll(struct node *list )
227{ struct node *next ;
228 unsigned int __cil_tmp3 ;
229 unsigned int __cil_tmp4 ;
230 unsigned int __cil_tmp5 ;
231 unsigned int __cil_tmp6 ;
232
233 {
234 {
235#line 76
236 while (1) {
237 while_4_continue: ;
238#line 76
239 if (list) {
240
241 } else {
242 goto while_4_break;
243 }
244#line 77
245 next = *((struct node **)list);
246#line 78
247 __cil_tmp3 = (unsigned int )list;
248#line 78
249 __cil_tmp4 = __cil_tmp3 + 4;
250#line 78
251 *((struct node **)list) = *((struct node **)__cil_tmp4);
252#line 79
253 __cil_tmp5 = (unsigned int )list;
254#line 79
255 __cil_tmp6 = __cil_tmp5 + 4;
256#line 79
257 *((struct node **)__cil_tmp6) = next;
258#line 80
259 list = next;
260 }
261 while_4_break: ;
262 }
263#line 82
264 return;
265}
266}
267#line 84 "sll_to_dll_rev_BUG.c"
268void remove_fw_link(struct node *list )
269{ struct node *next ;
270 void *__cil_tmp3 ;
271
272 {
273 {
274#line 85
275 while (1) {
276 while_5_continue: ;
277#line 85
278 if (list) {
279
280 } else {
281 goto while_5_break;
282 }
283#line 86
284 next = *((struct node **)list);
285#line 87
286 __cil_tmp3 = (void *)0;
287#line 87
288 *((struct node **)list) = (struct node *)__cil_tmp3;
289#line 88
290 list = next;
291 }
292 while_5_break: ;
293 }
294#line 90
295 return;
296}
297}
298#line 92 "sll_to_dll_rev_BUG.c"
299void check_seq_next(struct node const *beg , struct node const *end )
300{ struct node *__cil_tmp3 ;
301 unsigned int __cil_tmp4 ;
302 unsigned int __cil_tmp5 ;
303 struct node *__cil_tmp6 ;
304
305 {
306 {
307#line 93
308 while (1) {
309 while_6_continue: ;
310#line 93
311 if (! beg) {
312 {
313#line 93
314 fail();
315 }
316 } else {
317
318 }
319 goto while_6_break;
320 }
321 while_6_break: ;
322 }
323 {
324#line 94
325 while (1) {
326 while_7_continue: ;
327#line 94
328 if (! end) {
329 {
330#line 94
331 fail();
332 }
333 } else {
334
335 }
336 goto while_7_break;
337 }
338 while_7_break: ;
339 }
340#line 96
341 __cil_tmp3 = *((struct node * const *)beg);
342#line 96
343 beg = (struct node const *)__cil_tmp3;
344 {
345#line 96
346 while (1) {
347 while_8_continue: ;
348 {
349#line 96
350 __cil_tmp4 = (unsigned int )beg;
351#line 96
352 __cil_tmp5 = (unsigned int )end;
353#line 96
354 if (__cil_tmp5 != __cil_tmp4) {
355
356 } else {
357 goto while_8_break;
358 }
359 }
360 {
361#line 97
362 while (1) {
363 while_9_continue: ;
364#line 97
365 if (! beg) {
366 {
367#line 97
368 fail();
369 }
370 } else {
371
372 }
373 goto while_9_break;
374 }
375 while_9_break: ;
376 }
377#line 96
378 __cil_tmp6 = *((struct node * const *)beg);
379#line 96
380 beg = (struct node const *)__cil_tmp6;
381 }
382 while_8_break: ;
383 }
384#line 98
385 return;
386}
387}
388#line 100 "sll_to_dll_rev_BUG.c"
389void check_seq_prev(struct node const *beg , struct node const *end )
390{ unsigned int __cil_tmp3 ;
391 unsigned int __cil_tmp4 ;
392 struct node *__cil_tmp5 ;
393 unsigned int __cil_tmp6 ;
394 unsigned int __cil_tmp7 ;
395 unsigned int __cil_tmp8 ;
396 unsigned int __cil_tmp9 ;
397 struct node *__cil_tmp10 ;
398
399 {
400 {
401#line 101
402 while (1) {
403 while_10_continue: ;
404#line 101
405 if (! beg) {
406 {
407#line 101
408 fail();
409 }
410 } else {
411
412 }
413 goto while_10_break;
414 }
415 while_10_break: ;
416 }
417 {
418#line 102
419 while (1) {
420 while_11_continue: ;
421#line 102
422 if (! end) {
423 {
424#line 102
425 fail();
426 }
427 } else {
428
429 }
430 goto while_11_break;
431 }
432 while_11_break: ;
433 }
434#line 104
435 __cil_tmp3 = (unsigned int )beg;
436#line 104
437 __cil_tmp4 = __cil_tmp3 + 4;
438#line 104
439 __cil_tmp5 = *((struct node * const *)__cil_tmp4);
440#line 104
441 beg = (struct node const *)__cil_tmp5;
442 {
443#line 104
444 while (1) {
445 while_12_continue: ;
446 {
447#line 104
448 __cil_tmp6 = (unsigned int )beg;
449#line 104
450 __cil_tmp7 = (unsigned int )end;
451#line 104
452 if (__cil_tmp7 != __cil_tmp6) {
453
454 } else {
455 goto while_12_break;
456 }
457 }
458 {
459#line 105
460 while (1) {
461 while_13_continue: ;
462#line 105
463 if (! beg) {
464 {
465#line 105
466 fail();
467 }
468 } else {
469
470 }
471 goto while_13_break;
472 }
473 while_13_break: ;
474 }
475#line 104
476 __cil_tmp8 = (unsigned int )beg;
477#line 104
478 __cil_tmp9 = __cil_tmp8 + 4;
479#line 104
480 __cil_tmp10 = *((struct node * const *)__cil_tmp9);
481#line 104
482 beg = (struct node const *)__cil_tmp10;
483 }
484 while_12_break: ;
485 }
486#line 106
487 return;
488}
489}
490#line 108 "sll_to_dll_rev_BUG.c"
491int main(void)
492{ struct node const *p1 ;
493 struct node const *p2 ;
494 struct node *list ;
495 struct node *tmp ;
496 struct node *prev ;
497 struct node const **__cil_tmp6 ;
498 struct node const *__cil_tmp7 ;
499 struct node const **__cil_tmp8 ;
500 struct node const *__cil_tmp9 ;
501 struct node const **__cil_tmp10 ;
502 struct node const *__cil_tmp11 ;
503 unsigned int __cil_tmp12 ;
504 unsigned int __cil_tmp13 ;
505 struct node *__cil_tmp14 ;
506 int __cil_tmp15 ;
507 struct node const **__cil_tmp16 ;
508 struct node const *__cil_tmp17 ;
509 unsigned int __cil_tmp18 ;
510 unsigned int __cil_tmp19 ;
511 struct node *__cil_tmp20 ;
512 int __cil_tmp21 ;
513 struct node const **__cil_tmp22 ;
514 struct node const *__cil_tmp23 ;
515 struct node const **__cil_tmp24 ;
516 struct node const *__cil_tmp25 ;
517 struct node const **__cil_tmp26 ;
518 struct node const *__cil_tmp27 ;
519 struct node const **__cil_tmp28 ;
520 struct node const *__cil_tmp29 ;
521 struct node const **__cil_tmp30 ;
522 struct node const *__cil_tmp31 ;
523 struct node const **__cil_tmp32 ;
524 struct node const *__cil_tmp33 ;
525 struct node const **__cil_tmp34 ;
526 struct node const *__cil_tmp35 ;
527 struct node const **__cil_tmp36 ;
528 struct node const *__cil_tmp37 ;
529 struct node const **__cil_tmp38 ;
530 struct node const *__cil_tmp39 ;
531 struct node const **__cil_tmp40 ;
532 struct node const *__cil_tmp41 ;
533 unsigned int __cil_tmp42 ;
534 unsigned int __cil_tmp43 ;
535 void *__cil_tmp44 ;
536
537 {
538 {
539#line 112
540 tmp = create_sll(& p1, & p2);
541#line 112
542 list = tmp;
543 }
544 {
545#line 113
546 while (1) {
547 while_14_continue: ;
548 goto while_14_break;
549 }
550 while_14_break: ;
551 }
552 {
553#line 114
554 __cil_tmp6 = & p1;
555#line 114
556 __cil_tmp7 = *__cil_tmp6;
557#line 114
558 __cil_tmp8 = & p2;
559#line 114
560 __cil_tmp9 = *__cil_tmp8;
561#line 114
562 check_seq_next(__cil_tmp7, __cil_tmp9);
563 }
564 {
565#line 115
566 while (1) {
567 while_15_continue: ;
568 {
569#line 115
570 __cil_tmp10 = & p1;
571#line 115
572 __cil_tmp11 = *__cil_tmp10;
573#line 115
574 __cil_tmp12 = (unsigned int )__cil_tmp11;
575#line 115
576 __cil_tmp13 = __cil_tmp12 + 4;
577#line 115
578 __cil_tmp14 = *((struct node * const *)__cil_tmp13);
579#line 115
580 __cil_tmp15 = ! __cil_tmp14;
581#line 115
582 if (! __cil_tmp15) {
583 {
584#line 115
585 fail();
586 }
587 } else {
588
589 }
590 }
591 goto while_15_break;
592 }
593 while_15_break: ;
594 }
595 {
596#line 116
597 while (1) {
598 while_16_continue: ;
599 {
600#line 116
601 __cil_tmp16 = & p2;
602#line 116
603 __cil_tmp17 = *__cil_tmp16;
604#line 116
605 __cil_tmp18 = (unsigned int )__cil_tmp17;
606#line 116
607 __cil_tmp19 = __cil_tmp18 + 4;
608#line 116
609 __cil_tmp20 = *((struct node * const *)__cil_tmp19);
610#line 116
611 __cil_tmp21 = ! __cil_tmp20;
612#line 116
613 if (! __cil_tmp21) {
614 {
615#line 116
616 fail();
617 }
618 } else {
619
620 }
621 }
622 goto while_16_break;
623 }
624 while_16_break: ;
625 }
626 {
627#line 118
628 init_back_link(list);
629 }
630 {
631#line 119
632 while (1) {
633 while_17_continue: ;
634 goto while_17_break;
635 }
636 while_17_break: ;
637 }
638 {
639#line 120
640 __cil_tmp22 = & p1;
641#line 120
642 __cil_tmp23 = *__cil_tmp22;
643#line 120
644 __cil_tmp24 = & p2;
645#line 120
646 __cil_tmp25 = *__cil_tmp24;
647#line 120
648 check_seq_next(__cil_tmp23, __cil_tmp25);
649#line 121
650 __cil_tmp26 = & p2;
651#line 121
652 __cil_tmp27 = *__cil_tmp26;
653#line 121
654 __cil_tmp28 = & p1;
655#line 121
656 __cil_tmp29 = *__cil_tmp28;
657#line 121
658 check_seq_prev(__cil_tmp27, __cil_tmp29);
659#line 123
660 reverse_dll(list);
661 }
662 {
663#line 124
664 while (1) {
665 while_18_continue: ;
666 goto while_18_break;
667 }
668 while_18_break: ;
669 }
670 {
671#line 125
672 __cil_tmp30 = & p1;
673#line 125
674 __cil_tmp31 = *__cil_tmp30;
675#line 125
676 __cil_tmp32 = & p2;
677#line 125
678 __cil_tmp33 = *__cil_tmp32;
679#line 125
680 check_seq_prev(__cil_tmp31, __cil_tmp33);
681#line 126
682 __cil_tmp34 = & p2;
683#line 126
684 __cil_tmp35 = *__cil_tmp34;
685#line 126
686 __cil_tmp36 = & p1;
687#line 126
688 __cil_tmp37 = *__cil_tmp36;
689#line 126
690 check_seq_next(__cil_tmp35, __cil_tmp37);
691#line 128
692 remove_fw_link(list);
693 }
694 {
695#line 129
696 while (1) {
697 while_19_continue: ;
698 goto while_19_break;
699 }
700 while_19_break: ;
701 }
702 {
703#line 130
704 __cil_tmp38 = & p1;
705#line 130
706 __cil_tmp39 = *__cil_tmp38;
707#line 130
708 __cil_tmp40 = & p2;
709#line 130
710 __cil_tmp41 = *__cil_tmp40;
711#line 130
712 check_seq_prev(__cil_tmp39, __cil_tmp41);
713 }
714 {
715#line 132
716 while (1) {
717 while_20_continue: ;
718#line 132
719 if (list) {
720
721 } else {
722 goto while_20_break;
723 }
724 {
725#line 133
726 __cil_tmp42 = (unsigned int )list;
727#line 133
728 __cil_tmp43 = __cil_tmp42 + 4;
729#line 133
730 prev = *((struct node **)__cil_tmp43);
731#line 134
732 __cil_tmp44 = (void *)list;
733#line 134
734 free(__cil_tmp44);
735#line 135
736 list = prev;
737 }
738 }
739 while_20_break: ;
740 }
741#line 138
742 return (0);
743}
744}