1865 goto switch_break;
1866 switch_default:
1867#line 311
1868 goto switch_break;
1869 } else {
1870 switch_break: ;
1871 }
1872 }
1873 }
1874 }
1875 while_break: ;
1876 }
1877 {
1878#line 329
1879 w1_gpio_exit();
1880 }
1881 ldv_final:
1882 {
1883#line 332
1884 ldv_check_final_state();
1885 }
1886#line 335
1887 return;
1888}
1889}
1890#line 5 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/12372/dscv_tempdir/dscv/ri/32_1/kernel-rules/files/engine-blast-assert.h"
1891void ldv_blast_assert(void)
1892{
1893
1894 {
1895 ERROR:
1896#line 6
1897 goto ERROR;
1898}
1899}
1900#line 6 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/12372/dscv_tempdir/dscv/ri/32_1/kernel-rules/files/engine-blast.h"
1901extern int __VERIFIER_nondet_int(void) ;
1902#line 19 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/12372/dscv_tempdir/dscv/ri/32_1/kernel-rules/files/model0032.c"
1903int ldv_mutex = 1;
1904#line 22 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/12372/dscv_tempdir/dscv/ri/32_1/kernel-rules/files/model0032.c"
1905int __attribute__((__warn_unused_result__)) mutex_lock_interruptible(struct mutex *lock )