6241 goto ldv_37718;
6242 } else
6243#line 419
6244 if (ldv_s_ma600_dongle_driver != 0) {
6245#line 421
6246 goto ldv_37718;
6247 } else {
6248#line 423
6249 goto ldv_37720;
6250 }
6251 ldv_37720: ;
6252 ldv_module_exit:
6253 {
6254#line 559
6255 ma600_sir_cleanup();
6256 }
6257 ldv_final:
6258 {
6259#line 566
6260 ldv_check_final_state();
6261 }
6262#line 569
6263 return;
6264}
6265}
6266#line 5 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--43_1a--X--cpachecker/linux-3.4/csd_deg_dscv/12688/dscv_tempdir/dscv/ri/43_1a/kernel-rules/files/engine-blast-assert.h"
6267void ldv_blast_assert(void)
6268{
6269
6270 {
6271 ERROR: ;
6272#line 6
6273 goto ERROR;
6274}
6275}
6276#line 6 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--43_1a--X--cpachecker/linux-3.4/csd_deg_dscv/12688/dscv_tempdir/dscv/ri/43_1a/kernel-rules/files/engine-blast.h"
6277extern int __VERIFIER_nondet_int(void) ;
6278#line 590 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--43_1a--X--cpachecker/linux-3.4/csd_deg_dscv/12688/dscv_tempdir/dscv/ri/43_1a/drivers/net/irda/ma600-sir.c.p"
6279int ldv_spin = 0;
6280#line 594 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--43_1a--X--cpachecker/linux-3.4/csd_deg_dscv/12688/dscv_tempdir/dscv/ri/43_1a/drivers/net/irda/ma600-sir.c.p"
6281void ldv_check_alloc_flags(gfp_t flags )