13271 switch_default:
13272# 1977 "/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/drivers/media/dvb/ttusb-dec/ttusb_dec.c.common.c"
13273 goto switch_break;
13274 } else {
13275 switch_break: ;
13276 }
13277 }
13278 }
13279 while_break___0: ;
13280 }
13281 while_break: ;
13282 ldv_module_exit:
13283 {
13284# 2004 "/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/drivers/media/dvb/ttusb-dec/ttusb_dec.c.common.c"
13285 ttusb_dec_exit();
13286 }
13287 ldv_final:
13288 {
13289# 2007 "/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/drivers/media/dvb/ttusb-dec/ttusb_dec.c.common.c"
13290 ldv_check_final_state();
13291 }
13292# 2010 "/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/drivers/media/dvb/ttusb-dec/ttusb_dec.c.common.c"
13293 return;
13294}
13295}
13296# 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"
13297void ldv_blast_assert(void)
13298{
13299
13300 {
13301 ERROR:
13302# 6 "/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"
13303 goto ERROR;
13304}
13305}
13306# 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"
13307extern void *ldv_undefined_pointer(void) ;
13308# 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"
13309void ldv_assume_stop(void) __attribute__((__ldv_model_inline__)) ;
13310# 22 "/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"
13311void ldv_assume_stop(void) __attribute__((__ldv_model_inline__)) ;