2560#line 321
2561 if (0) {
2562 switch_default:
2563#line 323
2564 goto switch_break;
2565 } else {
2566 switch_break: ;
2567 }
2568 }
2569 }
2570 while_break: ;
2571 }
2572 {
2573#line 339
2574 ramoops_exit();
2575 }
2576 ldv_final:
2577 {
2578#line 342
2579 ldv_check_final_state();
2580 }
2581#line 345
2582 return;
2583}
2584}
2585#line 5 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/16701/dscv_tempdir/dscv/ri/32_1/kernel-rules/files/engine-blast-assert.h"
2586void ldv_blast_assert(void)
2587{
2588
2589 {
2590 ERROR:
2591#line 6
2592 goto ERROR;
2593}
2594}
2595#line 6 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/16701/dscv_tempdir/dscv/ri/32_1/kernel-rules/files/engine-blast.h"
2596extern int __VERIFIER_nondet_int(void) ;
2597#line 19 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/16701/dscv_tempdir/dscv/ri/32_1/kernel-rules/files/model0032.c"
2598int ldv_mutex = 1;
2599#line 22 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/16701/dscv_tempdir/dscv/ri/32_1/kernel-rules/files/model0032.c"
2600int __attribute__((__warn_unused_result__)) mutex_lock_interruptible(struct mutex *lock )