6986 goto switch_break;
6987 switch_default:
6988# 1210 "/anthill/stuff/tacas-comp/work/current--X--drivers/misc/c2port/core.ko--X--bulklinux-3.0.1--X--68_1/linux-3.0.1/csd_deg_dscv/11/dscv_tempdir/dscv/ri/68_1/drivers/misc/c2port/core.c.common.c"
6989 goto switch_break;
6990 } else {
6991 switch_break: ;
6992 }
6993 }
6994 }
6995 while_break___0: ;
6996 }
6997 while_break:
6998 {
6999# 1237 "/anthill/stuff/tacas-comp/work/current--X--drivers/misc/c2port/core.ko--X--bulklinux-3.0.1--X--68_1/linux-3.0.1/csd_deg_dscv/11/dscv_tempdir/dscv/ri/68_1/drivers/misc/c2port/core.c.common.c"
7000 c2port_exit();
7001 }
7002 ldv_final:
7003 {
7004# 1240 "/anthill/stuff/tacas-comp/work/current--X--drivers/misc/c2port/core.ko--X--bulklinux-3.0.1--X--68_1/linux-3.0.1/csd_deg_dscv/11/dscv_tempdir/dscv/ri/68_1/drivers/misc/c2port/core.c.common.c"
7005 ldv_check_final_state();
7006 }
7007# 1243 "/anthill/stuff/tacas-comp/work/current--X--drivers/misc/c2port/core.ko--X--bulklinux-3.0.1--X--68_1/linux-3.0.1/csd_deg_dscv/11/dscv_tempdir/dscv/ri/68_1/drivers/misc/c2port/core.c.common.c"
7008 return;
7009}
7010}
7011# 5 "/anthill/stuff/tacas-comp/work/current--X--drivers/misc/c2port/core.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"
7012void ldv_blast_assert(void)
7013{
7014
7015 {
7016 ERROR:
7017# 6 "/anthill/stuff/tacas-comp/work/current--X--drivers/misc/c2port/core.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"
7018 goto ERROR;
7019}
7020}
7021# 7 "/anthill/stuff/tacas-comp/work/current--X--drivers/misc/c2port/core.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"
7022extern void *ldv_undefined_pointer(void) ;
7023# 1332 "include/linux/usb.h"
7024struct urb *usb_alloc_urb(int iso_packets , gfp_t mem_flags ) __attribute__((__ldv_model__)) ;
7025# 1333 "include/linux/usb.h"
7026void usb_free_urb(struct urb *urb ) __attribute__((__ldv_model__)) ;