4511 switch_default:
4512#line 455
4513 goto switch_break;
4514 } else {
4515 switch_break: ;
4516 }
4517 }
4518 }
4519 }
4520 while_break: ;
4521 }
4522 ldv_module_exit:
4523 {
4524#line 474
4525 tle62x0_exit();
4526 }
4527 ldv_final:
4528 {
4529#line 477
4530 ldv_check_final_state();
4531 }
4532#line 480
4533 return;
4534}
4535}
4536#line 5 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/16730/dscv_tempdir/dscv/ri/32_1/kernel-rules/files/engine-blast-assert.h"
4537void ldv_blast_assert(void)
4538{
4539
4540 {
4541 ERROR:
4542#line 6
4543 goto ERROR;
4544}
4545}
4546#line 6 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/16730/dscv_tempdir/dscv/ri/32_1/kernel-rules/files/engine-blast.h"
4547extern int __VERIFIER_nondet_int(void) ;
4548#line 19 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/16730/dscv_tempdir/dscv/ri/32_1/kernel-rules/files/model0032.c"
4549int ldv_mutex = 1;
4550#line 22 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/16730/dscv_tempdir/dscv/ri/32_1/kernel-rules/files/model0032.c"
4551int __attribute__((__warn_unused_result__)) mutex_lock_interruptible(struct mutex *lock )