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 8 "alternating_list.c"
8struct node {
9 int h ;
10 struct node *n ;
11};
12#line 8 "alternating_list.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 13 "alternating_list.c"
19 __attribute__((__nothrow__, __noreturn__)) void exit(int s ) ;
20#line 13 "alternating_list.c"
21void exit(int s )
22{
23
24 {
25 _EXIT:
26 goto _EXIT;
27}
28}
29#line 25
30extern int ( __VERIFIER_nondet_int)() ;
31#line 59
32extern int ( printf)() ;
33#line 17 "alternating_list.c"
34int main(void)
35{ int flag ;
36 List a ;
37 void *tmp ;
38 List t ;
39 List p ;
40 void *tmp___0 ;
41 int tmp___1 ;
42 unsigned long __cil_tmp8 ;
43 List __cil_tmp9 ;
44 unsigned int __cil_tmp10 ;
45 unsigned int __cil_tmp11 ;
46 unsigned long __cil_tmp12 ;
47 List __cil_tmp13 ;
48 unsigned int __cil_tmp14 ;
49 unsigned int __cil_tmp15 ;
50 unsigned int __cil_tmp16 ;
51 unsigned int __cil_tmp17 ;
52 unsigned int __cil_tmp18 ;
53 unsigned int __cil_tmp19 ;
54 int __cil_tmp20 ;
55 int __cil_tmp21 ;
56 int __cil_tmp22 ;
57 unsigned int __cil_tmp23 ;
58 unsigned int __cil_tmp24 ;
59
60 {
61 {
62#line 18
63 flag = 1;
64#line 21
65 __cil_tmp8 = (unsigned long )8U;
66#line 21
67 tmp = malloc(__cil_tmp8);
68#line 21
69 a = (struct node *)tmp;
70 }
71 {
72#line 22
73 __cil_tmp9 = (List )0;
74#line 22
75 __cil_tmp10 = (unsigned int )__cil_tmp9;
76#line 22
77 __cil_tmp11 = (unsigned int )a;
78#line 22
79 if (__cil_tmp11 == __cil_tmp10) {
80 {
81#line 22
82 exit(1);
83 }
84 } else {
85
86 }
87 }
88#line 24
89 p = a;
90 {
91#line 25
92 while (1) {
93 while_0_continue: ;
94 {
95#line 25
96 tmp___1 = __VERIFIER_nondet_int();
97 }
98#line 25
99 if (tmp___1) {
100
101 } else {
102 goto while_0_break;
103 }
104#line 26
105 if (flag) {
106#line 27
107 *((int *)p) = 1;
108#line 28
109 flag = 0;
110 } else {
111#line 30
112 *((int *)p) = 2;
113#line 31
114 flag = 1;
115 }
116 {
117#line 33
118 __cil_tmp12 = (unsigned long )8U;
119#line 33
120 tmp___0 = malloc(__cil_tmp12);
121#line 33
122 t = (struct node *)tmp___0;
123 }
124 {
125#line 34
126 __cil_tmp13 = (List )0;
127#line 34
128 __cil_tmp14 = (unsigned int )__cil_tmp13;
129#line 34
130 __cil_tmp15 = (unsigned int )t;
131#line 34
132 if (__cil_tmp15 == __cil_tmp14) {
133 {
134#line 34
135 exit(1);
136 }
137 } else {
138
139 }
140 }
141#line 35
142 __cil_tmp16 = (unsigned int )p;
143#line 35
144 __cil_tmp17 = __cil_tmp16 + 4;
145#line 35
146 *((struct node **)__cil_tmp17) = t;
147#line 36
148 __cil_tmp18 = (unsigned int )p;
149#line 36
150 __cil_tmp19 = __cil_tmp18 + 4;
151#line 36
152 p = *((struct node **)__cil_tmp19);
153 }
154 while_0_break: ;
155 }
156#line 38
157 *((int *)p) = 3;
158#line 41
159 p = a;
160#line 42
161 flag = 1;
162 {
163#line 43
164 while (1) {
165 while_1_continue: ;
166 {
167#line 43
168 __cil_tmp20 = *((int *)p);
169#line 43
170 if (__cil_tmp20 != 3) {
171
172 } else {
173 goto while_1_break;
174 }
175 }
176#line 44
177 if (flag) {
178#line 45
179 flag = 0;
180 {
181#line 46
182 __cil_tmp21 = *((int *)p);
183#line 46
184 if (__cil_tmp21 != 1) {
185 goto ERROR;
186 } else {
187
188 }
189 }
190 } else {
191#line 49
192 flag = 1;
193 {
194#line 50
195 __cil_tmp22 = *((int *)p);
196#line 50
197 if (__cil_tmp22 != 2) {
198 goto ERROR;
199 } else {
200
201 }
202 }
203 }
204#line 53
205 __cil_tmp23 = (unsigned int )p;
206#line 53
207 __cil_tmp24 = __cil_tmp23 + 4;
208#line 53
209 p = *((struct node **)__cil_tmp24);
210 }
211 while_1_break: ;
212 }
213#line 56
214 return (0);
215 ERROR:
216 {
217#line 59
218 printf("Alternation violation found.\n");
219 }
220#line 60
221 return (1);
222}
223}