6832 __cil_tmp15 = dev->bus;
6833#line 711
6834 hcd_buffer_free(__cil_tmp15, size, addr, dma);
6835 }
6836#line 712
6837 return;
6838}
6839}
6840#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"
6841int usb_disabled(void)
6842{
6843
6844 {
6845#line 947
6846 return (nousb);
6847}
6848}
6849#line 1109
6850void ldv_check_final_state(void) ;
6851#line 1115
6852extern void ldv_initialize(void) ;
6853#line 1118
6854extern int nondet_int(void) ;
6855#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"
6856int LDV_IN_INTERRUPT ;
6857#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"
6858void ldv_blast_assert(void)
6859{
6860
6861 {
6862 ERROR: ;
6863#line 6
6864 goto ERROR;
6865}
6866}
6867#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"
6868extern int ldv_undefined_int(void) ;
6869#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"
6870int ldv_module_refcounter = 1;
6871#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"
6872void ldv_module_get(struct module *module )