8977 } else {
8978
8979 }
8980#line 886
8981 goto switch_break;
8982 switch_default:
8983#line 887
8984 goto switch_break;
8985 } else {
8986 switch_break: ;
8987 }
8988 }
8989 }
8990 }
8991 while_break: ;
8992 }
8993 ldv_module_exit:
8994 {
8995#line 896
8996 ldv_check_final_state();
8997 }
8998#line 899
8999 return;
9000}
9001}
9002#line 5 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/7659/dscv_tempdir/dscv/ri/32_1/kernel-rules/files/engine-blast-assert.h"
9003void ldv_blast_assert(void)
9004{
9005
9006 {
9007 ERROR:
9008#line 6
9009 goto ERROR;
9010}
9011}
9012#line 6 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/7659/dscv_tempdir/dscv/ri/32_1/kernel-rules/files/engine-blast.h"
9013extern int __VERIFIER_nondet_int(void) ;
9014#line 19 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/7659/dscv_tempdir/dscv/ri/32_1/kernel-rules/files/model0032.c"
9015int ldv_mutex = 1;
9016#line 22 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/7659/dscv_tempdir/dscv/ri/32_1/kernel-rules/files/model0032.c"
9017int __attribute__((__warn_unused_result__)) mutex_lock_interruptible(struct mutex *lock )