17520 switch_default:
17521# 7622 "/anthill/stuff/tacas-comp/work/current--X--drivers/scsi/dc395x.ko--X--bulklinux-3.0.1--X--68_1/linux-3.0.1/csd_deg_dscv/11/dscv_tempdir/dscv/ri/68_1/drivers/scsi/dc395x.c.common.c"
17522 goto switch_break;
17523 } else {
17524 switch_break: ;
17525 }
17526 }
17527 }
17528 while_break___0: ;
17529 }
17530 while_break: ;
17531 ldv_module_exit:
17532 {
17533# 7747 "/anthill/stuff/tacas-comp/work/current--X--drivers/scsi/dc395x.ko--X--bulklinux-3.0.1--X--68_1/linux-3.0.1/csd_deg_dscv/11/dscv_tempdir/dscv/ri/68_1/drivers/scsi/dc395x.c.common.c"
17534 dc395x_module_exit();
17535 }
17536 ldv_final:
17537 {
17538# 7750 "/anthill/stuff/tacas-comp/work/current--X--drivers/scsi/dc395x.ko--X--bulklinux-3.0.1--X--68_1/linux-3.0.1/csd_deg_dscv/11/dscv_tempdir/dscv/ri/68_1/drivers/scsi/dc395x.c.common.c"
17539 ldv_check_final_state();
17540 }
17541# 7753 "/anthill/stuff/tacas-comp/work/current--X--drivers/scsi/dc395x.ko--X--bulklinux-3.0.1--X--68_1/linux-3.0.1/csd_deg_dscv/11/dscv_tempdir/dscv/ri/68_1/drivers/scsi/dc395x.c.common.c"
17542 return;
17543}
17544}
17545# 5 "/anthill/stuff/tacas-comp/work/current--X--drivers/scsi/dc395x.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"
17546void ldv_blast_assert(void)
17547{
17548
17549 {
17550 ERROR:
17551# 6 "/anthill/stuff/tacas-comp/work/current--X--drivers/scsi/dc395x.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"
17552 goto ERROR;
17553}
17554}
17555# 7 "/anthill/stuff/tacas-comp/work/current--X--drivers/scsi/dc395x.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"
17556extern void *ldv_undefined_pointer(void) ;
17557# 1332 "include/linux/usb.h"
17558struct urb *usb_alloc_urb(int iso_packets , gfp_t mem_flags ) __attribute__((__ldv_model__)) ;
17559# 1333 "include/linux/usb.h"
17560void usb_free_urb(struct urb *urb ) __attribute__((__ldv_model__)) ;