7572 goto ldv_36501;
7573 } else
7574#line 562
7575 if (ldv_s_abyss_driver_pci_driver != 0) {
7576#line 564
7577 goto ldv_36501;
7578 } else {
7579#line 566
7580 goto ldv_36503;
7581 }
7582 ldv_36503: ;
7583 ldv_module_exit:
7584 {
7585#line 603
7586 abyss_rmmod();
7587 }
7588 ldv_final:
7589 {
7590#line 606
7591 ldv_check_final_state();
7592 }
7593#line 609
7594 return;
7595}
7596}
7597#line 5 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--43_1a--X--cpachecker/linux-3.4/csd_deg_dscv/15094/dscv_tempdir/dscv/ri/43_1a/kernel-rules/files/engine-blast-assert.h"
7598void ldv_blast_assert(void)
7599{
7600
7601 {
7602 ERROR: ;
7603#line 6
7604 goto ERROR;
7605}
7606}
7607#line 6 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--43_1a--X--cpachecker/linux-3.4/csd_deg_dscv/15094/dscv_tempdir/dscv/ri/43_1a/kernel-rules/files/engine-blast.h"
7608extern int __VERIFIER_nondet_int(void) ;
7609#line 630 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--43_1a--X--cpachecker/linux-3.4/csd_deg_dscv/15094/dscv_tempdir/dscv/ri/43_1a/drivers/net/tokenring/abyss.c.p"
7610int ldv_spin = 0;
7611#line 634 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--43_1a--X--cpachecker/linux-3.4/csd_deg_dscv/15094/dscv_tempdir/dscv/ri/43_1a/drivers/net/tokenring/abyss.c.p"
7612void ldv_check_alloc_flags(gfp_t flags )