1818 goto ldv_15872;
1819 } else
1820#line 270
1821 if (ldv_s_tps65912_gpio_driver_platform_driver != 0) {
1822#line 272
1823 goto ldv_15872;
1824 } else {
1825#line 274
1826 goto ldv_15874;
1827 }
1828 ldv_15874: ;
1829 ldv_module_exit:
1830 {
1831#line 371
1832 tps65912_gpio_exit();
1833 }
1834 ldv_final:
1835 {
1836#line 374
1837 ldv_check_final_state();
1838 }
1839#line 377
1840 return;
1841}
1842}
1843#line 5 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--43_1a--X--cpachecker/linux-3.4/csd_deg_dscv/2765/dscv_tempdir/dscv/ri/43_1a/kernel-rules/files/engine-blast-assert.h"
1844void ldv_blast_assert(void)
1845{
1846
1847 {
1848 ERROR: ;
1849#line 6
1850 goto ERROR;
1851}
1852}
1853#line 6 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--43_1a--X--cpachecker/linux-3.4/csd_deg_dscv/2765/dscv_tempdir/dscv/ri/43_1a/kernel-rules/files/engine-blast.h"
1854extern int __VERIFIER_nondet_int(void) ;
1855#line 398 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--43_1a--X--cpachecker/linux-3.4/csd_deg_dscv/2765/dscv_tempdir/dscv/ri/43_1a/drivers/gpio/gpio-tps65912.c.p"
1856int ldv_spin = 0;
1857#line 402 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--43_1a--X--cpachecker/linux-3.4/csd_deg_dscv/2765/dscv_tempdir/dscv/ri/43_1a/drivers/gpio/gpio-tps65912.c.p"
1858void ldv_check_alloc_flags(gfp_t flags )