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