10730#line 1962
10731 goto switch_break;
10732 } else {
10733 switch_break: ;
10734 }
10735 }
10736 }
10737 while_break___0: ;
10738 }
10739
10740 while_break: ;
10741 ldv_module_exit:
10742 {
10743#line 2031
10744 ems_usb_exit();
10745 }
10746 ldv_final:
10747 {
10748#line 2034
10749 ldv_check_final_state();
10750 }
10751#line 2037
10752 return;
10753}
10754}
10755#line 5 "/anthill/stuff/tacas-comp/work/current--X--drivers/net/can/usb/ems_usb.ko--X--bulklinux-3.0.1--X--68_1/linux-3.0.1/csd_deg_dscv/11/dscv_tempdir/dscv/ri/68_1/kernel-rules/files/engine-blast-assert.h"
10756void ldv_blast_assert(void)
10757{
10758
10759 {
10760 ERROR:
10761#line 6
10762 goto ERROR;
10763}
10764}
10765#line 7 "/anthill/stuff/tacas-comp/work/current--X--drivers/net/can/usb/ems_usb.ko--X--bulklinux-3.0.1--X--68_1/linux-3.0.1/csd_deg_dscv/11/dscv_tempdir/dscv/ri/68_1/kernel-rules/files/engine-blast.h"
10766extern void *ldv_undefined_pointer(void) ;
10767#line 10 "/anthill/stuff/tacas-comp/work/current--X--drivers/net/can/usb/ems_usb.ko--X--bulklinux-3.0.1--X--68_1/linux-3.0.1/csd_deg_dscv/11/dscv_tempdir/dscv/ri/68_1/kernel-rules/files/model0068.c"
10768void ldv_assume_stop(void) __attribute__((__ldv_model_inline__)) ;
10769#line 22
10770void ldv_assume_stop(void) __attribute__((__ldv_model_inline__)) ;