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