17057#line 1977
17058 goto switch_break;
17059 } else {
17060 switch_break: ;
17061 }
17062 }
17063 }
17064 while_break___0: ;
17065 }
17066
17067 while_break: ;
17068 ldv_module_exit:
17069 {
17070#line 2004
17071 ttusb_dec_exit();
17072 }
17073 ldv_final:
17074 {
17075#line 2007
17076 ldv_check_final_state();
17077 }
17078#line 2010
17079 return;
17080}
17081}
17082#line 5 "/anthill/stuff/tacas-comp/work/current--X--drivers/media/dvb/ttusb-dec/ttusb_dec.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"
17083void ldv_blast_assert(void)
17084{
17085
17086 {
17087 ERROR:
17088#line 6
17089 goto ERROR;
17090}
17091}
17092#line 7 "/anthill/stuff/tacas-comp/work/current--X--drivers/media/dvb/ttusb-dec/ttusb_dec.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"
17093extern void *ldv_undefined_pointer(void) ;
17094#line 10 "/anthill/stuff/tacas-comp/work/current--X--drivers/media/dvb/ttusb-dec/ttusb_dec.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"
17095void ldv_assume_stop(void) __attribute__((__ldv_model_inline__)) ;
17096#line 22
17097void ldv_assume_stop(void) __attribute__((__ldv_model_inline__)) ;