6830 __cil_tmp15 = dev->bus;
6831#line 711
6832 hcd_buffer_free(__cil_tmp15, size, addr, dma);
6833 }
6834#line 712
6835 return;
6836}
6837}
6838#line 945 "/anthill/stuff/tacas-comp/work/current--X--drivers/usb/core/usbcore.ko--X--bulklinux-3.0.1--X--08_1/linux-3.0.1/csd_deg_dscv/28/dscv_tempdir/dscv/ri/08_1/drivers/usb/core/usb.c.p"
6839int usb_disabled(void)
6840{
6841
6842 {
6843#line 947
6844 return (nousb);
6845}
6846}
6847#line 1109
6848void ldv_check_final_state(void) ;
6849#line 1115
6850extern void ldv_initialize(void) ;
6851#line 1118
6852extern int nondet_int(void) ;
6853#line 1121 "/anthill/stuff/tacas-comp/work/current--X--drivers/usb/core/usbcore.ko--X--bulklinux-3.0.1--X--08_1/linux-3.0.1/csd_deg_dscv/28/dscv_tempdir/dscv/ri/08_1/drivers/usb/core/usb.c.p"
6854int LDV_IN_INTERRUPT ;
6855#line 5 "/anthill/stuff/tacas-comp/work/current--X--drivers/usb/core/usbcore.ko--X--bulklinux-3.0.1--X--08_1/linux-3.0.1/csd_deg_dscv/28/dscv_tempdir/dscv/ri/08_1/kernel-rules/files/engine-blast-assert.h"
6856void ldv_blast_assert(void)
6857{
6858
6859 {
6860 ERROR: ;
6861#line 6
6862 goto ERROR;
6863}
6864}
6865#line 6 "/anthill/stuff/tacas-comp/work/current--X--drivers/usb/core/usbcore.ko--X--bulklinux-3.0.1--X--08_1/linux-3.0.1/csd_deg_dscv/28/dscv_tempdir/dscv/ri/08_1/kernel-rules/files/engine-blast.h"
6866extern int ldv_undefined_int(void) ;
6867#line 2286 "/anthill/stuff/tacas-comp/work/current--X--drivers/usb/core/usbcore.ko--X--bulklinux-3.0.1--X--08_1/linux-3.0.1/csd_deg_dscv/28/dscv_tempdir/dscv/ri/08_1/drivers/usb/core/usb.c.p"
6868int ldv_module_refcounter = 1;
6869#line 2289 "/anthill/stuff/tacas-comp/work/current--X--drivers/usb/core/usbcore.ko--X--bulklinux-3.0.1--X--08_1/linux-3.0.1/csd_deg_dscv/28/dscv_tempdir/dscv/ri/08_1/drivers/usb/core/usb.c.p"
6870void ldv_module_get(struct module *module )