6153#line 413
6154 goto switch_break;
6155 } else {
6156 switch_break: ;
6157 }
6158 }
6159 }
6160 while_break___0: ;
6161 }
6162
6163 while_break: ;
6164 ldv_module_exit:
6165 {
6166#line 432
6167 usb_mouse_exit();
6168 }
6169 ldv_final:
6170 {
6171#line 435
6172 ldv_check_final_state();
6173 }
6174#line 438
6175 return;
6176}
6177}
6178#line 5 "/anthill/stuff/tacas-comp/work/current--X--drivers/hid/usbhid/usbmouse.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"
6179void ldv_blast_assert(void)
6180{
6181
6182 {
6183 ERROR:
6184#line 6
6185 goto ERROR;
6186}
6187}
6188#line 7 "/anthill/stuff/tacas-comp/work/current--X--drivers/hid/usbhid/usbmouse.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"
6189extern void *ldv_undefined_pointer(void) ;
6190#line 10 "/anthill/stuff/tacas-comp/work/current--X--drivers/hid/usbhid/usbmouse.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"
6191void ldv_assume_stop(void) __attribute__((__ldv_model_inline__)) ;
6192#line 22
6193void ldv_assume_stop(void) __attribute__((__ldv_model_inline__)) ;