8128 switch_default:
8129#line 608
8130 goto switch_break;
8131 } else {
8132 switch_break: ;
8133 }
8134 }
8135 }
8136 }
8137 while_break: ;
8138 }
8139 ldv_module_exit:
8140 {
8141#line 620
8142 wl1251_spi_exit();
8143 }
8144 ldv_final:
8145 {
8146#line 623
8147 ldv_check_final_state();
8148 }
8149#line 626
8150 return;
8151}
8152}
8153#line 5 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/9994/dscv_tempdir/dscv/ri/32_1/kernel-rules/files/engine-blast-assert.h"
8154void ldv_blast_assert(void)
8155{
8156
8157 {
8158 ERROR:
8159#line 6
8160 goto ERROR;
8161}
8162}
8163#line 6 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/9994/dscv_tempdir/dscv/ri/32_1/kernel-rules/files/engine-blast.h"
8164extern int __VERIFIER_nondet_int(void) ;
8165#line 19 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/9994/dscv_tempdir/dscv/ri/32_1/kernel-rules/files/model0032.c"
8166int ldv_mutex = 1;
8167#line 22 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/9994/dscv_tempdir/dscv/ri/32_1/kernel-rules/files/model0032.c"
8168int __attribute__((__warn_unused_result__)) mutex_lock_interruptible(struct mutex *lock )