7302#line 748
7303 goto switch_break;
7304 } else {
7305 switch_break: ;
7306 }
7307 }
7308 }
7309 while_break___0: ;
7310 }
7311
7312 while_break: ;
7313 ldv_module_exit:
7314 {
7315#line 764
7316 ir_exit();
7317 }
7318 ldv_final:
7319 {
7320#line 767
7321 ldv_check_final_state();
7322 }
7323#line 770
7324 return;
7325}
7326}
7327#line 5 "/anthill/stuff/tacas-comp/work/current--X--drivers/usb/serial/ir-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"
7328void ldv_blast_assert(void)
7329{
7330
7331 {
7332 ERROR:
7333#line 6
7334 goto ERROR;
7335}
7336}
7337#line 7 "/anthill/stuff/tacas-comp/work/current--X--drivers/usb/serial/ir-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"
7338extern void *ldv_undefined_pointer(void) ;
7339#line 10 "/anthill/stuff/tacas-comp/work/current--X--drivers/usb/serial/ir-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"
7340void ldv_assume_stop(void) __attribute__((__ldv_model_inline__)) ;
7341#line 22
7342void ldv_assume_stop(void) __attribute__((__ldv_model_inline__)) ;