2630 goto switch_break;
2631 switch_default:
2632#line 388
2633 goto switch_break;
2634 } else {
2635 switch_break: ;
2636 }
2637 }
2638 }
2639 }
2640 while_break: ;
2641 }
2642 {
2643#line 400
2644 gpio_trig_exit();
2645 }
2646 ldv_final:
2647 {
2648#line 403
2649 ldv_check_final_state();
2650 }
2651#line 406
2652 return;
2653}
2654}
2655#line 5 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/12615/dscv_tempdir/dscv/ri/32_1/kernel-rules/files/engine-blast-assert.h"
2656void ldv_blast_assert(void)
2657{
2658
2659 {
2660 ERROR:
2661#line 6
2662 goto ERROR;
2663}
2664}
2665#line 6 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/12615/dscv_tempdir/dscv/ri/32_1/kernel-rules/files/engine-blast.h"
2666extern int __VERIFIER_nondet_int(void) ;
2667#line 19 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/12615/dscv_tempdir/dscv/ri/32_1/kernel-rules/files/model0032.c"
2668int ldv_mutex = 1;
2669#line 22 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/12615/dscv_tempdir/dscv/ri/32_1/kernel-rules/files/model0032.c"
2670int __attribute__((__warn_unused_result__)) mutex_lock_interruptible(struct mutex *lock )