4348 goto ldv_26533;
4349 } else
4350#line 249
4351 if (ldv_s_ucb1400_core_driver_device_driver != 0) {
4352#line 251
4353 goto ldv_26533;
4354 } else {
4355#line 253
4356 goto ldv_26535;
4357 }
4358 ldv_26535: ;
4359 ldv_module_exit:
4360 {
4361#line 302
4362 ucb1400_core_exit();
4363 }
4364 ldv_final:
4365 {
4366#line 305
4367 ldv_check_final_state();
4368 }
4369#line 308
4370 return;
4371}
4372}
4373#line 5 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--43_1a--X--cpachecker/linux-3.4/csd_deg_dscv/5008/dscv_tempdir/dscv/ri/43_1a/kernel-rules/files/engine-blast-assert.h"
4374void ldv_blast_assert(void)
4375{
4376
4377 {
4378 ERROR: ;
4379#line 6
4380 goto ERROR;
4381}
4382}
4383#line 6 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--43_1a--X--cpachecker/linux-3.4/csd_deg_dscv/5008/dscv_tempdir/dscv/ri/43_1a/kernel-rules/files/engine-blast.h"
4384extern int __VERIFIER_nondet_int(void) ;
4385#line 329 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--43_1a--X--cpachecker/linux-3.4/csd_deg_dscv/5008/dscv_tempdir/dscv/ri/43_1a/drivers/mfd/ucb1400_core.c.p"
4386int ldv_spin = 0;
4387#line 333 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--43_1a--X--cpachecker/linux-3.4/csd_deg_dscv/5008/dscv_tempdir/dscv/ri/43_1a/drivers/mfd/ucb1400_core.c.p"
4388void ldv_check_alloc_flags(gfp_t flags )