5833#line 368
5834 goto switch_break;
5835 } else {
5836 switch_break: ;
5837 }
5838 }
5839 }
5840 while_break___0: ;
5841 }
5842
5843 while_break: ;
5844 ldv_module_exit:
5845 {
5846#line 386
5847 kbtab_exit();
5848 }
5849 ldv_final:
5850 {
5851#line 389
5852 ldv_check_final_state();
5853 }
5854#line 392
5855 return;
5856}
5857}
5858#line 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"
5859void ldv_blast_assert(void)
5860{
5861
5862 {
5863 ERROR:
5864#line 6
5865 goto ERROR;
5866}
5867}
5868#line 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"
5869extern void *ldv_undefined_pointer(void) ;
5870#line 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"
5871void ldv_assume_stop(void) __attribute__((__ldv_model_inline__)) ;
5872#line 22
5873void ldv_assume_stop(void) __attribute__((__ldv_model_inline__)) ;