7243 goto ldv_29047;
7244 } else
7245#line 970
7246 if (ldv_s_sdricoh_driver_pcmcia_driver != 0) {
7247#line 972
7248 goto ldv_29047;
7249 } else {
7250#line 974
7251 goto ldv_29049;
7252 }
7253 ldv_29049: ;
7254 ldv_module_exit:
7255 {
7256#line 1389
7257 sdricoh_drv_exit();
7258 }
7259 ldv_final:
7260 {
7261#line 1392
7262 ldv_check_final_state();
7263 }
7264#line 1395
7265 return;
7266}
7267}
7268#line 5 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--43_1a--X--cpachecker/linux-3.4/csd_deg_dscv/17208/dscv_tempdir/dscv/ri/43_1a/kernel-rules/files/engine-blast-assert.h"
7269void ldv_blast_assert(void)
7270{
7271
7272 {
7273 ERROR: ;
7274#line 6
7275 goto ERROR;
7276}
7277}
7278#line 6 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--43_1a--X--cpachecker/linux-3.4/csd_deg_dscv/17208/dscv_tempdir/dscv/ri/43_1a/kernel-rules/files/engine-blast.h"
7279extern int __VERIFIER_nondet_int(void) ;
7280#line 1416 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--43_1a--X--cpachecker/linux-3.4/csd_deg_dscv/17208/dscv_tempdir/dscv/ri/43_1a/drivers/mmc/host/sdricoh_cs.c.p"
7281int ldv_spin = 0;
7282#line 1420 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--43_1a--X--cpachecker/linux-3.4/csd_deg_dscv/17208/dscv_tempdir/dscv/ri/43_1a/drivers/mmc/host/sdricoh_cs.c.p"
7283void ldv_check_alloc_flags(gfp_t flags )