8769 switch_default:
8770#line 1402
8771 goto switch_break;
8772 } else {
8773 switch_break: ;
8774 }
8775 }
8776 }
8777 }
8778 while_break: ;
8779 }
8780 ldv_module_exit:
8781 {
8782#line 1427
8783 i2o_scsi_exit();
8784 }
8785 ldv_final:
8786 {
8787#line 1430
8788 ldv_check_final_state();
8789 }
8790#line 1433
8791 return;
8792}
8793}
8794#line 5 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/1078/dscv_tempdir/dscv/ri/32_1/kernel-rules/files/engine-blast-assert.h"
8795void ldv_blast_assert(void)
8796{
8797
8798 {
8799 ERROR:
8800#line 6
8801 goto ERROR;
8802}
8803}
8804#line 6 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/1078/dscv_tempdir/dscv/ri/32_1/kernel-rules/files/engine-blast.h"
8805extern int __VERIFIER_nondet_int(void) ;
8806#line 19 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/1078/dscv_tempdir/dscv/ri/32_1/kernel-rules/files/model0032.c"
8807int ldv_mutex = 1;
8808#line 22 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/1078/dscv_tempdir/dscv/ri/32_1/kernel-rules/files/model0032.c"
8809int __attribute__((__warn_unused_result__)) mutex_lock_interruptible(struct mutex *lock )