4975 switch_default:
4976#line 730
4977 goto switch_break;
4978 } else {
4979 switch_break: ;
4980 }
4981 }
4982 }
4983 }
4984 while_break: ;
4985 }
4986 ldv_module_exit:
4987 {
4988#line 750
4989 tifm_exit();
4990 }
4991 ldv_final:
4992 {
4993#line 753
4994 ldv_check_final_state();
4995 }
4996#line 756
4997 return;
4998}
4999}
5000#line 5 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/4897/dscv_tempdir/dscv/ri/32_1/kernel-rules/files/engine-blast-assert.h"
5001void ldv_blast_assert(void)
5002{
5003
5004 {
5005 ERROR:
5006#line 6
5007 goto ERROR;
5008}
5009}
5010#line 6 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/4897/dscv_tempdir/dscv/ri/32_1/kernel-rules/files/engine-blast.h"
5011extern int __VERIFIER_nondet_int(void) ;
5012#line 19 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/4897/dscv_tempdir/dscv/ri/32_1/kernel-rules/files/model0032.c"
5013int ldv_mutex = 1;
5014#line 22 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/4897/dscv_tempdir/dscv/ri/32_1/kernel-rules/files/model0032.c"
5015int __attribute__((__warn_unused_result__)) mutex_lock_interruptible(struct mutex *lock )