7194 switch_default:
7195#line 1013
7196 goto switch_break;
7197 } else {
7198 switch_break: ;
7199 }
7200 }
7201 }
7202 }
7203 while_break: ;
7204 }
7205 ldv_module_exit:
7206 {
7207#line 1034
7208 vfb_exit();
7209 }
7210 ldv_final:
7211 {
7212#line 1040
7213 ldv_check_final_state();
7214 }
7215#line 1043
7216 return;
7217}
7218}
7219#line 5 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/17329/dscv_tempdir/dscv/ri/32_1/kernel-rules/files/engine-blast-assert.h"
7220void ldv_blast_assert(void)
7221{
7222
7223 {
7224 ERROR:
7225#line 6
7226 goto ERROR;
7227}
7228}
7229#line 6 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/17329/dscv_tempdir/dscv/ri/32_1/kernel-rules/files/engine-blast.h"
7230extern int __VERIFIER_nondet_int(void) ;
7231#line 19 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/17329/dscv_tempdir/dscv/ri/32_1/kernel-rules/files/model0032.c"
7232int ldv_mutex = 1;
7233#line 22 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/17329/dscv_tempdir/dscv/ri/32_1/kernel-rules/files/model0032.c"
7234int __attribute__((__warn_unused_result__)) mutex_lock_interruptible(struct mutex *lock )