1813#line 273
1814 goto ldv_15778;
1815 } else
1816#line 271
1817 if (ldv_s_w1_gpio_driver_platform_driver != 0) {
1818#line 273
1819 goto ldv_15778;
1820 } else {
1821#line 275
1822 goto ldv_15780;
1823 }
1824 ldv_15780: ;
1825 {
1826#line 343
1827 w1_gpio_exit();
1828 }
1829 ldv_final:
1830 {
1831#line 346
1832 ldv_check_final_state();
1833 }
1834#line 349
1835 return;
1836}
1837}
1838#line 5 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--43_1a--X--cpachecker/linux-3.4/csd_deg_dscv/4896/dscv_tempdir/dscv/ri/43_1a/kernel-rules/files/engine-blast-assert.h"
1839void ldv_blast_assert(void)
1840{
1841
1842 {
1843 ERROR: ;
1844#line 6
1845 goto ERROR;
1846}
1847}
1848#line 6 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--43_1a--X--cpachecker/linux-3.4/csd_deg_dscv/4896/dscv_tempdir/dscv/ri/43_1a/kernel-rules/files/engine-blast.h"
1849extern int __VERIFIER_nondet_int(void) ;
1850#line 370 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--43_1a--X--cpachecker/linux-3.4/csd_deg_dscv/4896/dscv_tempdir/dscv/ri/43_1a/drivers/w1/masters/w1-gpio.c.p"
1851int ldv_spin = 0;
1852#line 374 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--43_1a--X--cpachecker/linux-3.4/csd_deg_dscv/4896/dscv_tempdir/dscv/ri/43_1a/drivers/w1/masters/w1-gpio.c.p"
1853void ldv_check_alloc_flags(gfp_t flags )