4010 switch_default:
4011#line 194
4012 goto switch_break;
4013 } else {
4014 switch_break: ;
4015 }
4016 }
4017 }
4018 }
4019 while_break: ;
4020 }
4021 ldv_module_exit:
4022 {
4023#line 208
4024 poulsbo_exit();
4025 }
4026 ldv_final:
4027 {
4028#line 211
4029 ldv_check_final_state();
4030 }
4031#line 214
4032 return;
4033}
4034}
4035#line 5 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/6963/dscv_tempdir/dscv/ri/32_1/kernel-rules/files/engine-blast-assert.h"
4036void ldv_blast_assert(void)
4037{
4038
4039 {
4040 ERROR:
4041#line 6
4042 goto ERROR;
4043}
4044}
4045#line 6 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/6963/dscv_tempdir/dscv/ri/32_1/kernel-rules/files/engine-blast.h"
4046extern int __VERIFIER_nondet_int(void) ;
4047#line 19 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/6963/dscv_tempdir/dscv/ri/32_1/kernel-rules/files/model0032.c"
4048int ldv_mutex = 1;
4049#line 22 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/6963/dscv_tempdir/dscv/ri/32_1/kernel-rules/files/model0032.c"
4050int __attribute__((__warn_unused_result__)) mutex_lock_interruptible(struct mutex *lock )