6517 goto ldv_27967;
6518 } else
6519#line 609
6520 if (ldv_s_ir_device_usb_serial_driver != 0) {
6521#line 611
6522 goto ldv_27967;
6523 } else {
6524#line 613
6525 goto ldv_27969;
6526 }
6527 ldv_27969: ;
6528 ldv_module_exit:
6529 {
6530#line 734
6531 ir_exit();
6532 }
6533 ldv_final:
6534 {
6535#line 737
6536 ldv_check_final_state();
6537 }
6538#line 740
6539 return;
6540}
6541}
6542#line 5 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--43_1a--X--cpachecker/linux-3.4/csd_deg_dscv/1810/dscv_tempdir/dscv/ri/43_1a/kernel-rules/files/engine-blast-assert.h"
6543void ldv_blast_assert(void)
6544{
6545
6546 {
6547 ERROR: ;
6548#line 6
6549 goto ERROR;
6550}
6551}
6552#line 6 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--43_1a--X--cpachecker/linux-3.4/csd_deg_dscv/1810/dscv_tempdir/dscv/ri/43_1a/kernel-rules/files/engine-blast.h"
6553extern int __VERIFIER_nondet_int(void) ;
6554#line 761 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--43_1a--X--cpachecker/linux-3.4/csd_deg_dscv/1810/dscv_tempdir/dscv/ri/43_1a/drivers/usb/serial/ir-usb.c.p"
6555int ldv_spin = 0;
6556#line 765 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--43_1a--X--cpachecker/linux-3.4/csd_deg_dscv/1810/dscv_tempdir/dscv/ri/43_1a/drivers/usb/serial/ir-usb.c.p"
6557void ldv_check_alloc_flags(gfp_t flags )