7340 switch_default:
7341#line 390
7342 goto switch_break;
7343 } else {
7344 switch_break: ;
7345 }
7346 }
7347 }
7348 }
7349 while_break: ;
7350 }
7351 ldv_module_exit:
7352 {
7353#line 410
7354 orinoco_pci_exit();
7355 }
7356 ldv_final:
7357 {
7358#line 413
7359 ldv_check_final_state();
7360 }
7361#line 416
7362 return;
7363}
7364}
7365#line 5 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/10308/dscv_tempdir/dscv/ri/32_1/kernel-rules/files/engine-blast-assert.h"
7366void ldv_blast_assert(void)
7367{
7368
7369 {
7370 ERROR:
7371#line 6
7372 goto ERROR;
7373}
7374}
7375#line 6 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/10308/dscv_tempdir/dscv/ri/32_1/kernel-rules/files/engine-blast.h"
7376extern int __VERIFIER_nondet_int(void) ;
7377#line 19 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/10308/dscv_tempdir/dscv/ri/32_1/kernel-rules/files/model0032.c"
7378int ldv_mutex = 1;
7379#line 22 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/10308/dscv_tempdir/dscv/ri/32_1/kernel-rules/files/model0032.c"
7380int __attribute__((__warn_unused_result__)) mutex_lock_interruptible(struct mutex *lock )