5790 switch_default:
5791#line 403
5792 goto switch_break;
5793 } else {
5794 switch_break: ;
5795 }
5796 }
5797 }
5798 }
5799 while_break: ;
5800 }
5801 ldv_module_exit:
5802 {
5803#line 422
5804 marvell_exit();
5805 }
5806 ldv_final:
5807 {
5808#line 425
5809 ldv_check_final_state();
5810 }
5811#line 428
5812 return;
5813}
5814}
5815#line 5 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/12721/dscv_tempdir/dscv/ri/32_1/kernel-rules/files/engine-blast-assert.h"
5816void ldv_blast_assert(void)
5817{
5818
5819 {
5820 ERROR:
5821#line 6
5822 goto ERROR;
5823}
5824}
5825#line 6 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/12721/dscv_tempdir/dscv/ri/32_1/kernel-rules/files/engine-blast.h"
5826extern int __VERIFIER_nondet_int(void) ;
5827#line 19 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/12721/dscv_tempdir/dscv/ri/32_1/kernel-rules/files/model0032.c"
5828int ldv_mutex = 1;
5829#line 22 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/12721/dscv_tempdir/dscv/ri/32_1/kernel-rules/files/model0032.c"
5830int __attribute__((__warn_unused_result__)) mutex_lock_interruptible(struct mutex *lock )