21621#line 7476
21622 mos7840_interrupt_callback(var_group5);
21623 }
21624#line 7497
21625 goto switch_break;
21626 switch_default:
21627#line 7498
21628 goto switch_break;
21629 } else {
21630 switch_break: ;
21631 }
21632 }
21633 }
21634 }
21635 while_break: ;
21636 }
21637 ldv_module_exit:
21638 {
21639#line 7507
21640 ldv_check_final_state();
21641 }
21642#line 7510
21643 return;
21644}
21645}
21646#line 5 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/7545/dscv_tempdir/dscv/ri/32_1/kernel-rules/files/engine-blast-assert.h"
21647void ldv_blast_assert(void)
21648{
21649
21650 {
21651 ERROR:
21652#line 6
21653 goto ERROR;
21654}
21655}
21656#line 6 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/7545/dscv_tempdir/dscv/ri/32_1/kernel-rules/files/engine-blast.h"
21657extern int __VERIFIER_nondet_int(void) ;
21658#line 19 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/7545/dscv_tempdir/dscv/ri/32_1/kernel-rules/files/model0032.c"
21659int ldv_mutex = 1;
21660#line 22 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/7545/dscv_tempdir/dscv/ri/32_1/kernel-rules/files/model0032.c"
21661int __attribute__((__warn_unused_result__)) mutex_lock_interruptible(struct mutex *lock )