6687 goto switch_break;
6688 switch_default:
6689#line 9288
6690 goto switch_break;
6691 } else {
6692 switch_break: ;
6693 }
6694 }
6695 }
6696 }
6697 while_break: ;
6698 }
6699 {
6700#line 9407
6701 broadcom_exit();
6702 }
6703 ldv_final:
6704 {
6705#line 9410
6706 ldv_check_final_state();
6707 }
6708#line 9413
6709 return;
6710}
6711}
6712#line 5 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/9657/dscv_tempdir/dscv/ri/32_1/kernel-rules/files/engine-blast-assert.h"
6713void ldv_blast_assert(void)
6714{
6715
6716 {
6717 ERROR:
6718#line 6
6719 goto ERROR;
6720}
6721}
6722#line 6 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/9657/dscv_tempdir/dscv/ri/32_1/kernel-rules/files/engine-blast.h"
6723extern int __VERIFIER_nondet_int(void) ;
6724#line 19 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/9657/dscv_tempdir/dscv/ri/32_1/kernel-rules/files/model0032.c"
6725int ldv_mutex = 1;
6726#line 22 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/9657/dscv_tempdir/dscv/ri/32_1/kernel-rules/files/model0032.c"
6727int __attribute__((__warn_unused_result__)) mutex_lock_interruptible(struct mutex *lock )