8571 switch_default:
8572# 1373 "/anthill/stuff/tacas-comp/work/current--X--drivers/media/video/msp3400.ko--X--bulklinux-3.0.1--X--68_1/linux-3.0.1/csd_deg_dscv/22/dscv_tempdir/dscv/ri/68_1/drivers/media/video/msp3400-driver.c.common.c"
8573 goto switch_break;
8574 } else {
8575 switch_break: ;
8576 }
8577 }
8578 }
8579 while_break___0: ;
8580 }
8581 while_break: ;
8582 ldv_module_exit:
8583 {
8584# 1389 "/anthill/stuff/tacas-comp/work/current--X--drivers/media/video/msp3400.ko--X--bulklinux-3.0.1--X--68_1/linux-3.0.1/csd_deg_dscv/22/dscv_tempdir/dscv/ri/68_1/drivers/media/video/msp3400-driver.c.common.c"
8585 exit_msp();
8586 }
8587 ldv_final:
8588 {
8589# 1392 "/anthill/stuff/tacas-comp/work/current--X--drivers/media/video/msp3400.ko--X--bulklinux-3.0.1--X--68_1/linux-3.0.1/csd_deg_dscv/22/dscv_tempdir/dscv/ri/68_1/drivers/media/video/msp3400-driver.c.common.c"
8590 ldv_check_final_state();
8591 }
8592# 1395 "/anthill/stuff/tacas-comp/work/current--X--drivers/media/video/msp3400.ko--X--bulklinux-3.0.1--X--68_1/linux-3.0.1/csd_deg_dscv/22/dscv_tempdir/dscv/ri/68_1/drivers/media/video/msp3400-driver.c.common.c"
8593 return;
8594}
8595}
8596# 5 "/anthill/stuff/tacas-comp/work/current--X--drivers/media/video/msp3400.ko--X--bulklinux-3.0.1--X--68_1/linux-3.0.1/csd_deg_dscv/22/dscv_tempdir/dscv/ri/68_1/kernel-rules/files/engine-blast-assert.h"
8597void ldv_blast_assert(void)
8598{
8599
8600 {
8601 ERROR:
8602# 6 "/anthill/stuff/tacas-comp/work/current--X--drivers/media/video/msp3400.ko--X--bulklinux-3.0.1--X--68_1/linux-3.0.1/csd_deg_dscv/22/dscv_tempdir/dscv/ri/68_1/kernel-rules/files/engine-blast-assert.h"
8603 goto ERROR;
8604}
8605}
8606# 7 "/anthill/stuff/tacas-comp/work/current--X--drivers/media/video/msp3400.ko--X--bulklinux-3.0.1--X--68_1/linux-3.0.1/csd_deg_dscv/22/dscv_tempdir/dscv/ri/68_1/kernel-rules/files/engine-blast.h"
8607extern void *ldv_undefined_pointer(void) ;
8608# 1332 "include/linux/usb.h"
8609struct urb *usb_alloc_urb(int iso_packets , gfp_t mem_flags ) __attribute__((__ldv_model__)) ;
8610# 1333 "include/linux/usb.h"
8611void usb_free_urb(struct urb *urb ) __attribute__((__ldv_model__)) ;