3810 switch_default:
3811#line 296
3812 goto switch_break;
3813 } else {
3814 switch_break: ;
3815 }
3816 }
3817 }
3818 }
3819 while_break: ;
3820 }
3821 ldv_module_exit:
3822 {
3823#line 310
3824 acpi_ec_sys_exit();
3825 }
3826 ldv_final:
3827 {
3828#line 313
3829 ldv_check_final_state();
3830 }
3831#line 316
3832 return;
3833}
3834}
3835#line 5 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/93/dscv_tempdir/dscv/ri/32_1/kernel-rules/files/engine-blast-assert.h"
3836void ldv_blast_assert(void)
3837{
3838
3839 {
3840 ERROR:
3841#line 6
3842 goto ERROR;
3843}
3844}
3845#line 6 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/93/dscv_tempdir/dscv/ri/32_1/kernel-rules/files/engine-blast.h"
3846extern int __VERIFIER_nondet_int(void) ;
3847#line 19 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/93/dscv_tempdir/dscv/ri/32_1/kernel-rules/files/model0032.c"
3848int ldv_mutex = 1;
3849#line 22 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/93/dscv_tempdir/dscv/ri/32_1/kernel-rules/files/model0032.c"
3850int __attribute__((__warn_unused_result__)) mutex_lock_interruptible(struct mutex *lock )