5175 switch_default:
5176# 368 "/anthill/stuff/tacas-comp/work/current--X--drivers/input/tablet/kbtab.ko--X--bulklinux-3.0.1--X--68_1/linux-3.0.1/csd_deg_dscv/11/dscv_tempdir/dscv/ri/68_1/drivers/input/tablet/kbtab.c.common.c"
5177 goto switch_break;
5178 } else {
5179 switch_break: ;
5180 }
5181 }
5182 }
5183 while_break___0: ;
5184 }
5185 while_break: ;
5186 ldv_module_exit:
5187 {
5188# 386 "/anthill/stuff/tacas-comp/work/current--X--drivers/input/tablet/kbtab.ko--X--bulklinux-3.0.1--X--68_1/linux-3.0.1/csd_deg_dscv/11/dscv_tempdir/dscv/ri/68_1/drivers/input/tablet/kbtab.c.common.c"
5189 kbtab_exit();
5190 }
5191 ldv_final:
5192 {
5193# 389 "/anthill/stuff/tacas-comp/work/current--X--drivers/input/tablet/kbtab.ko--X--bulklinux-3.0.1--X--68_1/linux-3.0.1/csd_deg_dscv/11/dscv_tempdir/dscv/ri/68_1/drivers/input/tablet/kbtab.c.common.c"
5194 ldv_check_final_state();
5195 }
5196# 392 "/anthill/stuff/tacas-comp/work/current--X--drivers/input/tablet/kbtab.ko--X--bulklinux-3.0.1--X--68_1/linux-3.0.1/csd_deg_dscv/11/dscv_tempdir/dscv/ri/68_1/drivers/input/tablet/kbtab.c.common.c"
5197 return;
5198}
5199}
5200# 5 "/anthill/stuff/tacas-comp/work/current--X--drivers/input/tablet/kbtab.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"
5201void ldv_blast_assert(void)
5202{
5203
5204 {
5205 ERROR:
5206# 6 "/anthill/stuff/tacas-comp/work/current--X--drivers/input/tablet/kbtab.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"
5207 goto ERROR;
5208}
5209}
5210# 7 "/anthill/stuff/tacas-comp/work/current--X--drivers/input/tablet/kbtab.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"
5211extern void *ldv_undefined_pointer(void) ;
5212# 10 "/anthill/stuff/tacas-comp/work/current--X--drivers/input/tablet/kbtab.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"
5213void ldv_assume_stop(void) __attribute__((__ldv_model_inline__)) ;
5214# 22 "/anthill/stuff/tacas-comp/work/current--X--drivers/input/tablet/kbtab.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"
5215void ldv_assume_stop(void) __attribute__((__ldv_model_inline__)) ;