8021 goto ldv_42012;
8022 } else
8023#line 639
8024 if (ldv_s_ath6kl_usb_driver_usb_driver != 0) {
8025#line 641
8026 goto ldv_42012;
8027 } else {
8028#line 643
8029 goto ldv_42014;
8030 }
8031 ldv_42014: ;
8032 ldv_module_exit:
8033 {
8034#line 869
8035 ath6kl_usb_exit();
8036 }
8037 ldv_final:
8038 {
8039#line 872
8040 ldv_check_final_state();
8041 }
8042#line 875
8043 return;
8044}
8045}
8046#line 5 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--43_1a--X--cpachecker/linux-3.4/csd_deg_dscv/14141/dscv_tempdir/dscv/ri/43_1a/kernel-rules/files/engine-blast-assert.h"
8047void ldv_blast_assert(void)
8048{
8049
8050 {
8051 ERROR: ;
8052#line 6
8053 goto ERROR;
8054}
8055}
8056#line 6 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--43_1a--X--cpachecker/linux-3.4/csd_deg_dscv/14141/dscv_tempdir/dscv/ri/43_1a/kernel-rules/files/engine-blast.h"
8057extern int __VERIFIER_nondet_int(void) ;
8058#line 896 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--43_1a--X--cpachecker/linux-3.4/csd_deg_dscv/14141/dscv_tempdir/dscv/ri/43_1a/drivers/net/wireless/ath/ath6kl/usb.c.p"
8059int ldv_spin = 0;
8060#line 900 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--43_1a--X--cpachecker/linux-3.4/csd_deg_dscv/14141/dscv_tempdir/dscv/ri/43_1a/drivers/net/wireless/ath/ath6kl/usb.c.p"
8061void ldv_check_alloc_flags(gfp_t flags )