4276 goto ldv_21966;
4277 } else
4278#line 555
4279 if (ldv_s_tifm_bus_type_bus_type != 0) {
4280#line 557
4281 goto ldv_21966;
4282 } else {
4283#line 559
4284 goto ldv_21968;
4285 }
4286 ldv_21968: ;
4287 ldv_module_exit:
4288 {
4289#line 764
4290 tifm_exit();
4291 }
4292 ldv_final:
4293 {
4294#line 767
4295 ldv_check_final_state();
4296 }
4297#line 770
4298 return;
4299}
4300}
4301#line 5 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--43_1a--X--cpachecker/linux-3.4/csd_deg_dscv/12648/dscv_tempdir/dscv/ri/43_1a/kernel-rules/files/engine-blast-assert.h"
4302void ldv_blast_assert(void)
4303{
4304
4305 {
4306 ERROR: ;
4307#line 6
4308 goto ERROR;
4309}
4310}
4311#line 6 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--43_1a--X--cpachecker/linux-3.4/csd_deg_dscv/12648/dscv_tempdir/dscv/ri/43_1a/kernel-rules/files/engine-blast.h"
4312extern int __VERIFIER_nondet_int(void) ;
4313#line 791 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--43_1a--X--cpachecker/linux-3.4/csd_deg_dscv/12648/dscv_tempdir/dscv/ri/43_1a/drivers/misc/tifm_core.c.p"
4314int ldv_spin = 0;
4315#line 795 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--43_1a--X--cpachecker/linux-3.4/csd_deg_dscv/12648/dscv_tempdir/dscv/ri/43_1a/drivers/misc/tifm_core.c.p"
4316void ldv_check_alloc_flags(gfp_t flags )