1# 1 "files/rule57_ebda_blast.c"
2# 1 "<built-in>"
3# 1 "<command-line>"
4# 1 "files/rule57_ebda_blast.c"
5# 1 "./assert.h" 1
6
7void __blast_assert()
8{
9 ERROR: goto ERROR;
10}
11# 2 "files/rule57_ebda_blast.c" 2
12
13
14
15
16
17
18
19
20
21struct hotplug_slot;
22
23struct bus_info {
24};
25
26struct slot {
27 int a;
28 int b;
29 struct hotplug_slot * hotplug_slot;
30 struct bus_info *bus_on;
31};
32
33struct hotplug_slot {
34 struct slot *private;
35 int b;
36};
37
38
39
40
41
42
43struct slot *tmp_slot;
44int used_tmp_slot = 0;
45int freed_tmp_slot = 1;
46
47extern void * kzalloc(int, int);
48
49void kfree(void *p) {
50 if(p!=0 && p==tmp_slot)
51 freed_tmp_slot = 1;
52}
53
54extern void *__VERIFIER_nondet_pointer(void);
55
56struct bus_info *ibmphp_find_same_bus_num() {
57 return __VERIFIER_nondet_pointer();
58}
59
60extern int __VERIFIER_nondet_int(void);
61
62int fillslotinfo(struct hotplug_slot *p) {
63 (void) p;
64 return __VERIFIER_nondet_int();
65}
66
67int ibmphp_init_devno(struct slot **pp) {
68 (void) pp;
69 return __VERIFIER_nondet_int();
70}
71
72int ebda_rsrc_controller() {
73 struct hotplug_slot *hp_slot_ptr;
74
75 struct bus_info *bus_info_ptr1;
76 int rc;
77
78 hp_slot_ptr = kzalloc(sizeof(*hp_slot_ptr), 1);
79 if(!hp_slot_ptr) {
80 rc = -2;
81 goto error_no_hp_slot;
82 }
83 hp_slot_ptr->b = 5;
84
85 tmp_slot = kzalloc(sizeof(*tmp_slot), 1);
86
87 if(!tmp_slot) {
88 rc = -2;
89 goto error_no_slot;
90 }
91
92 used_tmp_slot = 0;
93 freed_tmp_slot = 0;
94
95 tmp_slot->a = 2;
96 tmp_slot->b = 3;
97
98 bus_info_ptr1 = ibmphp_find_same_bus_num();
99 if(!bus_info_ptr1) {
100 rc = -3;
101
102
103 kfree(tmp_slot);
104 freed_tmp_slot = 1;
105
106 goto error;
107 }
108 tmp_slot->bus_on = bus_info_ptr1;
109 bus_info_ptr1 = 0;
110
111 tmp_slot->hotplug_slot = hp_slot_ptr;
112
113 hp_slot_ptr->private = tmp_slot;
114 used_tmp_slot = 1;
115
116 rc = fillslotinfo(hp_slot_ptr);
117 if(rc)
118 goto error;
119
120 rc = ibmphp_init_devno((struct slot **) &hp_slot_ptr->private);
121 if(rc)
122 goto error;
123
124 return 0;
125
126error:
127 kfree(hp_slot_ptr->private);
128error_no_slot:
129
130error_no_hp_slot:
131
132 return rc;
133}
134
135void main() {
136 ebda_rsrc_controller();
137 if(!used_tmp_slot)
138 ((freed_tmp_slot) ? (0) : __blast_assert ());
139}