extern void __VERIFIER_error() __attribute__ ((__noreturn__));


void __blast_assert()
{
 ERROR: __VERIFIER_error();
}









struct hotplug_slot;

struct bus_info {
};

struct slot {
 int a;
 int b;
 struct hotplug_slot * hotplug_slot;
 struct bus_info *bus_on;
};

struct hotplug_slot {
 struct slot *private;
 int b;
};






struct slot *tmp_slot;
int used_tmp_slot = 0;
int freed_tmp_slot = 1;

extern void * kzalloc(int, int);

void kfree(void *p) {
 if(p!=0 && p==tmp_slot)
  freed_tmp_slot = 1;
}

extern void *__VERIFIER_nondet_pointer(void);

struct bus_info *ibmphp_find_same_bus_num() {
 return __VERIFIER_nondet_pointer();
}

extern int __VERIFIER_nondet_int(void);

int fillslotinfo(struct hotplug_slot *p) {
 (void) p;
 return __VERIFIER_nondet_int();
}

int ibmphp_init_devno(struct slot **pp) {
 (void) pp;
 return __VERIFIER_nondet_int();
}

int ebda_rsrc_controller() {
 struct hotplug_slot *hp_slot_ptr;

 struct bus_info *bus_info_ptr1;
 int rc;

 hp_slot_ptr = kzalloc(sizeof(*hp_slot_ptr), 1);
 if(!hp_slot_ptr) {
  rc = -2;
  goto error_no_hp_slot;
 }
 hp_slot_ptr->b = 5;

 tmp_slot = kzalloc(sizeof(*tmp_slot), 1);

 if(!tmp_slot) {
  rc = -2;
  goto error_no_slot;
 }

 used_tmp_slot = 0;
 freed_tmp_slot = 0;

 tmp_slot->a = 2;
 tmp_slot->b = 3;

 bus_info_ptr1 = ibmphp_find_same_bus_num();
 if(!bus_info_ptr1) {
  rc = -3;


  kfree(tmp_slot);
  freed_tmp_slot = 1;

  goto error;
 }
 tmp_slot->bus_on = bus_info_ptr1;
 bus_info_ptr1 = 0;

 tmp_slot->hotplug_slot = hp_slot_ptr;

 hp_slot_ptr->private = tmp_slot;
 used_tmp_slot = 1;

 rc = fillslotinfo(hp_slot_ptr);
 if(rc)
  goto error;

 rc = ibmphp_init_devno((struct slot **) &hp_slot_ptr->private);
 if(rc)
  goto error;

 return 0;

error:
 kfree(hp_slot_ptr->private);
error_no_slot:

error_no_hp_slot:

 return rc;
}

int main() {
 ebda_rsrc_controller();
 if(!used_tmp_slot)
  ((freed_tmp_slot) ? (0) : __blast_assert ());
}