3435 switch_default:
3436#line 431
3437 goto switch_break;
3438 } else {
3439 switch_break: ;
3440 }
3441 }
3442 }
3443 }
3444 while_break: ;
3445 }
3446 ldv_module_exit:
3447 {
3448#line 455
3449 hampshire_exit();
3450 }
3451 ldv_final:
3452 {
3453#line 458
3454 ldv_check_final_state();
3455 }
3456#line 461
3457 return;
3458}
3459}
3460#line 5 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/4177/dscv_tempdir/dscv/ri/32_1/kernel-rules/files/engine-blast-assert.h"
3461void ldv_blast_assert(void)
3462{
3463
3464 {
3465 ERROR:
3466#line 6
3467 goto ERROR;
3468}
3469}
3470#line 6 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/4177/dscv_tempdir/dscv/ri/32_1/kernel-rules/files/engine-blast.h"
3471extern int __VERIFIER_nondet_int(void) ;
3472#line 19 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/4177/dscv_tempdir/dscv/ri/32_1/kernel-rules/files/model0032.c"
3473int ldv_mutex = 1;
3474#line 22 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/4177/dscv_tempdir/dscv/ri/32_1/kernel-rules/files/model0032.c"
3475int __attribute__((__warn_unused_result__)) mutex_lock_interruptible(struct mutex *lock )