1
2
3
4#line 10 "files/rule57_ebda_blast.c"
5struct hotplug_slot;
6#line 10
7struct hotplug_slot;
8#line 12 "files/rule57_ebda_blast.c"
9struct bus_info {
10
11};
12#line 15 "files/rule57_ebda_blast.c"
13struct slot {
14 int a ;
15 int b ;
16 struct hotplug_slot *hotplug_slot ;
17 struct bus_info *bus_on ;
18};
19#line 22 "files/rule57_ebda_blast.c"
20struct hotplug_slot {
21 struct slot *private ;
22 int b ;
23};
24#line 2 "./assert.h"
25void __blast_assert(void)
26{
27
28 {
29 ERROR:assert(0);
30#line 4
31 goto ERROR;
32}
33}
34#line 32 "files/rule57_ebda_blast.c"
35struct slot *tmp_slot ;
36#line 33 "files/rule57_ebda_blast.c"
37int used_tmp_slot = 0;
38#line 34 "files/rule57_ebda_blast.c"
39int freed_tmp_slot = 1;
40#line 36
41extern void *kzalloc(int , int ) ;
42#line 38 "files/rule57_ebda_blast.c"
43void kfree(void *p )
44{ void *__cil_tmp2 ;
45 unsigned int __cil_tmp3 ;
46 unsigned int __cil_tmp4 ;
47 unsigned int __cil_tmp5 ;
48 unsigned int __cil_tmp6 ;
49
50 {
51 {
52#line 39
53 __cil_tmp2 = (void *)0;
54#line 39
55 __cil_tmp3 = (unsigned int )__cil_tmp2;
56#line 39
57 __cil_tmp4 = (unsigned int )p;
58#line 39
59 if (__cil_tmp4 != __cil_tmp3) {
60 {
61#line 39
62 __cil_tmp5 = (unsigned int )tmp_slot;
63#line 39
64 __cil_tmp6 = (unsigned int )p;
65#line 39
66 if (__cil_tmp6 == __cil_tmp5) {
67#line 40
68 freed_tmp_slot = 1;
69 } else {
70
71 }
72 }
73 } else {
74
75 }
76 }
77#line 41
78 return;
79}
80}
81#line 44
82extern void *__VERIFIER_nondet_pointer(void) ;
83#line 45 "files/rule57_ebda_blast.c"
84static struct bus_info *ibmphp_find_same_bus_num(void)
85{ void *tmp ;
86
87 {
88 {
89#line 47
90 tmp = __VERIFIER_nondet_pointer();
91 }
92#line 47
93 return ((struct bus_info *)tmp);
94}
95}
96#line 46
97extern int __VERIFIER_nondet_int(void) ;
98#line 47 "files/rule57_ebda_blast.c"
99static int fillslotinfo(struct hotplug_slot *ptr )
100{ int tmp ;
101
102 {
103 {
104#line 49
105 tmp = __VERIFIER_nondet_int();
106 }
107#line 49
108 return (tmp);
109}
110}
111#line 47 "files/rule57_ebda_blast.c"
112static int ibmphp_init_devno(struct slot **ptr )
113{ int tmp ;
114
115 {
116 {
117#line 49
118 tmp = __VERIFIER_nondet_int();
119 }
120#line 49
121 return (tmp);
122}
123}
124#line 49 "files/rule57_ebda_blast.c"
125int ebda_rsrc_controller(void)
126{ struct hotplug_slot *hp_slot_ptr ;
127 struct bus_info *bus_info_ptr1 ;
128 int rc ;
129 void *tmp ;
130 void *tmp___0 ;
131 int __cil_tmp6 ;
132 int __cil_tmp7 ;
133 struct slot **__cil_tmp8 ;
134 struct slot *__cil_tmp9 ;
135 void *__cil_tmp10 ;
136
137 {
138 {
139#line 54
140 __cil_tmp6 = (int )8U;
141#line 54
142 tmp = kzalloc(__cil_tmp6, 1);
143#line 54
144 hp_slot_ptr = (struct hotplug_slot *)tmp;
145 }
146#line 55
147 if (! hp_slot_ptr) {
148#line 56
149 rc = -2;
150#line 57
151 goto error_no_slot;
152 } else {
153
154 }
155 {
156#line 59
157 hp_slot_ptr->b = 5;
158#line 61
159 __cil_tmp7 = (int )16U;
160#line 61
161 tmp___0 = kzalloc(__cil_tmp7, 1);
162#line 61
163 tmp_slot = (struct slot *)tmp___0;
164 }
165#line 63
166 if (! tmp_slot) {
167#line 64
168 rc = -2;
169#line 65
170 goto error_no_slot;
171 } else {
172
173 }
174 {
175#line 68
176 used_tmp_slot = 0;
177#line 69
178 freed_tmp_slot = 0;
179#line 71
180 tmp_slot->a = 2;
181#line 72
182 tmp_slot->b = 3;
183#line 74
184 bus_info_ptr1 = ibmphp_find_same_bus_num();
185 }
186#line 75
187 if (! bus_info_ptr1) {
188#line 76
189 rc = -3;
190#line 82
191 goto error;
192 } else {
193
194 }
195 {
196#line 84
197 tmp_slot->bus_on = bus_info_ptr1;
198#line 85
199 bus_info_ptr1 = (struct bus_info *)0;
200#line 87
201 tmp_slot->hotplug_slot = hp_slot_ptr;
202#line 89
203 hp_slot_ptr->private = tmp_slot;
204#line 90
205 used_tmp_slot = 1;
206#line 92
207 rc = fillslotinfo(hp_slot_ptr);
208 }
209#line 93
210 if (rc) {
211#line 94
212 goto error;
213 } else {
214
215 }
216 {
217#line 96
218 __cil_tmp8 = & hp_slot_ptr->private;
219#line 96
220 rc = ibmphp_init_devno(__cil_tmp8);
221 }
222#line 97
223 if (rc) {
224#line 98
225 goto error;
226 } else {
227
228 }
229#line 100
230 return (0);
231 error:
232 {
233#line 103
234 __cil_tmp9 = hp_slot_ptr->private;
235#line 103
236 __cil_tmp10 = (void *)__cil_tmp9;
237#line 103
238 kfree(__cil_tmp10);
239 }
240 error_no_slot:
241#line 108
242 return (rc);
243}
244}
245#line 111 "files/rule57_ebda_blast.c"
246int main(void)
247{
248
249 {
250 {
251#line 112
252 ebda_rsrc_controller();
253 }
254#line 113
255 if (! used_tmp_slot) {
256#line 114
257 if (freed_tmp_slot) {
258
259 } else {
260 {
261#line 114
262 __blast_assert();
263 }
264 }
265 } else {
266
267 }
268#line 115
269 return;
270}
271}