4543 goto ldv_22614;
4544 } else
4545#line 554
4546 if (ldv_s_wm8400_regulator_driver_platform_driver != 0) {
4547#line 556
4548 goto ldv_22614;
4549 } else {
4550#line 558
4551 goto ldv_22616;
4552 }
4553 ldv_22616: ;
4554 ldv_module_exit:
4555 {
4556#line 831
4557 wm8400_regulator_exit();
4558 }
4559 ldv_final:
4560 {
4561#line 834
4562 ldv_check_final_state();
4563 }
4564#line 837
4565 return;
4566}
4567}
4568#line 5 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--43_1a--X--cpachecker/linux-3.4/csd_deg_dscv/12256/dscv_tempdir/dscv/ri/43_1a/kernel-rules/files/engine-blast-assert.h"
4569void ldv_blast_assert(void)
4570{
4571
4572 {
4573 ERROR: ;
4574#line 6
4575 goto ERROR;
4576}
4577}
4578#line 6 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--43_1a--X--cpachecker/linux-3.4/csd_deg_dscv/12256/dscv_tempdir/dscv/ri/43_1a/kernel-rules/files/engine-blast.h"
4579extern int __VERIFIER_nondet_int(void) ;
4580#line 858 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--43_1a--X--cpachecker/linux-3.4/csd_deg_dscv/12256/dscv_tempdir/dscv/ri/43_1a/drivers/regulator/wm8400-regulator.c.p"
4581int ldv_spin = 0;
4582#line 862 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--43_1a--X--cpachecker/linux-3.4/csd_deg_dscv/12256/dscv_tempdir/dscv/ri/43_1a/drivers/regulator/wm8400-regulator.c.p"
4583void ldv_check_alloc_flags(gfp_t flags )