1extern int __VERIFIER_nondet_int();
2
3
4
5#line 211 "/usr/lib/x86_64-linux-gnu/gcc/x86_64-linux-gnu/4.5.2/include/stddef.h"
6typedef unsigned long size_t;
7#line 12 "simple_built_from_end.c"
8struct node {
9 int h ;
10 struct node *n ;
11};
12#line 12 "simple_built_from_end.c"
13typedef struct node *List;
14#line 471 "/usr/include/stdlib.h"
15extern __attribute__((__nothrow__)) void *malloc(size_t __size ) __attribute__((__malloc__)) ;
16#line 544
17 __attribute__((__nothrow__, __noreturn__)) void exit(int s ) ;
18#line 8 "simple_built_from_end.c"
19 __attribute__((__nothrow__, __noreturn__)) void exit(int s ) ;
20#line 8 "simple_built_from_end.c"
21void exit(int s )
22{
23
24 {
25 _EXIT:
26 goto _EXIT;
27}
28}
29#line 21
30extern int ( __VERIFIER_nondet_int)() ;
31#line 17 "simple_built_from_end.c"
32int main(void)
33{ List t ;
34 List p ;
35 void *tmp ;
36 int tmp___0 ;
37 unsigned long __cil_tmp5 ;
38 List __cil_tmp6 ;
39 unsigned int __cil_tmp7 ;
40 unsigned int __cil_tmp8 ;
41 unsigned int __cil_tmp9 ;
42 unsigned int __cil_tmp10 ;
43 List __cil_tmp11 ;
44 unsigned int __cil_tmp12 ;
45 unsigned int __cil_tmp13 ;
46 int __cil_tmp14 ;
47 unsigned int __cil_tmp15 ;
48 unsigned int __cil_tmp16 ;
49
50 {
51#line 20
52 p = (List )0;
53 {
54#line 21
55 while (1) {
56 while_0_continue: ;
57 {
58#line 21
59 tmp___0 = __VERIFIER_nondet_int();
60 }
61#line 21
62 if (tmp___0) {
63
64 } else {
65 goto while_0_break;
66 }
67 {
68#line 22
69 __cil_tmp5 = (unsigned long )8U;
70#line 22
71 tmp = malloc(__cil_tmp5);
72#line 22
73 t = (struct node *)tmp;
74 }
75 {
76#line 23
77 __cil_tmp6 = (List )0;
78#line 23
79 __cil_tmp7 = (unsigned int )__cil_tmp6;
80#line 23
81 __cil_tmp8 = (unsigned int )t;
82#line 23
83 if (__cil_tmp8 == __cil_tmp7) {
84 {
85#line 23
86 exit(1);
87 }
88 } else {
89
90 }
91 }
92#line 24
93 *((int *)t) = 1;
94#line 25
95 __cil_tmp9 = (unsigned int )t;
96#line 25
97 __cil_tmp10 = __cil_tmp9 + 4;
98#line 25
99 *((struct node **)__cil_tmp10) = p;
100#line 26
101 p = t;
102 }
103 while_0_break: ;
104 }
105 {
106#line 28
107 while (1) {
108 while_1_continue: ;
109 {
110#line 28
111 __cil_tmp11 = (List )0;
112#line 28
113 __cil_tmp12 = (unsigned int )__cil_tmp11;
114#line 28
115 __cil_tmp13 = (unsigned int )p;
116#line 28
117 if (__cil_tmp13 != __cil_tmp12) {
118
119 } else {
120 goto while_1_break;
121 }
122 }
123 {
124#line 29
125 __cil_tmp14 = *((int *)p);
126#line 29
127 if (__cil_tmp14 != 1) {
128 ERROR:
129 goto ERROR;
130 } else {
131
132 }
133 }
134#line 32
135 __cil_tmp15 = (unsigned int )p;
136#line 32
137 __cil_tmp16 = __cil_tmp15 + 4;
138#line 32
139 p = *((struct node **)__cil_tmp16);
140 }
141 while_1_break: ;
142 }
143#line 35
144 return (0);
145}
146}