1
2
3
4#line 211 "/usr/lib/x86_64-linux-gnu/gcc/x86_64-linux-gnu/4.5.2/include/stddef.h"
5typedef unsigned long size_t;
6#line 13 "list.c"
7struct node {
8 int h ;
9 struct node *n ;
10};
11#line 13 "list.c"
12typedef struct node *List;
13#line 471 "/usr/include/stdlib.h"
14extern __attribute__((__nothrow__)) void *malloc(size_t __size ) __attribute__((__malloc__)) ;
15#line 544
16 __attribute__((__nothrow__, __noreturn__)) void exit(int s ) ;
17#line 9 "list.c"
18 __attribute__((__nothrow__, __noreturn__)) void exit(int s ) ;
19#line 9 "list.c"
20void exit(int s )
21{
22
23 {
24 _EXIT:
25 goto _EXIT;
26}
27}
28#line 24
29extern int ( __VERIFIER_nondet_int)() ;
30#line 18 "list.c"
31void main(void)
32{ List a ;
33 void *tmp ;
34 List t ;
35 List p ;
36 void *tmp___0 ;
37 int tmp___1 ;
38 void *tmp___2 ;
39 int tmp___3 ;
40 unsigned long __cil_tmp9 ;
41 List __cil_tmp10 ;
42 unsigned int __cil_tmp11 ;
43 unsigned int __cil_tmp12 ;
44 unsigned long __cil_tmp13 ;
45 List __cil_tmp14 ;
46 unsigned int __cil_tmp15 ;
47 unsigned int __cil_tmp16 ;
48 unsigned int __cil_tmp17 ;
49 unsigned int __cil_tmp18 ;
50 unsigned int __cil_tmp19 ;
51 unsigned int __cil_tmp20 ;
52 unsigned long __cil_tmp21 ;
53 List __cil_tmp22 ;
54 unsigned int __cil_tmp23 ;
55 unsigned int __cil_tmp24 ;
56 unsigned int __cil_tmp25 ;
57 unsigned int __cil_tmp26 ;
58 unsigned int __cil_tmp27 ;
59 unsigned int __cil_tmp28 ;
60 int __cil_tmp29 ;
61 unsigned int __cil_tmp30 ;
62 unsigned int __cil_tmp31 ;
63 int __cil_tmp32 ;
64 unsigned int __cil_tmp33 ;
65 unsigned int __cil_tmp34 ;
66 int __cil_tmp35 ;
67
68 {
69 {
70#line 20
71 __cil_tmp9 = (unsigned long )8U;
72#line 20
73 tmp = malloc(__cil_tmp9);
74#line 20
75 a = (struct node *)tmp;
76 }
77 {
78#line 21
79 __cil_tmp10 = (List )0;
80#line 21
81 __cil_tmp11 = (unsigned int )__cil_tmp10;
82#line 21
83 __cil_tmp12 = (unsigned int )a;
84#line 21
85 if (__cil_tmp12 == __cil_tmp11) {
86 {
87#line 21
88 exit(1);
89 }
90 } else {
91
92 }
93 }
94#line 23
95 p = a;
96 {
97#line 24
98 while (1) {
99 while_0_continue: ;
100 {
101#line 24
102 tmp___1 = __VERIFIER_nondet_int();
103 }
104#line 24
105 if (tmp___1) {
106
107 } else {
108 goto while_0_break;
109 }
110 {
111#line 25
112 *((int *)p) = 1;
113#line 26
114 __cil_tmp13 = (unsigned long )8U;
115#line 26
116 tmp___0 = malloc(__cil_tmp13);
117#line 26
118 t = (struct node *)tmp___0;
119 }
120 {
121#line 27
122 __cil_tmp14 = (List )0;
123#line 27
124 __cil_tmp15 = (unsigned int )__cil_tmp14;
125#line 27
126 __cil_tmp16 = (unsigned int )t;
127#line 27
128 if (__cil_tmp16 == __cil_tmp15) {
129 {
130#line 27
131 exit(1);
132 }
133 } else {
134
135 }
136 }
137#line 28
138 __cil_tmp17 = (unsigned int )p;
139#line 28
140 __cil_tmp18 = __cil_tmp17 + 4;
141#line 28
142 *((struct node **)__cil_tmp18) = t;
143#line 29
144 __cil_tmp19 = (unsigned int )p;
145#line 29
146 __cil_tmp20 = __cil_tmp19 + 4;
147#line 29
148 p = *((struct node **)__cil_tmp20);
149 }
150 while_0_break: ;
151 }
152 {
153#line 31
154 while (1) {
155 while_1_continue: ;
156 {
157#line 31
158 tmp___3 = __VERIFIER_nondet_int();
159 }
160#line 31
161 if (tmp___3) {
162
163 } else {
164 goto while_1_break;
165 }
166 {
167#line 32
168 *((int *)p) = 2;
169#line 33
170 __cil_tmp21 = (unsigned long )8U;
171#line 33
172 tmp___2 = malloc(__cil_tmp21);
173#line 33
174 t = (struct node *)tmp___2;
175 }
176 {
177#line 34
178 __cil_tmp22 = (List )0;
179#line 34
180 __cil_tmp23 = (unsigned int )__cil_tmp22;
181#line 34
182 __cil_tmp24 = (unsigned int )t;
183#line 34
184 if (__cil_tmp24 == __cil_tmp23) {
185 {
186#line 34
187 exit(1);
188 }
189 } else {
190
191 }
192 }
193#line 35
194 __cil_tmp25 = (unsigned int )p;
195#line 35
196 __cil_tmp26 = __cil_tmp25 + 4;
197#line 35
198 *((struct node **)__cil_tmp26) = t;
199#line 36
200 __cil_tmp27 = (unsigned int )p;
201#line 36
202 __cil_tmp28 = __cil_tmp27 + 4;
203#line 36
204 p = *((struct node **)__cil_tmp28);
205 }
206 while_1_break: ;
207 }
208#line 38
209 *((int *)p) = 3;
210#line 41
211 p = a;
212 {
213#line 42
214 while (1) {
215 while_2_continue: ;
216 {
217#line 42
218 __cil_tmp29 = *((int *)p);
219#line 42
220 if (__cil_tmp29 == 1) {
221
222 } else {
223 goto while_2_break;
224 }
225 }
226#line 43
227 __cil_tmp30 = (unsigned int )p;
228#line 43
229 __cil_tmp31 = __cil_tmp30 + 4;
230#line 43
231 p = *((struct node **)__cil_tmp31);
232 }
233 while_2_break: ;
234 }
235 {
236#line 44
237 while (1) {
238 while_3_continue: ;
239 {
240#line 44
241 __cil_tmp32 = *((int *)p);
242#line 44
243 if (__cil_tmp32 == 2) {
244
245 } else {
246 goto while_3_break;
247 }
248 }
249#line 45
250 __cil_tmp33 = (unsigned int )p;
251#line 45
252 __cil_tmp34 = __cil_tmp33 + 4;
253#line 45
254 p = *((struct node **)__cil_tmp34);
255 }
256 while_3_break: ;
257 }
258 {
259#line 46
260 __cil_tmp35 = *((int *)p);
261#line 46
262 if (__cil_tmp35 != 3) {
263 ERROR:
264 goto ERROR;
265 } else {
266
267 }
268 }
269#line 49
270 return;
271}
272}