6447 goto ldv_36763;
6448 } else
6449#line 345
6450 if (ldv_s_airo_driver_pcmcia_driver != 0) {
6451#line 347
6452 goto ldv_36763;
6453 } else {
6454#line 349
6455 goto ldv_36765;
6456 }
6457 ldv_36765: ;
6458 ldv_module_exit:
6459 {
6460#line 445
6461 airo_cs_cleanup();
6462 }
6463 ldv_final:
6464 {
6465#line 448
6466 ldv_check_final_state();
6467 }
6468#line 451
6469 return;
6470}
6471}
6472#line 5 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--43_1a--X--cpachecker/linux-3.4/csd_deg_dscv/15009/dscv_tempdir/dscv/ri/43_1a/kernel-rules/files/engine-blast-assert.h"
6473void ldv_blast_assert(void)
6474{
6475
6476 {
6477 ERROR: ;
6478#line 6
6479 goto ERROR;
6480}
6481}
6482#line 6 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--43_1a--X--cpachecker/linux-3.4/csd_deg_dscv/15009/dscv_tempdir/dscv/ri/43_1a/kernel-rules/files/engine-blast.h"
6483extern int __VERIFIER_nondet_int(void) ;
6484#line 472 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--43_1a--X--cpachecker/linux-3.4/csd_deg_dscv/15009/dscv_tempdir/dscv/ri/43_1a/drivers/net/wireless/airo_cs.c.p"
6485int ldv_spin = 0;
6486#line 476 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--43_1a--X--cpachecker/linux-3.4/csd_deg_dscv/15009/dscv_tempdir/dscv/ri/43_1a/drivers/net/wireless/airo_cs.c.p"
6487void ldv_check_alloc_flags(gfp_t flags )