4532 switch_default:
4533#line 519
4534 goto switch_break;
4535 } else {
4536 switch_break: ;
4537 }
4538 }
4539 }
4540 }
4541 while_break: ;
4542 }
4543 ldv_module_exit:
4544 {
4545#line 537
4546 pm_exit();
4547 }
4548 ldv_final:
4549 {
4550#line 540
4551 ldv_check_final_state();
4552 }
4553#line 543
4554 return;
4555}
4556}
4557#line 5 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/4186/dscv_tempdir/dscv/ri/32_1/kernel-rules/files/engine-blast-assert.h"
4558void ldv_blast_assert(void)
4559{
4560
4561 {
4562 ERROR:
4563#line 6
4564 goto ERROR;
4565}
4566}
4567#line 6 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/4186/dscv_tempdir/dscv/ri/32_1/kernel-rules/files/engine-blast.h"
4568extern int __VERIFIER_nondet_int(void) ;
4569#line 19 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/4186/dscv_tempdir/dscv/ri/32_1/kernel-rules/files/model0032.c"
4570int ldv_mutex = 1;
4571#line 22 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/4186/dscv_tempdir/dscv/ri/32_1/kernel-rules/files/model0032.c"
4572int __attribute__((__warn_unused_result__)) mutex_lock_interruptible(struct mutex *lock )