4254 switch_default:
4255#line 518
4256 goto switch_break;
4257 } else {
4258 switch_break: ;
4259 }
4260 }
4261 }
4262 }
4263 while_break: ;
4264 }
4265 ldv_module_exit:
4266 {
4267#line 532
4268 wm831x_isink_exit();
4269 }
4270 ldv_final:
4271 {
4272#line 535
4273 ldv_check_final_state();
4274 }
4275#line 538
4276 return;
4277}
4278}
4279#line 5 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/4593/dscv_tempdir/dscv/ri/32_1/kernel-rules/files/engine-blast-assert.h"
4280void ldv_blast_assert(void)
4281{
4282
4283 {
4284 ERROR:
4285#line 6
4286 goto ERROR;
4287}
4288}
4289#line 6 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/4593/dscv_tempdir/dscv/ri/32_1/kernel-rules/files/engine-blast.h"
4290extern int __VERIFIER_nondet_int(void) ;
4291#line 19 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/4593/dscv_tempdir/dscv/ri/32_1/kernel-rules/files/model0032.c"
4292int ldv_mutex = 1;
4293#line 22 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/4593/dscv_tempdir/dscv/ri/32_1/kernel-rules/files/model0032.c"
4294int __attribute__((__warn_unused_result__)) mutex_lock_interruptible(struct mutex *lock )