732 goto switch_break;
733 switch_default:
734#line 387
735 goto switch_break;
736 } else {
737 switch_break: ;
738 }
739 }
740 }
741 }
742 while_break: ;
743 }
744 {
745#line 404
746 duramar2150_c2port_exit();
747 }
748 ldv_final:
749 {
750#line 407
751 ldv_check_final_state();
752 }
753#line 410
754 return;
755}
756}
757#line 5 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/4773/dscv_tempdir/dscv/ri/32_1/kernel-rules/files/engine-blast-assert.h"
758void ldv_blast_assert(void)
759{
760
761 {
762 ERROR:
763#line 6
764 goto ERROR;
765}
766}
767#line 6 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/4773/dscv_tempdir/dscv/ri/32_1/kernel-rules/files/engine-blast.h"
768extern int __VERIFIER_nondet_int(void) ;
769#line 19 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/4773/dscv_tempdir/dscv/ri/32_1/kernel-rules/files/model0032.c"
770int ldv_mutex = 1;
771#line 22 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/4773/dscv_tempdir/dscv/ri/32_1/kernel-rules/files/model0032.c"
772int __attribute__((__warn_unused_result__)) mutex_lock_interruptible(struct mutex *lock )