4566 goto ldv_23050;
4567 } else
4568#line 539
4569 if (ldv_s_wm8400_i2c_driver_i2c_driver != 0) {
4570#line 541
4571 goto ldv_23050;
4572 } else {
4573#line 543
4574 goto ldv_23052;
4575 }
4576 ldv_23052: ;
4577 ldv_module_exit:
4578 {
4579#line 618
4580 wm8400_module_exit();
4581 }
4582 ldv_final:
4583 {
4584#line 621
4585 ldv_check_final_state();
4586 }
4587#line 624
4588 return;
4589}
4590}
4591#line 5 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--43_1a--X--cpachecker/linux-3.4/csd_deg_dscv/5011/dscv_tempdir/dscv/ri/43_1a/kernel-rules/files/engine-blast-assert.h"
4592void ldv_blast_assert(void)
4593{
4594
4595 {
4596 ERROR: ;
4597#line 6
4598 goto ERROR;
4599}
4600}
4601#line 6 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--43_1a--X--cpachecker/linux-3.4/csd_deg_dscv/5011/dscv_tempdir/dscv/ri/43_1a/kernel-rules/files/engine-blast.h"
4602extern int __VERIFIER_nondet_int(void) ;
4603#line 645 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--43_1a--X--cpachecker/linux-3.4/csd_deg_dscv/5011/dscv_tempdir/dscv/ri/43_1a/drivers/mfd/wm8400-core.c.p"
4604int ldv_spin = 0;
4605#line 649 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--43_1a--X--cpachecker/linux-3.4/csd_deg_dscv/5011/dscv_tempdir/dscv/ri/43_1a/drivers/mfd/wm8400-core.c.p"
4606void ldv_check_alloc_flags(gfp_t flags )