5287 switch_default:
5288# 413 "/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/drivers/hid/usbhid/usbmouse.c.common.c"
5289 goto switch_break;
5290 } else {
5291 switch_break: ;
5292 }
5293 }
5294 }
5295 while_break___0: ;
5296 }
5297 while_break: ;
5298 ldv_module_exit:
5299 {
5300# 432 "/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/drivers/hid/usbhid/usbmouse.c.common.c"
5301 usb_mouse_exit();
5302 }
5303 ldv_final:
5304 {
5305# 435 "/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/drivers/hid/usbhid/usbmouse.c.common.c"
5306 ldv_check_final_state();
5307 }
5308# 438 "/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/drivers/hid/usbhid/usbmouse.c.common.c"
5309 return;
5310}
5311}
5312# 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"
5313void ldv_blast_assert(void)
5314{
5315
5316 {
5317 ERROR:
5318# 6 "/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"
5319 goto ERROR;
5320}
5321}
5322# 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"
5323extern void *ldv_undefined_pointer(void) ;
5324# 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"
5325void ldv_assume_stop(void) __attribute__((__ldv_model_inline__)) ;
5326# 22 "/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"
5327void ldv_assume_stop(void) __attribute__((__ldv_model_inline__)) ;