7572#line 811
7573 goto switch_break;
7574 } else {
7575 switch_break: ;
7576 }
7577 }
7578 }
7579 while_break___0: ;
7580 }
7581
7582 while_break: ;
7583 ldv_module_exit:
7584 {
7585#line 840
7586 usb_keyspan_exit();
7587 }
7588 ldv_final:
7589 {
7590#line 843
7591 ldv_check_final_state();
7592 }
7593#line 846
7594 return;
7595}
7596}
7597#line 5 "/anthill/stuff/tacas-comp/work/current--X--drivers/input/misc/keyspan_remote.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"
7598void ldv_blast_assert(void)
7599{
7600
7601 {
7602 ERROR:
7603#line 6
7604 goto ERROR;
7605}
7606}
7607#line 7 "/anthill/stuff/tacas-comp/work/current--X--drivers/input/misc/keyspan_remote.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"
7608extern void *ldv_undefined_pointer(void) ;
7609#line 10 "/anthill/stuff/tacas-comp/work/current--X--drivers/input/misc/keyspan_remote.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"
7610void ldv_assume_stop(void) __attribute__((__ldv_model_inline__)) ;
7611#line 22
7612void ldv_assume_stop(void) __attribute__((__ldv_model_inline__)) ;