8517#line 1306
8518 goto switch_break;
8519 } else {
8520 switch_break: ;
8521 }
8522 }
8523 }
8524 while_break___0: ;
8525 }
8526
8527 while_break: ;
8528 ldv_module_exit:
8529 {
8530#line 1329
8531 imon_exit();
8532 }
8533 ldv_final:
8534 {
8535#line 1332
8536 ldv_check_final_state();
8537 }
8538#line 1335
8539 return;
8540}
8541}
8542#line 5 "/anthill/stuff/tacas-comp/work/current--X--drivers/staging/lirc/lirc_imon.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"
8543void ldv_blast_assert(void)
8544{
8545
8546 {
8547 ERROR:
8548#line 6
8549 goto ERROR;
8550}
8551}
8552#line 7 "/anthill/stuff/tacas-comp/work/current--X--drivers/staging/lirc/lirc_imon.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"
8553extern void *ldv_undefined_pointer(void) ;
8554#line 10 "/anthill/stuff/tacas-comp/work/current--X--drivers/staging/lirc/lirc_imon.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"
8555void ldv_assume_stop(void) __attribute__((__ldv_model_inline__)) ;
8556#line 22
8557void ldv_assume_stop(void) __attribute__((__ldv_model_inline__)) ;