3917 goto ldv_23080;
3918 } else
3919#line 337
3920 if (ldv_s_tps6105x_driver_i2c_driver != 0) {
3921#line 339
3922 goto ldv_23080;
3923 } else {
3924#line 341
3925 goto ldv_23082;
3926 }
3927 ldv_23082: ;
3928 ldv_module_exit:
3929 {
3930#line 374
3931 tps6105x_exit();
3932 }
3933 ldv_final:
3934 {
3935#line 377
3936 ldv_check_final_state();
3937 }
3938#line 380
3939 return;
3940}
3941}
3942#line 5 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--43_1a--X--cpachecker/linux-3.4/csd_deg_dscv/5004/dscv_tempdir/dscv/ri/43_1a/kernel-rules/files/engine-blast-assert.h"
3943void ldv_blast_assert(void)
3944{
3945
3946 {
3947 ERROR: ;
3948#line 6
3949 goto ERROR;
3950}
3951}
3952#line 6 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--43_1a--X--cpachecker/linux-3.4/csd_deg_dscv/5004/dscv_tempdir/dscv/ri/43_1a/kernel-rules/files/engine-blast.h"
3953extern int __VERIFIER_nondet_int(void) ;
3954#line 401 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--43_1a--X--cpachecker/linux-3.4/csd_deg_dscv/5004/dscv_tempdir/dscv/ri/43_1a/drivers/mfd/tps6105x.c.p"
3955int ldv_spin = 0;
3956#line 405 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--43_1a--X--cpachecker/linux-3.4/csd_deg_dscv/5004/dscv_tempdir/dscv/ri/43_1a/drivers/mfd/tps6105x.c.p"
3957void ldv_check_alloc_flags(gfp_t flags )