6945 goto ldv_21168;
6946 } else
6947#line 1571
6948 if (ldv_s_wm831x_alive_ldo_driver_platform_driver != 0) {
6949#line 1575
6950 goto ldv_21168;
6951 } else {
6952#line 1577
6953 goto ldv_21170;
6954 }
6955 ldv_21170: ;
6956 ldv_module_exit:
6957 {
6958#line 2590
6959 wm831x_ldo_exit();
6960 }
6961 ldv_final:
6962 {
6963#line 2593
6964 ldv_check_final_state();
6965 }
6966#line 2596
6967 return;
6968}
6969}
6970#line 5 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--43_1a--X--cpachecker/linux-3.4/csd_deg_dscv/12255/dscv_tempdir/dscv/ri/43_1a/kernel-rules/files/engine-blast-assert.h"
6971void ldv_blast_assert(void)
6972{
6973
6974 {
6975 ERROR: ;
6976#line 6
6977 goto ERROR;
6978}
6979}
6980#line 6 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--43_1a--X--cpachecker/linux-3.4/csd_deg_dscv/12255/dscv_tempdir/dscv/ri/43_1a/kernel-rules/files/engine-blast.h"
6981extern int __VERIFIER_nondet_int(void) ;
6982#line 2617 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--43_1a--X--cpachecker/linux-3.4/csd_deg_dscv/12255/dscv_tempdir/dscv/ri/43_1a/drivers/regulator/wm831x-ldo.c.p"
6983int ldv_spin = 0;
6984#line 2621 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--43_1a--X--cpachecker/linux-3.4/csd_deg_dscv/12255/dscv_tempdir/dscv/ri/43_1a/drivers/regulator/wm831x-ldo.c.p"
6985void ldv_check_alloc_flags(gfp_t flags )