9542 switch_default:
9543#line 810
9544 goto switch_break;
9545 } else {
9546 switch_break: ;
9547 }
9548 }
9549 }
9550 }
9551 while_break: ;
9552 }
9553 ldv_module_exit:
9554 {
9555#line 833
9556 wl1271_exit();
9557 }
9558 ldv_final:
9559 {
9560#line 836
9561 ldv_check_final_state();
9562 }
9563#line 839
9564 return;
9565}
9566}
9567#line 5 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/9905/dscv_tempdir/dscv/ri/32_1/kernel-rules/files/engine-blast-assert.h"
9568void ldv_blast_assert(void)
9569{
9570
9571 {
9572 ERROR:
9573#line 6
9574 goto ERROR;
9575}
9576}
9577#line 6 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/9905/dscv_tempdir/dscv/ri/32_1/kernel-rules/files/engine-blast.h"
9578extern int __VERIFIER_nondet_int(void) ;
9579#line 19 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/9905/dscv_tempdir/dscv/ri/32_1/kernel-rules/files/model0032.c"
9580int ldv_mutex = 1;
9581#line 22 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/9905/dscv_tempdir/dscv/ri/32_1/kernel-rules/files/model0032.c"
9582int __attribute__((__warn_unused_result__)) mutex_lock_interruptible(struct mutex *lock )