1
2extern void __assert_fail (__const char *__assertion, __const char *__file,
3 unsigned int __line, __const char *__function)
4 __attribute__ ((__nothrow__ , __leaf__)) __attribute__ ((__noreturn__));
5extern void __assert_perror_fail (int __errnum, __const char *__file,
6 unsigned int __line,
7 __const char *__function)
8 __attribute__ ((__nothrow__ , __leaf__)) __attribute__ ((__noreturn__));
9extern void __assert (const char *__assertion, const char *__file, int __line)
10 __attribute__ ((__nothrow__ , __leaf__)) __attribute__ ((__noreturn__));
11
12typedef unsigned int size_t;
13
14
15
16
17struct list_head {
18 struct list_head *next ;
19 struct list_head *prev ;
20};
21struct node {
22 int value ;
23 struct list_head linkage ;
24 struct list_head nested ;
25};
26extern __attribute__((__nothrow__)) void *malloc(size_t __size ) __attribute__((__malloc__)) ;
27extern __attribute__((__nothrow__)) void free(void *__ptr ) ;
28extern __attribute__((__nothrow__, __noreturn__)) void abort(void) ;
29extern int __VERIFIER_nondet_int(void);
30static void fail(void)
31{
32 {
33 ERROR: ((0) ? (void) (0) : __assert_fail ("0", "test-0180.c", 11, __PRETTY_FUNCTION__));
34 goto ERROR;
35}
36}
37
38
39struct list_head gl_list = {& gl_list, & gl_list};
40
41static void inspect(struct list_head const *head )
42{ struct node const *node ;
43 unsigned int __cil_tmp3 ;
44 struct list_head *__cil_tmp4 ;
45 unsigned int __cil_tmp5 ;
46 int __cil_tmp6 ;
47 unsigned int __cil_tmp7 ;
48 unsigned int __cil_tmp8 ;
49 unsigned int __cil_tmp9 ;
50 struct list_head *__cil_tmp10 ;
51 unsigned int __cil_tmp11 ;
52 int __cil_tmp12 ;
53 unsigned int __cil_tmp13 ;
54 unsigned int __cil_tmp14 ;
55 struct list_head *__cil_tmp15 ;
56 unsigned int __cil_tmp16 ;
57 struct list_head *__cil_tmp17 ;
58 unsigned int __cil_tmp18 ;
59 int __cil_tmp19 ;
60 unsigned int __cil_tmp20 ;
61 unsigned int __cil_tmp21 ;
62 unsigned int __cil_tmp22 ;
63 struct list_head *__cil_tmp23 ;
64 unsigned int __cil_tmp24 ;
65 int __cil_tmp25 ;
66 struct node *__cil_tmp26 ;
67 unsigned int __cil_tmp27 ;
68 unsigned int __cil_tmp28 ;
69 struct list_head *__cil_tmp29 ;
70 unsigned long __cil_tmp30 ;
71 char *__cil_tmp31 ;
72 char *__cil_tmp32 ;
73 struct node *__cil_tmp33 ;
74 unsigned int __cil_tmp34 ;
75 unsigned int __cil_tmp35 ;
76 struct list_head const *__cil_tmp36 ;
77 unsigned int __cil_tmp37 ;
78 unsigned int __cil_tmp38 ;
79 unsigned int __cil_tmp39 ;
80 struct list_head *__cil_tmp40 ;
81 unsigned int __cil_tmp41 ;
82 int __cil_tmp42 ;
83 unsigned int __cil_tmp43 ;
84 unsigned int __cil_tmp44 ;
85 struct list_head const *__cil_tmp45 ;
86 unsigned int __cil_tmp46 ;
87 unsigned int __cil_tmp47 ;
88 unsigned int __cil_tmp48 ;
89 unsigned int __cil_tmp49 ;
90 struct list_head *__cil_tmp50 ;
91 unsigned int __cil_tmp51 ;
92 int __cil_tmp52 ;
93 unsigned int __cil_tmp53 ;
94 unsigned int __cil_tmp54 ;
95 struct list_head const *__cil_tmp55 ;
96 unsigned int __cil_tmp56 ;
97 unsigned int __cil_tmp57 ;
98 unsigned int __cil_tmp58 ;
99 struct list_head *__cil_tmp59 ;
100 unsigned int __cil_tmp60 ;
101 int __cil_tmp61 ;
102 unsigned int __cil_tmp62 ;
103 unsigned int __cil_tmp63 ;
104 struct list_head const *__cil_tmp64 ;
105 unsigned int __cil_tmp65 ;
106 unsigned int __cil_tmp66 ;
107 unsigned int __cil_tmp67 ;
108 unsigned int __cil_tmp68 ;
109 struct list_head *__cil_tmp69 ;
110 unsigned int __cil_tmp70 ;
111 int __cil_tmp71 ;
112 struct node const *__cil_tmp72 ;
113 unsigned int __cil_tmp73 ;
114 unsigned int __cil_tmp74 ;
115 int __cil_tmp75 ;
116 unsigned int __cil_tmp76 ;
117 unsigned int __cil_tmp77 ;
118 struct list_head const *__cil_tmp78 ;
119 struct node const *__cil_tmp79 ;
120 unsigned int __cil_tmp80 ;
121 unsigned int __cil_tmp81 ;
122 int __cil_tmp82 ;
123 int const *__cil_tmp83 ;
124 struct node const *__cil_tmp84 ;
125 unsigned int __cil_tmp85 ;
126 unsigned int __cil_tmp86 ;
127 int __cil_tmp87 ;
128 unsigned int __cil_tmp88 ;
129 unsigned int __cil_tmp89 ;
130 struct list_head *__cil_tmp90 ;
131 unsigned int __cil_tmp91 ;
132 unsigned int __cil_tmp92 ;
133 struct list_head *__cil_tmp93 ;
134 unsigned int __cil_tmp94 ;
135 unsigned int __cil_tmp95 ;
136 int __cil_tmp96 ;
137 unsigned int __cil_tmp97 ;
138 unsigned int __cil_tmp98 ;
139 unsigned int __cil_tmp99 ;
140 struct list_head *__cil_tmp100 ;
141 struct list_head *__cil_tmp101 ;
142 unsigned int __cil_tmp102 ;
143 unsigned int __cil_tmp103 ;
144 int __cil_tmp104 ;
145 struct list_head *__cil_tmp105 ;
146 unsigned int __cil_tmp106 ;
147 unsigned int __cil_tmp107 ;
148 unsigned int __cil_tmp108 ;
149 struct list_head const *__cil_tmp109 ;
150 unsigned int __cil_tmp110 ;
151 struct list_head *__cil_tmp111 ;
152 unsigned int __cil_tmp112 ;
153 struct node *__cil_tmp113 ;
154 unsigned int __cil_tmp114 ;
155 unsigned int __cil_tmp115 ;
156 struct list_head *__cil_tmp116 ;
157 unsigned long __cil_tmp117 ;
158 char *__cil_tmp118 ;
159 char *__cil_tmp119 ;
160 struct node *__cil_tmp120 ;
161 unsigned int __cil_tmp121 ;
162 int __cil_tmp122 ;
163
164 {
165 {
166 while (1) {
167 while_0_continue: ;
168 if (! head) {
169 {
170 fail();
171 }
172 } else {
173 }
174 goto while_0_break;
175 }
176 while_0_break: ;
177 }
178 {
179 while (1) {
180 while_1_continue: ;
181 {
182 __cil_tmp3 = (unsigned int )head;
183 __cil_tmp4 = *((struct list_head * const *)head);
184 __cil_tmp5 = (unsigned int )__cil_tmp4;
185 __cil_tmp6 = __cil_tmp5 != __cil_tmp3;
186 if (! __cil_tmp6) {
187 {
188 fail();
189 }
190 } else {
191 }
192 }
193 goto while_1_break;
194 }
195 while_1_break: ;
196 }
197 {
198 while (1) {
199 while_2_continue: ;
200 {
201 __cil_tmp7 = (unsigned int )head;
202 __cil_tmp8 = (unsigned int )head;
203 __cil_tmp9 = __cil_tmp8 + 4;
204 __cil_tmp10 = *((struct list_head * const *)__cil_tmp9);
205 __cil_tmp11 = (unsigned int )__cil_tmp10;
206 __cil_tmp12 = __cil_tmp11 != __cil_tmp7;
207 if (! __cil_tmp12) {
208 {
209 fail();
210 }
211 } else {
212 }
213 }
214 goto while_2_break;
215 }
216 while_2_break: ;
217 }
218 __cil_tmp13 = (unsigned int )head;
219 __cil_tmp14 = __cil_tmp13 + 4;
220 __cil_tmp15 = *((struct list_head * const *)__cil_tmp14);
221 head = (struct list_head const *)__cil_tmp15;
222 {
223 while (1) {
224 while_3_continue: ;
225 if (! head) {
226 {
227 fail();
228 }
229 } else {
230 }
231 goto while_3_break;
232 }
233 while_3_break: ;
234 }
235 {
236 while (1) {
237 while_4_continue: ;
238 {
239 __cil_tmp16 = (unsigned int )head;
240 __cil_tmp17 = *((struct list_head * const *)head);
241 __cil_tmp18 = (unsigned int )__cil_tmp17;
242 __cil_tmp19 = __cil_tmp18 != __cil_tmp16;
243 if (! __cil_tmp19) {
244 {
245 fail();
246 }
247 } else {
248 }
249 }
250 goto while_4_break;
251 }
252 while_4_break: ;
253 }
254 {
255 while (1) {
256 while_5_continue: ;
257 {
258 __cil_tmp20 = (unsigned int )head;
259 __cil_tmp21 = (unsigned int )head;
260 __cil_tmp22 = __cil_tmp21 + 4;
261 __cil_tmp23 = *((struct list_head * const *)__cil_tmp22);
262 __cil_tmp24 = (unsigned int )__cil_tmp23;
263 __cil_tmp25 = __cil_tmp24 != __cil_tmp20;
264 if (! __cil_tmp25) {
265 {
266 fail();
267 }
268 } else {
269 }
270 }
271 goto while_5_break;
272 }
273 while_5_break: ;
274 }
275 __cil_tmp26 = (struct node *)0;
276 __cil_tmp27 = (unsigned int )__cil_tmp26;
277 __cil_tmp28 = __cil_tmp27 + 4;
278 __cil_tmp29 = (struct list_head *)__cil_tmp28;
279 __cil_tmp30 = (unsigned long )__cil_tmp29;
280 __cil_tmp31 = (char *)head;
281 __cil_tmp32 = __cil_tmp31 - __cil_tmp30;
282 __cil_tmp33 = (struct node *)__cil_tmp32;
283 node = (struct node const *)__cil_tmp33;
284 {
285 while (1) {
286 while_6_continue: ;
287 if (! node) {
288 {
289 fail();
290 }
291 } else {
292 }
293 goto while_6_break;
294 }
295 while_6_break: ;
296 }
297 {
298 while (1) {
299 while_7_continue: ;
300 {
301 __cil_tmp34 = (unsigned int )node;
302 __cil_tmp35 = __cil_tmp34 + 12;
303 __cil_tmp36 = (struct list_head const *)__cil_tmp35;
304 __cil_tmp37 = (unsigned int )__cil_tmp36;
305 __cil_tmp38 = (unsigned int )node;
306 __cil_tmp39 = __cil_tmp38 + 12;
307 __cil_tmp40 = *((struct list_head * const *)__cil_tmp39);
308 __cil_tmp41 = (unsigned int )__cil_tmp40;
309 __cil_tmp42 = __cil_tmp41 == __cil_tmp37;
310 if (! __cil_tmp42) {
311 {
312 fail();
313 }
314 } else {
315 }
316 }
317 goto while_7_break;
318 }
319 while_7_break: ;
320 }
321 {
322 while (1) {
323 while_8_continue: ;
324 {
325 __cil_tmp43 = (unsigned int )node;
326 __cil_tmp44 = __cil_tmp43 + 12;
327 __cil_tmp45 = (struct list_head const *)__cil_tmp44;
328 __cil_tmp46 = (unsigned int )__cil_tmp45;
329 __cil_tmp47 = 12 + 4;
330 __cil_tmp48 = (unsigned int )node;
331 __cil_tmp49 = __cil_tmp48 + __cil_tmp47;
332 __cil_tmp50 = *((struct list_head * const *)__cil_tmp49);
333 __cil_tmp51 = (unsigned int )__cil_tmp50;
334 __cil_tmp52 = __cil_tmp51 == __cil_tmp46;
335 if (! __cil_tmp52) {
336 {
337 fail();
338 }
339 } else {
340 }
341 }
342 goto while_8_break;
343 }
344 while_8_break: ;
345 }
346 {
347 while (1) {
348 while_9_continue: ;
349 {
350 __cil_tmp53 = (unsigned int )node;
351 __cil_tmp54 = __cil_tmp53 + 4;
352 __cil_tmp55 = (struct list_head const *)__cil_tmp54;
353 __cil_tmp56 = (unsigned int )__cil_tmp55;
354 __cil_tmp57 = (unsigned int )node;
355 __cil_tmp58 = __cil_tmp57 + 12;
356 __cil_tmp59 = *((struct list_head * const *)__cil_tmp58);
357 __cil_tmp60 = (unsigned int )__cil_tmp59;
358 __cil_tmp61 = __cil_tmp60 != __cil_tmp56;
359 if (! __cil_tmp61) {
360 {
361 fail();
362 }
363 } else {
364 }
365 }
366 goto while_9_break;
367 }
368 while_9_break: ;
369 }
370 {
371 while (1) {
372 while_10_continue: ;
373 {
374 __cil_tmp62 = (unsigned int )node;
375 __cil_tmp63 = __cil_tmp62 + 4;
376 __cil_tmp64 = (struct list_head const *)__cil_tmp63;
377 __cil_tmp65 = (unsigned int )__cil_tmp64;
378 __cil_tmp66 = 12 + 4;
379 __cil_tmp67 = (unsigned int )node;
380 __cil_tmp68 = __cil_tmp67 + __cil_tmp66;
381 __cil_tmp69 = *((struct list_head * const *)__cil_tmp68);
382 __cil_tmp70 = (unsigned int )__cil_tmp69;
383 __cil_tmp71 = __cil_tmp70 != __cil_tmp65;
384 if (! __cil_tmp71) {
385 {
386 fail();
387 }
388 } else {
389 }
390 }
391 goto while_10_break;
392 }
393 while_10_break: ;
394 }
395 {
396 while (1) {
397 while_11_continue: ;
398 {
399 __cil_tmp72 = (struct node const *)head;
400 __cil_tmp73 = (unsigned int )__cil_tmp72;
401 __cil_tmp74 = (unsigned int )node;
402 __cil_tmp75 = __cil_tmp74 != __cil_tmp73;
403 if (! __cil_tmp75) {
404 {
405 fail();
406 }
407 } else {
408 }
409 }
410 goto while_11_break;
411 }
412 while_11_break: ;
413 }
414 {
415 while (1) {
416 while_12_continue: ;
417 {
418 __cil_tmp76 = (unsigned int )node;
419 __cil_tmp77 = __cil_tmp76 + 4;
420 __cil_tmp78 = (struct list_head const *)__cil_tmp77;
421 __cil_tmp79 = (struct node const *)__cil_tmp78;
422 __cil_tmp80 = (unsigned int )__cil_tmp79;
423 __cil_tmp81 = (unsigned int )node;
424 __cil_tmp82 = __cil_tmp81 != __cil_tmp80;
425 if (! __cil_tmp82) {
426 {
427 fail();
428 }
429 } else {
430 }
431 }
432 goto while_12_break;
433 }
434 while_12_break: ;
435 }
436 {
437 while (1) {
438 while_13_continue: ;
439 {
440 __cil_tmp83 = (int const *)node;
441 __cil_tmp84 = (struct node const *)__cil_tmp83;
442 __cil_tmp85 = (unsigned int )__cil_tmp84;
443 __cil_tmp86 = (unsigned int )node;
444 __cil_tmp87 = __cil_tmp86 == __cil_tmp85;
445 if (! __cil_tmp87) {
446 {
447 fail();
448 }
449 } else {
450 }
451 }
452 goto while_13_break;
453 }
454 while_13_break: ;
455 }
456 {
457 while (1) {
458 while_14_continue: ;
459 {
460 __cil_tmp88 = (unsigned int )node;
461 __cil_tmp89 = __cil_tmp88 + 4;
462 __cil_tmp90 = *((struct list_head * const *)__cil_tmp89);
463 __cil_tmp91 = (unsigned int )__cil_tmp90;
464 __cil_tmp92 = __cil_tmp91 + 4;
465 __cil_tmp93 = *((struct list_head **)__cil_tmp92);
466 __cil_tmp94 = (unsigned int )__cil_tmp93;
467 __cil_tmp95 = (unsigned int )head;
468 __cil_tmp96 = __cil_tmp95 == __cil_tmp94;
469 if (! __cil_tmp96) {
470 {
471 fail();
472 }
473 } else {
474 }
475 }
476 goto while_14_break;
477 }
478 while_14_break: ;
479 }
480 {
481 while (1) {
482 while_15_continue: ;
483 {
484 __cil_tmp97 = 4 + 4;
485 __cil_tmp98 = (unsigned int )node;
486 __cil_tmp99 = __cil_tmp98 + __cil_tmp97;
487 __cil_tmp100 = *((struct list_head * const *)__cil_tmp99);
488 __cil_tmp101 = *((struct list_head **)__cil_tmp100);
489 __cil_tmp102 = (unsigned int )__cil_tmp101;
490 __cil_tmp103 = (unsigned int )head;
491 __cil_tmp104 = __cil_tmp103 == __cil_tmp102;
492 if (! __cil_tmp104) {
493 {
494 fail();
495 }
496 } else {
497 }
498 }
499 goto while_15_break;
500 }
501 while_15_break: ;
502 }
503 __cil_tmp105 = *((struct list_head * const *)head);
504 head = (struct list_head const *)__cil_tmp105;
505 {
506 while (1) {
507 while_16_continue: ;
508 {
509 __cil_tmp106 = (unsigned int )head;
510 __cil_tmp107 = (unsigned int )node;
511 __cil_tmp108 = __cil_tmp107 + 4;
512 __cil_tmp109 = (struct list_head const *)__cil_tmp108;
513 __cil_tmp110 = (unsigned int )__cil_tmp109;
514 if (__cil_tmp110 != __cil_tmp106) {
515 } else {
516 goto while_16_break;
517 }
518 }
519 __cil_tmp111 = *((struct list_head * const *)head);
520 head = (struct list_head const *)__cil_tmp111;
521 }
522 while_16_break: ;
523 }
524 {
525 while (1) {
526 while_17_continue: ;
527 {
528 __cil_tmp112 = (unsigned int )node;
529 __cil_tmp113 = (struct node *)0;
530 __cil_tmp114 = (unsigned int )__cil_tmp113;
531 __cil_tmp115 = __cil_tmp114 + 4;
532 __cil_tmp116 = (struct list_head *)__cil_tmp115;
533 __cil_tmp117 = (unsigned long )__cil_tmp116;
534 __cil_tmp118 = (char *)head;
535 __cil_tmp119 = __cil_tmp118 - __cil_tmp117;
536 __cil_tmp120 = (struct node *)__cil_tmp119;
537 __cil_tmp121 = (unsigned int )__cil_tmp120;
538 __cil_tmp122 = __cil_tmp121 == __cil_tmp112;
539 if (! __cil_tmp122) {
540 {
541 fail();
542 }
543 } else {
544 }
545 }
546 goto while_17_break;
547 }
548 while_17_break: ;
549 }
550 return;
551}
552}
553__inline static void __list_add(struct list_head *new , struct list_head *prev , struct list_head *next )
554{ unsigned int __cil_tmp4 ;
555 unsigned int __cil_tmp5 ;
556 unsigned int __cil_tmp6 ;
557 unsigned int __cil_tmp7 ;
558 {
559 __cil_tmp4 = (unsigned int )next;
560 __cil_tmp5 = __cil_tmp4 + 4;
561 *((struct list_head **)__cil_tmp5) = new;
562 *((struct list_head **)new) = next;
563 __cil_tmp6 = (unsigned int )new;
564 __cil_tmp7 = __cil_tmp6 + 4;
565 *((struct list_head **)__cil_tmp7) = prev;
566 *((struct list_head **)prev) = new;
567 return;
568}
569}
570__inline static void __list_del(struct list_head *prev , struct list_head *next )
571{ unsigned int __cil_tmp3 ;
572 unsigned int __cil_tmp4 ;
573 {
574 __cil_tmp3 = (unsigned int )next;
575 __cil_tmp4 = __cil_tmp3 + 4;
576 *((struct list_head **)__cil_tmp4) = prev;
577 *((struct list_head **)prev) = next;
578 return;
579}
580}
581__inline static void list_add(struct list_head *new , struct list_head *head )
582{ struct list_head *__cil_tmp3 ;
583 {
584 {
585 __cil_tmp3 = *((struct list_head **)head);
586 __list_add(new, head, __cil_tmp3);
587 }
588 return;
589}
590}
591__inline static void list_move(struct list_head *list , struct list_head *head )
592{ unsigned int __cil_tmp3 ;
593 unsigned int __cil_tmp4 ;
594 struct list_head *__cil_tmp5 ;
595 struct list_head *__cil_tmp6 ;
596 {
597 {
598 __cil_tmp3 = (unsigned int )list;
599 __cil_tmp4 = __cil_tmp3 + 4;
600 __cil_tmp5 = *((struct list_head **)__cil_tmp4);
601 __cil_tmp6 = *((struct list_head **)list);
602 __list_del(__cil_tmp5, __cil_tmp6);
603 list_add(list, head);
604 }
605 return;
606}
607}
608static void gl_insert(int value )
609{ struct node *node ;
610 void *tmp ;
611 unsigned int __cil_tmp4 ;
612 unsigned int __cil_tmp5 ;
613 unsigned int __cil_tmp6 ;
614 struct list_head *__cil_tmp7 ;
615 unsigned int __cil_tmp8 ;
616 unsigned int __cil_tmp9 ;
617 unsigned int __cil_tmp10 ;
618 unsigned int __cil_tmp11 ;
619 unsigned int __cil_tmp12 ;
620 unsigned int __cil_tmp13 ;
621 unsigned int __cil_tmp14 ;
622 unsigned int __cil_tmp15 ;
623 {
624 {
625 __cil_tmp4 = (unsigned int )20UL;
626 tmp = malloc(__cil_tmp4);
627 node = (struct node *)tmp;
628 }
629 if (! node) {
630 {
631 abort();
632 }
633 } else {
634 }
635 {
636 *((int *)node) = value;
637 __cil_tmp5 = (unsigned int )node;
638 __cil_tmp6 = __cil_tmp5 + 4;
639 __cil_tmp7 = (struct list_head *)__cil_tmp6;
640 list_add(__cil_tmp7, & gl_list);
641 }
642 {
643 while (1) {
644 while_18_continue: ;
645 __cil_tmp8 = (unsigned int )node;
646 __cil_tmp9 = __cil_tmp8 + 12;
647 __cil_tmp10 = (unsigned int )node;
648 __cil_tmp11 = __cil_tmp10 + 12;
649 *((struct list_head **)__cil_tmp9) = (struct list_head *)__cil_tmp11;
650 __cil_tmp12 = (unsigned int )node;
651 __cil_tmp13 = __cil_tmp12 + 12;
652 __cil_tmp14 = (unsigned int )node;
653 __cil_tmp15 = __cil_tmp14 + 12;
654 *((struct list_head **)__cil_tmp13) = (struct list_head *)__cil_tmp15;
655 goto while_18_break;
656 }
657 while_18_break: ;
658 }
659 return;
660}
661}
662static void gl_read(void)
663{ int tmp ;
664 int tmp___0 ;
665 {
666 {
667 while (1) {
668 while_19_continue: ;
669 {
670 tmp = __VERIFIER_nondet_int();
671 gl_insert(tmp);
672 tmp___0 = __VERIFIER_nondet_int();
673 }
674 if (tmp___0) {
675 } else {
676 goto while_19_break;
677 }
678 }
679 while_19_break: ;
680 }
681 return;
682}
683}
684static void gl_destroy(void)
685{ struct list_head *next ;
686 struct list_head *__cil_tmp2 ;
687 unsigned int __cil_tmp3 ;
688 unsigned int __cil_tmp4 ;
689 struct list_head *__cil_tmp5 ;
690 struct node *__cil_tmp6 ;
691 unsigned int __cil_tmp7 ;
692 unsigned int __cil_tmp8 ;
693 struct list_head *__cil_tmp9 ;
694 unsigned long __cil_tmp10 ;
695 char *__cil_tmp11 ;
696 char *__cil_tmp12 ;
697 struct node *__cil_tmp13 ;
698 void *__cil_tmp14 ;
699 {
700 {
701 while (1) {
702 while_20_continue: ;
703 __cil_tmp2 = & gl_list;
704 next = *((struct list_head **)__cil_tmp2);
705 {
706 __cil_tmp3 = (unsigned int )next;
707 __cil_tmp4 = (unsigned int )(& gl_list);
708 if (__cil_tmp4 != __cil_tmp3) {
709 } else {
710 goto while_20_break;
711 }
712 }
713 {
714 __cil_tmp5 = & gl_list;
715 *((struct list_head **)__cil_tmp5) = *((struct list_head **)next);
716 __cil_tmp6 = (struct node *)0;
717 __cil_tmp7 = (unsigned int )__cil_tmp6;
718 __cil_tmp8 = __cil_tmp7 + 4;
719 __cil_tmp9 = (struct list_head *)__cil_tmp8;
720 __cil_tmp10 = (unsigned long )__cil_tmp9;
721 __cil_tmp11 = (char *)next;
722 __cil_tmp12 = __cil_tmp11 - __cil_tmp10;
723 __cil_tmp13 = (struct node *)__cil_tmp12;
724 __cil_tmp14 = (void *)__cil_tmp13;
725 free(__cil_tmp14);
726 }
727 }
728 while_20_break: ;
729 }
730 return;
731}
732}
733static int val_from_node(struct list_head *head )
734{ struct node *entry ;
735 struct node *__cil_tmp3 ;
736 unsigned int __cil_tmp4 ;
737 unsigned int __cil_tmp5 ;
738 struct list_head *__cil_tmp6 ;
739 unsigned long __cil_tmp7 ;
740 char *__cil_tmp8 ;
741 char *__cil_tmp9 ;
742 {
743 __cil_tmp3 = (struct node *)0;
744 __cil_tmp4 = (unsigned int )__cil_tmp3;
745 __cil_tmp5 = __cil_tmp4 + 4;
746 __cil_tmp6 = (struct list_head *)__cil_tmp5;
747 __cil_tmp7 = (unsigned long )__cil_tmp6;
748 __cil_tmp8 = (char *)head;
749 __cil_tmp9 = __cil_tmp8 - __cil_tmp7;
750 entry = (struct node *)__cil_tmp9;
751 return (*((int *)entry));
752}
753}
754static _Bool gl_sort_pass(void)
755{ _Bool any_change ;
756 struct list_head *pos0 ;
757 struct list_head *pos1 ;
758 int val0 ;
759 int tmp ;
760 int val1 ;
761 int tmp___0 ;
762 struct list_head *__cil_tmp8 ;
763 unsigned int __cil_tmp9 ;
764 unsigned int __cil_tmp10 ;
765 {
766 any_change = (_Bool)0;
767 __cil_tmp8 = & gl_list;
768 pos0 = *((struct list_head **)__cil_tmp8);
769 {
770 while (1) {
771 while_21_continue: ;
772 pos1 = *((struct list_head **)pos0);
773 {
774 __cil_tmp9 = (unsigned int )pos1;
775 __cil_tmp10 = (unsigned int )(& gl_list);
776 if (__cil_tmp10 != __cil_tmp9) {
777 } else {
778 goto while_21_break;
779 }
780 }
781 {
782 tmp = val_from_node(pos0);
783 val0 = tmp;
784 tmp___0 = val_from_node(pos1);
785 val1 = tmp___0;
786 }
787 if (val0 <= val1) {
788 pos0 = pos1;
789 goto while_21_continue;
790 } else {
791 }
792 {
793 any_change = (_Bool)1;
794 list_move(pos0, pos1);
795 }
796 }
797 while_21_break: ;
798 }
799 return (any_change);
800}
801}
802static void gl_sort(void)
803{ _Bool tmp ;
804 {
805 {
806 while (1) {
807 while_22_continue: ;
808 {
809 tmp = gl_sort_pass();
810 }
811 if (tmp) {
812 } else {
813 goto while_22_break;
814 }
815 }
816 while_22_break: ;
817 }
818 return;
819}
820}
821int main(void)
822{ struct list_head const *__cil_tmp1 ;
823 struct list_head const *__cil_tmp2 ;
824 {
825 {
826 gl_read();
827 __cil_tmp1 = (struct list_head const *)(& gl_list);
828 inspect(__cil_tmp1);
829 gl_sort();
830 __cil_tmp2 = (struct list_head const *)(& gl_list);
831 inspect(__cil_tmp2);
832 gl_destroy();
833 }
834 return (0);
835}
836}