9413#line 1655
9414 goto switch_break;
9415 } else {
9416 switch_break: ;
9417 }
9418 }
9419 }
9420 while_break___0: ;
9421 }
9422
9423 while_break: ;
9424 ldv_module_exit:
9425 {
9426#line 1689
9427 iowarrior_exit();
9428 }
9429 ldv_final:
9430 {
9431#line 1692
9432 ldv_check_final_state();
9433 }
9434#line 1695
9435 return;
9436}
9437}
9438#line 5 "/anthill/stuff/tacas-comp/work/current--X--drivers/usb/misc/iowarrior.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"
9439void ldv_blast_assert(void)
9440{
9441
9442 {
9443 ERROR:
9444#line 6
9445 goto ERROR;
9446}
9447}
9448#line 7 "/anthill/stuff/tacas-comp/work/current--X--drivers/usb/misc/iowarrior.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"
9449extern void *ldv_undefined_pointer(void) ;
9450#line 10 "/anthill/stuff/tacas-comp/work/current--X--drivers/usb/misc/iowarrior.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/model0068.c"
9451void ldv_assume_stop(void) __attribute__((__ldv_model_inline__)) ;
9452#line 22
9453void ldv_assume_stop(void) __attribute__((__ldv_model_inline__)) ;