6702 switch_default:
6703#line 845
6704 goto switch_break;
6705 } else {
6706 switch_break: ;
6707 }
6708 }
6709 }
6710 }
6711 while_break: ;
6712 }
6713 ldv_module_exit:
6714 {
6715#line 862
6716 ipaq_exit();
6717 }
6718 ldv_final:
6719 {
6720#line 865
6721 ldv_check_final_state();
6722 }
6723#line 868
6724 return;
6725}
6726}
6727#line 5 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/7534/dscv_tempdir/dscv/ri/32_1/kernel-rules/files/engine-blast-assert.h"
6728void ldv_blast_assert(void)
6729{
6730
6731 {
6732 ERROR:
6733#line 6
6734 goto ERROR;
6735}
6736}
6737#line 6 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/7534/dscv_tempdir/dscv/ri/32_1/kernel-rules/files/engine-blast.h"
6738extern int __VERIFIER_nondet_int(void) ;
6739#line 19 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/7534/dscv_tempdir/dscv/ri/32_1/kernel-rules/files/model0032.c"
6740int ldv_mutex = 1;
6741#line 22 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/7534/dscv_tempdir/dscv/ri/32_1/kernel-rules/files/model0032.c"
6742int __attribute__((__warn_unused_result__)) mutex_lock_interruptible(struct mutex *lock )