27918#line 7622
27919 goto switch_break;
27920 } else {
27921 switch_break: ;
27922 }
27923 }
27924 }
27925 while_break___0: ;
27926 }
27927
27928 while_break: ;
27929 ldv_module_exit:
27930 {
27931#line 7747
27932 dc395x_module_exit();
27933 }
27934 ldv_final:
27935 {
27936#line 7750
27937 ldv_check_final_state();
27938 }
27939#line 7753
27940 return;
27941}
27942}
27943#line 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"
27944void ldv_blast_assert(void)
27945{
27946
27947 {
27948 ERROR:
27949#line 6
27950 goto ERROR;
27951}
27952}
27953#line 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"
27954extern void *ldv_undefined_pointer(void) ;
27955#line 1332 "include/linux/usb.h"
27956struct urb *usb_alloc_urb(int iso_packets , gfp_t mem_flags ) __attribute__((__ldv_model__)) ;
27957#line 1333
27958void usb_free_urb(struct urb *urb ) __attribute__((__ldv_model__)) ;