2172 goto ldv_20481;
2173 } else
2174#line 279
2175 if (ldv_s_i2o_bus_driver_i2o_driver != 0) {
2176#line 281
2177 goto ldv_20481;
2178 } else {
2179#line 283
2180 goto ldv_20483;
2181 }
2182 ldv_20483: ;
2183 ldv_module_exit:
2184 {
2185#line 344
2186 i2o_bus_exit();
2187 }
2188 ldv_final:
2189 {
2190#line 347
2191 ldv_check_final_state();
2192 }
2193#line 350
2194 return;
2195}
2196}
2197#line 5 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--43_1a--X--cpachecker/linux-3.4/csd_deg_dscv/11974/dscv_tempdir/dscv/ri/43_1a/kernel-rules/files/engine-blast-assert.h"
2198void ldv_blast_assert(void)
2199{
2200
2201 {
2202 ERROR: ;
2203#line 6
2204 goto ERROR;
2205}
2206}
2207#line 6 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--43_1a--X--cpachecker/linux-3.4/csd_deg_dscv/11974/dscv_tempdir/dscv/ri/43_1a/kernel-rules/files/engine-blast.h"
2208extern int __VERIFIER_nondet_int(void) ;
2209#line 371 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--43_1a--X--cpachecker/linux-3.4/csd_deg_dscv/11974/dscv_tempdir/dscv/ri/43_1a/drivers/message/i2o/bus-osm.c.p"
2210int ldv_spin = 0;
2211#line 375 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--43_1a--X--cpachecker/linux-3.4/csd_deg_dscv/11974/dscv_tempdir/dscv/ri/43_1a/drivers/message/i2o/bus-osm.c.p"
2212void ldv_check_alloc_flags(gfp_t flags )