5519 goto ldv_36013;
5520 } else
5521#line 335
5522 if (ldv_s_marvell_pci_driver_pci_driver != 0) {
5523#line 337
5524 goto ldv_36013;
5525 } else {
5526#line 339
5527 goto ldv_36015;
5528 }
5529 ldv_36015: ;
5530 ldv_module_exit:
5531 {
5532#line 436
5533 marvell_exit();
5534 }
5535 ldv_final:
5536 {
5537#line 439
5538 ldv_check_final_state();
5539 }
5540#line 442
5541 return;
5542}
5543}
5544#line 5 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--43_1a--X--cpachecker/linux-3.4/csd_deg_dscv/17119/dscv_tempdir/dscv/ri/43_1a/kernel-rules/files/engine-blast-assert.h"
5545void ldv_blast_assert(void)
5546{
5547
5548 {
5549 ERROR: ;
5550#line 6
5551 goto ERROR;
5552}
5553}
5554#line 6 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--43_1a--X--cpachecker/linux-3.4/csd_deg_dscv/17119/dscv_tempdir/dscv/ri/43_1a/kernel-rules/files/engine-blast.h"
5555extern int __VERIFIER_nondet_int(void) ;
5556#line 463 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--43_1a--X--cpachecker/linux-3.4/csd_deg_dscv/17119/dscv_tempdir/dscv/ri/43_1a/drivers/ata/pata_marvell.c.p"
5557int ldv_spin = 0;
5558#line 467 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--43_1a--X--cpachecker/linux-3.4/csd_deg_dscv/17119/dscv_tempdir/dscv/ri/43_1a/drivers/ata/pata_marvell.c.p"
5559void ldv_check_alloc_flags(gfp_t flags )