13768 switch_default:
13769#line 4023
13770 goto switch_break;
13771 } else {
13772 switch_break: ;
13773 }
13774 }
13775 }
13776 }
13777 while_break: ;
13778 }
13779 ldv_module_exit:
13780 {
13781#line 4064
13782 hsu_pci_exit();
13783 }
13784 ldv_final:
13785 {
13786#line 4067
13787 ldv_check_final_state();
13788 }
13789#line 4070
13790 return;
13791}
13792}
13793#line 5 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/16491/dscv_tempdir/dscv/ri/32_1/kernel-rules/files/engine-blast-assert.h"
13794void ldv_blast_assert(void)
13795{
13796
13797 {
13798 ERROR:
13799#line 6
13800 goto ERROR;
13801}
13802}
13803#line 6 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/16491/dscv_tempdir/dscv/ri/32_1/kernel-rules/files/engine-blast.h"
13804extern int __VERIFIER_nondet_int(void) ;
13805#line 19 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/16491/dscv_tempdir/dscv/ri/32_1/kernel-rules/files/model0032.c"
13806int ldv_mutex = 1;
13807#line 22 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/16491/dscv_tempdir/dscv/ri/32_1/kernel-rules/files/model0032.c"
13808int __attribute__((__warn_unused_result__)) mutex_lock_interruptible(struct mutex *lock )