8282 goto ldv_32192;
8283 } else
8284#line 1103
8285 if (ldv_s_i2o_scsi_driver_i2o_driver != 0) {
8286#line 1105
8287 goto ldv_32192;
8288 } else {
8289#line 1107
8290 goto ldv_32194;
8291 }
8292 ldv_32194: ;
8293 ldv_module_exit:
8294 {
8295#line 1441
8296 i2o_scsi_exit();
8297 }
8298 ldv_final:
8299 {
8300#line 1444
8301 ldv_check_final_state();
8302 }
8303#line 1447
8304 return;
8305}
8306}
8307#line 5 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--43_1a--X--cpachecker/linux-3.4/csd_deg_dscv/11980/dscv_tempdir/dscv/ri/43_1a/kernel-rules/files/engine-blast-assert.h"
8308void ldv_blast_assert(void)
8309{
8310
8311 {
8312 ERROR: ;
8313#line 6
8314 goto ERROR;
8315}
8316}
8317#line 6 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--43_1a--X--cpachecker/linux-3.4/csd_deg_dscv/11980/dscv_tempdir/dscv/ri/43_1a/kernel-rules/files/engine-blast.h"
8318extern int __VERIFIER_nondet_int(void) ;
8319#line 1468 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--43_1a--X--cpachecker/linux-3.4/csd_deg_dscv/11980/dscv_tempdir/dscv/ri/43_1a/drivers/message/i2o/i2o_scsi.c.p"
8320int ldv_spin = 0;
8321#line 1472 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--43_1a--X--cpachecker/linux-3.4/csd_deg_dscv/11980/dscv_tempdir/dscv/ri/43_1a/drivers/message/i2o/i2o_scsi.c.p"
8322void ldv_check_alloc_flags(gfp_t flags )