6942 goto ldv_40320;
6943 } else
6944#line 350
6945 if (ldv_s_orinoco_tmd_driver_pci_driver != 0) {
6946#line 352
6947 goto ldv_40320;
6948 } else {
6949#line 354
6950 goto ldv_40322;
6951 }
6952 ldv_40322: ;
6953 ldv_module_exit:
6954 {
6955#line 399
6956 orinoco_tmd_exit();
6957 }
6958 ldv_final:
6959 {
6960#line 402
6961 ldv_check_final_state();
6962 }
6963#line 405
6964 return;
6965}
6966}
6967#line 5 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--43_1a--X--cpachecker/linux-3.4/csd_deg_dscv/13882/dscv_tempdir/dscv/ri/43_1a/kernel-rules/files/engine-blast-assert.h"
6968void ldv_blast_assert(void)
6969{
6970
6971 {
6972 ERROR: ;
6973#line 6
6974 goto ERROR;
6975}
6976}
6977#line 6 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--43_1a--X--cpachecker/linux-3.4/csd_deg_dscv/13882/dscv_tempdir/dscv/ri/43_1a/kernel-rules/files/engine-blast.h"
6978extern int __VERIFIER_nondet_int(void) ;
6979#line 426 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--43_1a--X--cpachecker/linux-3.4/csd_deg_dscv/13882/dscv_tempdir/dscv/ri/43_1a/drivers/net/wireless/orinoco/orinoco_tmd.c.p"
6980int ldv_spin = 0;
6981#line 430 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--43_1a--X--cpachecker/linux-3.4/csd_deg_dscv/13882/dscv_tempdir/dscv/ri/43_1a/drivers/net/wireless/orinoco/orinoco_tmd.c.p"
6982void ldv_check_alloc_flags(gfp_t flags )