10394#line 1373
10395 goto switch_break;
10396 } else {
10397 switch_break: ;
10398 }
10399 }
10400 }
10401 while_break___0: ;
10402 }
10403
10404 while_break: ;
10405 ldv_module_exit:
10406 {
10407#line 1389
10408 exit_msp();
10409 }
10410 ldv_final:
10411 {
10412#line 1392
10413 ldv_check_final_state();
10414 }
10415#line 1395
10416 return;
10417}
10418}
10419#line 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"
10420void ldv_blast_assert(void)
10421{
10422
10423 {
10424 ERROR:
10425#line 6
10426 goto ERROR;
10427}
10428}
10429#line 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"
10430extern void *ldv_undefined_pointer(void) ;
10431#line 1332 "include/linux/usb.h"
10432struct urb *usb_alloc_urb(int iso_packets , gfp_t mem_flags ) __attribute__((__ldv_model__)) ;
10433#line 1333
10434void usb_free_urb(struct urb *urb ) __attribute__((__ldv_model__)) ;