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