4639 switch_default:
4640#line 416
4641 goto switch_break;
4642 } else {
4643 switch_break: ;
4644 }
4645 }
4646 }
4647 }
4648 while_break: ;
4649 }
4650 ldv_module_exit:
4651 {
4652#line 440
4653 vr_nor_mtd_exit();
4654 }
4655 ldv_final:
4656 {
4657#line 443
4658 ldv_check_final_state();
4659 }
4660#line 446
4661 return;
4662}
4663}
4664#line 5 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/5442/dscv_tempdir/dscv/ri/32_1/kernel-rules/files/engine-blast-assert.h"
4665void ldv_blast_assert(void)
4666{
4667
4668 {
4669 ERROR:
4670#line 6
4671 goto ERROR;
4672}
4673}
4674#line 6 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/5442/dscv_tempdir/dscv/ri/32_1/kernel-rules/files/engine-blast.h"
4675extern int __VERIFIER_nondet_int(void) ;
4676#line 19 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/5442/dscv_tempdir/dscv/ri/32_1/kernel-rules/files/model0032.c"
4677int ldv_mutex = 1;
4678#line 22 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/5442/dscv_tempdir/dscv/ri/32_1/kernel-rules/files/model0032.c"
4679int __attribute__((__warn_unused_result__)) mutex_lock_interruptible(struct mutex *lock )