1926 goto ldv_17223;
1927 } else
1928#line 270
1929 if (ldv_s_gpio_switch_driver_platform_driver != 0) {
1930#line 272
1931 goto ldv_17223;
1932 } else {
1933#line 274
1934 goto ldv_17225;
1935 }
1936 ldv_17225: ;
1937 ldv_module_exit:
1938 {
1939#line 323
1940 gpio_switch_exit();
1941 }
1942 ldv_final:
1943 {
1944#line 326
1945 ldv_check_final_state();
1946 }
1947#line 329
1948 return;
1949}
1950}
1951#line 5 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--43_1a--X--cpachecker/linux-3.4/csd_deg_dscv/5575/dscv_tempdir/dscv/ri/43_1a/kernel-rules/files/engine-blast-assert.h"
1952void ldv_blast_assert(void)
1953{
1954
1955 {
1956 ERROR: ;
1957#line 6
1958 goto ERROR;
1959}
1960}
1961#line 6 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--43_1a--X--cpachecker/linux-3.4/csd_deg_dscv/5575/dscv_tempdir/dscv/ri/43_1a/kernel-rules/files/engine-blast.h"
1962extern int __VERIFIER_nondet_int(void) ;
1963#line 350 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--43_1a--X--cpachecker/linux-3.4/csd_deg_dscv/5575/dscv_tempdir/dscv/ri/43_1a/drivers/staging/android/switch/switch_gpio.c.p"
1964int ldv_spin = 0;
1965#line 354 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--43_1a--X--cpachecker/linux-3.4/csd_deg_dscv/5575/dscv_tempdir/dscv/ri/43_1a/drivers/staging/android/switch/switch_gpio.c.p"
1966void ldv_check_alloc_flags(gfp_t flags )