2750 switch_default:
2751#line 670
2752 goto switch_break;
2753 } else {
2754 switch_break: ;
2755 }
2756 }
2757 }
2758 }
2759 while_break: ;
2760 }
2761 ldv_module_exit:
2762 {
2763#line 687
2764 wm831x_gpio_exit();
2765 }
2766 ldv_final:
2767 {
2768#line 690
2769 ldv_check_final_state();
2770 }
2771#line 693
2772 return;
2773}
2774}
2775#line 5 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/5860/dscv_tempdir/dscv/ri/32_1/kernel-rules/files/engine-blast-assert.h"
2776void ldv_blast_assert(void)
2777{
2778
2779 {
2780 ERROR:
2781#line 6
2782 goto ERROR;
2783}
2784}
2785#line 6 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/5860/dscv_tempdir/dscv/ri/32_1/kernel-rules/files/engine-blast.h"
2786extern int __VERIFIER_nondet_int(void) ;
2787#line 19 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/5860/dscv_tempdir/dscv/ri/32_1/kernel-rules/files/model0032.c"
2788int ldv_mutex = 1;
2789#line 22 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/5860/dscv_tempdir/dscv/ri/32_1/kernel-rules/files/model0032.c"
2790int __attribute__((__warn_unused_result__)) mutex_lock_interruptible(struct mutex *lock )