9572 goto ldv_26933;
9573 } else
9574#line 1417
9575 if (ldv_s_lsi_fops_file_operations != 0) {
9576#line 1419
9577 goto ldv_26933;
9578 } else {
9579#line 1421
9580 goto ldv_26935;
9581 }
9582 ldv_26935: ;
9583 ldv_module_exit:
9584 {
9585#line 1545
9586 mraid_mm_exit();
9587 }
9588 ldv_final:
9589 {
9590#line 1548
9591 ldv_check_final_state();
9592 }
9593#line 1551
9594 return;
9595}
9596}
9597#line 5 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--43_1a--X--cpachecker/linux-3.4/csd_deg_dscv/3550/dscv_tempdir/dscv/ri/43_1a/kernel-rules/files/engine-blast-assert.h"
9598void ldv_blast_assert(void)
9599{
9600
9601 {
9602 ERROR: ;
9603#line 6
9604 goto ERROR;
9605}
9606}
9607#line 6 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--43_1a--X--cpachecker/linux-3.4/csd_deg_dscv/3550/dscv_tempdir/dscv/ri/43_1a/kernel-rules/files/engine-blast.h"
9608extern int __VERIFIER_nondet_int(void) ;
9609#line 1572 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--43_1a--X--cpachecker/linux-3.4/csd_deg_dscv/3550/dscv_tempdir/dscv/ri/43_1a/drivers/scsi/megaraid/megaraid_mm.c.p"
9610int ldv_spin = 0;
9611#line 1576 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--43_1a--X--cpachecker/linux-3.4/csd_deg_dscv/3550/dscv_tempdir/dscv/ri/43_1a/drivers/scsi/megaraid/megaraid_mm.c.p"
9612void ldv_check_alloc_flags(gfp_t flags )