7584 goto ldv_40205;
7585 } else
7586#line 485
7587 if (ldv_s_wl1251_spi_driver_spi_driver != 0) {
7588#line 487
7589 goto ldv_40205;
7590 } else {
7591#line 489
7592 goto ldv_40207;
7593 }
7594 ldv_40207: ;
7595 ldv_module_exit:
7596 {
7597#line 634
7598 wl1251_spi_exit();
7599 }
7600 ldv_final:
7601 {
7602#line 637
7603 ldv_check_final_state();
7604 }
7605#line 640
7606 return;
7607}
7608}
7609#line 5 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--43_1a--X--cpachecker/linux-3.4/csd_deg_dscv/14397/dscv_tempdir/dscv/ri/43_1a/kernel-rules/files/engine-blast-assert.h"
7610void ldv_blast_assert(void)
7611{
7612
7613 {
7614 ERROR: ;
7615#line 6
7616 goto ERROR;
7617}
7618}
7619#line 6 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--43_1a--X--cpachecker/linux-3.4/csd_deg_dscv/14397/dscv_tempdir/dscv/ri/43_1a/kernel-rules/files/engine-blast.h"
7620extern int __VERIFIER_nondet_int(void) ;
7621#line 661 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--43_1a--X--cpachecker/linux-3.4/csd_deg_dscv/14397/dscv_tempdir/dscv/ri/43_1a/drivers/net/wireless/wl1251/spi.c.p"
7622int ldv_spin = 0;
7623#line 665 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--43_1a--X--cpachecker/linux-3.4/csd_deg_dscv/14397/dscv_tempdir/dscv/ri/43_1a/drivers/net/wireless/wl1251/spi.c.p"
7624void ldv_check_alloc_flags(gfp_t flags )