5627 } else {
5628
5629 }
5630#line 516
5631 goto switch_break;
5632 switch_default:
5633#line 517
5634 goto switch_break;
5635 } else {
5636 switch_break: ;
5637 }
5638 }
5639 }
5640 }
5641 while_break: ;
5642 }
5643 ldv_module_exit:
5644 {
5645#line 526
5646 ldv_check_final_state();
5647 }
5648#line 529
5649 return;
5650}
5651}
5652#line 5 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/310/dscv_tempdir/dscv/ri/32_1/kernel-rules/files/engine-blast-assert.h"
5653void ldv_blast_assert(void)
5654{
5655
5656 {
5657 ERROR:
5658#line 6
5659 goto ERROR;
5660}
5661}
5662#line 6 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/310/dscv_tempdir/dscv/ri/32_1/kernel-rules/files/engine-blast.h"
5663extern int __VERIFIER_nondet_int(void) ;
5664#line 19 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/310/dscv_tempdir/dscv/ri/32_1/kernel-rules/files/model0032.c"
5665int ldv_mutex = 1;
5666#line 22 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/310/dscv_tempdir/dscv/ri/32_1/kernel-rules/files/model0032.c"
5667int __attribute__((__warn_unused_result__)) mutex_lock_interruptible(struct mutex *lock )