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 15 "splice.c"
7struct node {
8 int h ;
9 struct node *n ;
10};
11#line 15 "splice.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 11 "splice.c"
18 __attribute__((__nothrow__, __noreturn__)) void exit(int s ) ;
19#line 11 "splice.c"
20void exit(int s )
21{
22
23 {
24 _EXIT:
25 goto _EXIT;
26}
27}
28#line 32
29extern int ( __VERIFIER_nondet_int)() ;
30#line 20 "splice.c"
31int main(void)
32{ int flag ;
33 List a ;
34 void *tmp ;
35 List t ;
36 List l1 ;
37 List l2 ;
38 List p ;
39 void *tmp___0 ;
40 int tmp___1 ;
41 unsigned long __cil_tmp12 ;
42 List __cil_tmp13 ;
43 unsigned int __cil_tmp14 ;
44 unsigned int __cil_tmp15 ;
45 unsigned long __cil_tmp16 ;
46 List __cil_tmp17 ;
47 unsigned int __cil_tmp18 ;
48 unsigned int __cil_tmp19 ;
49 unsigned int __cil_tmp20 ;
50 unsigned int __cil_tmp21 ;
51 unsigned int __cil_tmp22 ;
52 unsigned int __cil_tmp23 ;
53 int __cil_tmp24 ;
54 int __cil_tmp25 ;
55 unsigned int __cil_tmp26 ;
56 unsigned int __cil_tmp27 ;
57 unsigned int __cil_tmp28 ;
58 unsigned int __cil_tmp29 ;
59 unsigned int __cil_tmp30 ;
60 unsigned int __cil_tmp31 ;
61 List __cil_tmp32 ;
62 unsigned int __cil_tmp33 ;
63 unsigned int __cil_tmp34 ;
64 int __cil_tmp35 ;
65 unsigned int __cil_tmp36 ;
66 unsigned int __cil_tmp37 ;
67 List __cil_tmp38 ;
68 unsigned int __cil_tmp39 ;
69 unsigned int __cil_tmp40 ;
70 int __cil_tmp41 ;
71 unsigned int __cil_tmp42 ;
72 unsigned int __cil_tmp43 ;
73
74 {
75 {
76#line 21
77 flag = 1;
78#line 24
79 __cil_tmp12 = (unsigned long )8U;
80#line 24
81 tmp = malloc(__cil_tmp12);
82#line 24
83 a = (struct node *)tmp;
84 }
85 {
86#line 25
87 __cil_tmp13 = (List )0;
88#line 25
89 __cil_tmp14 = (unsigned int )__cil_tmp13;
90#line 25
91 __cil_tmp15 = (unsigned int )a;
92#line 25
93 if (__cil_tmp15 == __cil_tmp14) {
94 {
95#line 25
96 exit(1);
97 }
98 } else {
99
100 }
101 }
102#line 31
103 p = a;
104 {
105#line 32
106 while (1) {
107 while_0_continue: ;
108 {
109#line 32
110 tmp___1 = __VERIFIER_nondet_int();
111 }
112#line 32
113 if (tmp___1) {
114
115 } else {
116 goto while_0_break;
117 }
118#line 33
119 if (flag) {
120#line 34
121 *((int *)p) = 1;
122#line 35
123 flag = 0;
124 } else {
125#line 37
126 *((int *)p) = 2;
127#line 38
128 flag = 1;
129 }
130 {
131#line 40
132 __cil_tmp16 = (unsigned long )8U;
133#line 40
134 tmp___0 = malloc(__cil_tmp16);
135#line 40
136 t = (struct node *)tmp___0;
137 }
138 {
139#line 41
140 __cil_tmp17 = (List )0;
141#line 41
142 __cil_tmp18 = (unsigned int )__cil_tmp17;
143#line 41
144 __cil_tmp19 = (unsigned int )t;
145#line 41
146 if (__cil_tmp19 == __cil_tmp18) {
147 {
148#line 41
149 exit(1);
150 }
151 } else {
152
153 }
154 }
155#line 42
156 __cil_tmp20 = (unsigned int )p;
157#line 42
158 __cil_tmp21 = __cil_tmp20 + 4;
159#line 42
160 *((struct node **)__cil_tmp21) = t;
161#line 43
162 __cil_tmp22 = (unsigned int )p;
163#line 43
164 __cil_tmp23 = __cil_tmp22 + 4;
165#line 43
166 p = *((struct node **)__cil_tmp23);
167 }
168 while_0_break: ;
169 }
170#line 45
171 *((int *)p) = 3;
172 {
173#line 47
174 __cil_tmp24 = *((int *)a);
175#line 47
176 if (__cil_tmp24 == 3) {
177#line 47
178 return (0);
179 } else {
180
181 }
182 }
183#line 49
184 flag = 1;
185#line 50
186 l1 = (struct node *)0;
187#line 51
188 l2 = (struct node *)0;
189#line 52
190 p = a;
191 {
192#line 53
193 while (1) {
194 while_1_continue: ;
195 {
196#line 53
197 __cil_tmp25 = *((int *)p);
198#line 53
199 if (__cil_tmp25 != 3) {
200
201 } else {
202 goto while_1_break;
203 }
204 }
205#line 54
206 t = p;
207#line 55
208 __cil_tmp26 = (unsigned int )p;
209#line 55
210 __cil_tmp27 = __cil_tmp26 + 4;
211#line 55
212 p = *((struct node **)__cil_tmp27);
213#line 56
214 if (flag) {
215#line 57
216 __cil_tmp28 = (unsigned int )t;
217#line 57
218 __cil_tmp29 = __cil_tmp28 + 4;
219#line 57
220 *((struct node **)__cil_tmp29) = l1;
221#line 58
222 l1 = t;
223#line 59
224 flag = 0;
225 } else {
226#line 61
227 __cil_tmp30 = (unsigned int )t;
228#line 61
229 __cil_tmp31 = __cil_tmp30 + 4;
230#line 61
231 *((struct node **)__cil_tmp31) = l2;
232#line 62
233 l2 = t;
234#line 63
235 flag = 1;
236 }
237 }
238 while_1_break: ;
239 }
240#line 68
241 p = l1;
242 {
243#line 69
244 while (1) {
245 while_2_continue: ;
246 {
247#line 69
248 __cil_tmp32 = (List )0;
249#line 69
250 __cil_tmp33 = (unsigned int )__cil_tmp32;
251#line 69
252 __cil_tmp34 = (unsigned int )p;
253#line 69
254 if (__cil_tmp34 != __cil_tmp33) {
255
256 } else {
257 goto while_2_break;
258 }
259 }
260 {
261#line 70
262 __cil_tmp35 = *((int *)p);
263#line 70
264 if (__cil_tmp35 != 1) {
265 goto ERROR;
266 } else {
267
268 }
269 }
270#line 71
271 __cil_tmp36 = (unsigned int )p;
272#line 71
273 __cil_tmp37 = __cil_tmp36 + 4;
274#line 71
275 p = *((struct node **)__cil_tmp37);
276 }
277 while_2_break: ;
278 }
279#line 73
280 p = l2;
281 {
282#line 74
283 while (1) {
284 while_3_continue: ;
285 {
286#line 74
287 __cil_tmp38 = (List )0;
288#line 74
289 __cil_tmp39 = (unsigned int )__cil_tmp38;
290#line 74
291 __cil_tmp40 = (unsigned int )p;
292#line 74
293 if (__cil_tmp40 != __cil_tmp39) {
294
295 } else {
296 goto while_3_break;
297 }
298 }
299 {
300#line 75
301 __cil_tmp41 = *((int *)p);
302#line 75
303 if (__cil_tmp41 != 2) {
304 goto ERROR;
305 } else {
306
307 }
308 }
309#line 76
310 __cil_tmp42 = (unsigned int )p;
311#line 76
312 __cil_tmp43 = __cil_tmp42 + 4;
313#line 76
314 p = *((struct node **)__cil_tmp43);
315 }
316 while_3_break: ;
317 }
318#line 79
319 return (0);
320 ERROR:
321#line 81
322 return (1);
323}
324}