6305 goto ldv_29267;
6306 } else
6307#line 278
6308 if (ldv_s_ixj_driver_pcmcia_driver != 0) {
6309#line 280
6310 goto ldv_29267;
6311 } else {
6312#line 282
6313 goto ldv_29269;
6314 }
6315 ldv_29269: ;
6316 ldv_module_exit:
6317 {
6318#line 331
6319 ixj_pcmcia_exit();
6320 }
6321 ldv_final:
6322 {
6323#line 334
6324 ldv_check_final_state();
6325 }
6326#line 337
6327 return;
6328}
6329}
6330#line 5 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--43_1a--X--cpachecker/linux-3.4/csd_deg_dscv/5534/dscv_tempdir/dscv/ri/43_1a/kernel-rules/files/engine-blast-assert.h"
6331void ldv_blast_assert(void)
6332{
6333
6334 {
6335 ERROR: ;
6336#line 6
6337 goto ERROR;
6338}
6339}
6340#line 6 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--43_1a--X--cpachecker/linux-3.4/csd_deg_dscv/5534/dscv_tempdir/dscv/ri/43_1a/kernel-rules/files/engine-blast.h"
6341extern int __VERIFIER_nondet_int(void) ;
6342#line 358 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--43_1a--X--cpachecker/linux-3.4/csd_deg_dscv/5534/dscv_tempdir/dscv/ri/43_1a/drivers/staging/telephony/ixj_pcmcia.c.p"
6343int ldv_spin = 0;
6344#line 362 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--43_1a--X--cpachecker/linux-3.4/csd_deg_dscv/5534/dscv_tempdir/dscv/ri/43_1a/drivers/staging/telephony/ixj_pcmcia.c.p"
6345void ldv_check_alloc_flags(gfp_t flags )