9214 switch_default:
9215#line 3132
9216 goto switch_break;
9217 } else {
9218 switch_break: ;
9219 }
9220 }
9221 }
9222 }
9223 while_break: ;
9224 }
9225 ldv_module_exit:
9226 {
9227#line 3158
9228 wm831x_dcdc_exit();
9229 }
9230 ldv_final:
9231 {
9232#line 3161
9233 ldv_check_final_state();
9234 }
9235#line 3164
9236 return;
9237}
9238}
9239#line 5 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/4592/dscv_tempdir/dscv/ri/32_1/kernel-rules/files/engine-blast-assert.h"
9240void ldv_blast_assert(void)
9241{
9242
9243 {
9244 ERROR:
9245#line 6
9246 goto ERROR;
9247}
9248}
9249#line 6 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/4592/dscv_tempdir/dscv/ri/32_1/kernel-rules/files/engine-blast.h"
9250extern int __VERIFIER_nondet_int(void) ;
9251#line 19 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/4592/dscv_tempdir/dscv/ri/32_1/kernel-rules/files/model0032.c"
9252int ldv_mutex = 1;
9253#line 22 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/4592/dscv_tempdir/dscv/ri/32_1/kernel-rules/files/model0032.c"
9254int __attribute__((__warn_unused_result__)) mutex_lock_interruptible(struct mutex *lock )