6016 goto ldv_37703;
6017 } else
6018#line 256
6019 if (ldv_s_esi_dongle_driver != 0) {
6020#line 258
6021 goto ldv_37703;
6022 } else {
6023#line 260
6024 goto ldv_37705;
6025 }
6026 ldv_37705: ;
6027 ldv_module_exit:
6028 {
6029#line 341
6030 esi_sir_cleanup();
6031 }
6032 ldv_final:
6033 {
6034#line 344
6035 ldv_check_final_state();
6036 }
6037#line 347
6038 return;
6039}
6040}
6041#line 5 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--43_1a--X--cpachecker/linux-3.4/csd_deg_dscv/12680/dscv_tempdir/dscv/ri/43_1a/kernel-rules/files/engine-blast-assert.h"
6042void ldv_blast_assert(void)
6043{
6044
6045 {
6046 ERROR: ;
6047#line 6
6048 goto ERROR;
6049}
6050}
6051#line 6 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--43_1a--X--cpachecker/linux-3.4/csd_deg_dscv/12680/dscv_tempdir/dscv/ri/43_1a/kernel-rules/files/engine-blast.h"
6052extern int __VERIFIER_nondet_int(void) ;
6053#line 368 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--43_1a--X--cpachecker/linux-3.4/csd_deg_dscv/12680/dscv_tempdir/dscv/ri/43_1a/drivers/net/irda/esi-sir.c.p"
6054int ldv_spin = 0;
6055#line 372 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--43_1a--X--cpachecker/linux-3.4/csd_deg_dscv/12680/dscv_tempdir/dscv/ri/43_1a/drivers/net/irda/esi-sir.c.p"
6056void ldv_check_alloc_flags(gfp_t flags )