6768 switch_default:
6769#line 626
6770 goto switch_break;
6771 } else {
6772 switch_break: ;
6773 }
6774 }
6775 }
6776 }
6777 while_break: ;
6778 }
6779 ldv_module_exit:
6780 {
6781#line 656
6782 girbil_sir_cleanup();
6783 }
6784 ldv_final:
6785 {
6786#line 665
6787 ldv_check_final_state();
6788 }
6789#line 668
6790 return;
6791}
6792}
6793#line 5 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/9298/dscv_tempdir/dscv/ri/32_1/kernel-rules/files/engine-blast-assert.h"
6794void ldv_blast_assert(void)
6795{
6796
6797 {
6798 ERROR:
6799#line 6
6800 goto ERROR;
6801}
6802}
6803#line 6 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/9298/dscv_tempdir/dscv/ri/32_1/kernel-rules/files/engine-blast.h"
6804extern int __VERIFIER_nondet_int(void) ;
6805#line 19 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/9298/dscv_tempdir/dscv/ri/32_1/kernel-rules/files/model0032.c"
6806int ldv_mutex = 1;
6807#line 22 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/9298/dscv_tempdir/dscv/ri/32_1/kernel-rules/files/model0032.c"
6808int __attribute__((__warn_unused_result__)) mutex_lock_interruptible(struct mutex *lock )