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:
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 void *__cil_tmp8 ;
134 struct slot **__cil_tmp9 ;
135 struct slot *__cil_tmp10 ;
136 void *__cil_tmp11 ;
137
138 {
139 {
140#line 54
141 __cil_tmp6 = (int )8U;
142#line 54
143 tmp = kzalloc(__cil_tmp6, 1);
144#line 54
145 hp_slot_ptr = (struct hotplug_slot *)tmp;
146 }
147#line 55
148 if (! hp_slot_ptr) {
149#line 56
150 rc = -2;
151#line 57
152 goto error_no_slot;
153 } else {
154
155 }
156 {
157#line 59
158 hp_slot_ptr->b = 5;
159#line 61
160 __cil_tmp7 = (int )16U;
161#line 61
162 tmp___0 = kzalloc(__cil_tmp7, 1);
163#line 61
164 tmp_slot = (struct slot *)tmp___0;
165 }
166#line 63
167 if (! tmp_slot) {
168#line 64
169 rc = -2;
170#line 65
171 goto error_no_slot;
172 } else {
173
174 }
175 {
176#line 68
177 used_tmp_slot = 0;
178#line 69
179 freed_tmp_slot = 0;
180#line 71
181 tmp_slot->a = 2;
182#line 72
183 tmp_slot->b = 3;
184#line 74
185 bus_info_ptr1 = ibmphp_find_same_bus_num();
186 }
187#line 75
188 if (! bus_info_ptr1) {
189 {
190#line 76
191 rc = -3;
192#line 79
193 __cil_tmp8 = (void *)tmp_slot;
194#line 79
195 kfree(__cil_tmp8);
196#line 80
197 freed_tmp_slot = 1;
198 }
199#line 82
200 goto error;
201 } else {
202
203 }
204 {
205#line 84
206 tmp_slot->bus_on = bus_info_ptr1;
207#line 85
208 bus_info_ptr1 = (struct bus_info *)0;
209#line 87
210 tmp_slot->hotplug_slot = hp_slot_ptr;
211#line 89
212 hp_slot_ptr->private = tmp_slot;
213#line 90
214 used_tmp_slot = 1;
215#line 92
216 rc = fillslotinfo(hp_slot_ptr);
217 }
218#line 93
219 if (rc) {
220#line 94
221 goto error;
222 } else {
223
224 }
225 {
226#line 96
227 __cil_tmp9 = & hp_slot_ptr->private;
228#line 96
229 rc = ibmphp_init_devno(__cil_tmp9);
230 }
231#line 97
232 if (rc) {
233#line 98
234 goto error;
235 } else {
236
237 }
238#line 100
239 return (0);
240 error:
241 {
242#line 103
243 __cil_tmp10 = hp_slot_ptr->private;
244#line 103
245 __cil_tmp11 = (void *)__cil_tmp10;
246#line 103
247 kfree(__cil_tmp11);
248 }
249 error_no_slot:
250#line 108
251 return (rc);
252}
253}
254#line 111 "files/rule57_ebda_blast.c"
255void main(void)
256{
257
258 {
259 {
260#line 112
261 ebda_rsrc_controller();
262 }
263#line 113
264 if (! used_tmp_slot) {
265#line 114
266 if (freed_tmp_slot) {
267
268 } else {
269 {
270#line 114
271 __blast_assert();
272 }
273 }
274 } else {
275
276 }
277#line 115
278 return;
279}
280}