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