3453 switch_default:
3454#line 359
3455 goto switch_break;
3456 } else {
3457 switch_break: ;
3458 }
3459 }
3460 }
3461 }
3462 while_break: ;
3463 }
3464 ldv_module_exit:
3465 {
3466#line 374
3467 tsc_exit();
3468 }
3469 ldv_final:
3470 {
3471#line 377
3472 ldv_check_final_state();
3473 }
3474#line 380
3475 return;
3476}
3477}
3478#line 5 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/4196/dscv_tempdir/dscv/ri/32_1/kernel-rules/files/engine-blast-assert.h"
3479void ldv_blast_assert(void)
3480{
3481
3482 {
3483 ERROR:
3484#line 6
3485 goto ERROR;
3486}
3487}
3488#line 6 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/4196/dscv_tempdir/dscv/ri/32_1/kernel-rules/files/engine-blast.h"
3489extern int __VERIFIER_nondet_int(void) ;
3490#line 19 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/4196/dscv_tempdir/dscv/ri/32_1/kernel-rules/files/model0032.c"
3491int ldv_mutex = 1;
3492#line 22 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/4196/dscv_tempdir/dscv/ri/32_1/kernel-rules/files/model0032.c"
3493int __attribute__((__warn_unused_result__)) mutex_lock_interruptible(struct mutex *lock )