3419 switch_default:
3420#line 467
3421 goto switch_break;
3422 } else {
3423 switch_break: ;
3424 }
3425 }
3426 }
3427 }
3428 while_break: ;
3429 }
3430 ldv_module_exit:
3431 {
3432#line 494
3433 mtouch_exit();
3434 }
3435 ldv_final:
3436 {
3437#line 497
3438 ldv_check_final_state();
3439 }
3440#line 500
3441 return;
3442}
3443}
3444#line 5 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/4184/dscv_tempdir/dscv/ri/32_1/kernel-rules/files/engine-blast-assert.h"
3445void ldv_blast_assert(void)
3446{
3447
3448 {
3449 ERROR:
3450#line 6
3451 goto ERROR;
3452}
3453}
3454#line 6 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/4184/dscv_tempdir/dscv/ri/32_1/kernel-rules/files/engine-blast.h"
3455extern int __VERIFIER_nondet_int(void) ;
3456#line 19 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/4184/dscv_tempdir/dscv/ri/32_1/kernel-rules/files/model0032.c"
3457int ldv_mutex = 1;
3458#line 22 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/4184/dscv_tempdir/dscv/ri/32_1/kernel-rules/files/model0032.c"
3459int __attribute__((__warn_unused_result__)) mutex_lock_interruptible(struct mutex *lock )