4503 goto switch_break;
4504 switch_default:
4505#line 389
4506 goto switch_break;
4507 } else {
4508 switch_break: ;
4509 }
4510 }
4511 }
4512 }
4513 while_break: ;
4514 }
4515 ldv_module_exit:
4516 {
4517#line 403
4518 wl1273_core_exit();
4519 }
4520 {
4521#line 406
4522 ldv_check_final_state();
4523 }
4524#line 409
4525 return;
4526}
4527}
4528#line 5 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/8235/dscv_tempdir/dscv/ri/32_1/kernel-rules/files/engine-blast-assert.h"
4529void ldv_blast_assert(void)
4530{
4531
4532 {
4533 ERROR:
4534#line 6
4535 goto ERROR;
4536}
4537}
4538#line 6 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/8235/dscv_tempdir/dscv/ri/32_1/kernel-rules/files/engine-blast.h"
4539extern int __VERIFIER_nondet_int(void) ;
4540#line 19 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/8235/dscv_tempdir/dscv/ri/32_1/kernel-rules/files/model0032.c"
4541int ldv_mutex = 1;
4542#line 22 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/8235/dscv_tempdir/dscv/ri/32_1/kernel-rules/files/model0032.c"
4543int __attribute__((__warn_unused_result__)) mutex_lock_interruptible(struct mutex *lock )