6465 goto ldv_23676;
6466 } else
6467#line 885
6468 if (ldv_s_available_error_type_fops_file_operations != 0) {
6469#line 887
6470 goto ldv_23676;
6471 } else {
6472#line 889
6473 goto ldv_23678;
6474 }
6475 ldv_23678: ;
6476 ldv_module_exit:
6477 {
6478#line 944
6479 einj_exit();
6480 }
6481 ldv_final:
6482 {
6483#line 947
6484 ldv_check_final_state();
6485 }
6486#line 950
6487 return;
6488}
6489}
6490#line 5 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--43_1a--X--cpachecker/linux-3.4/csd_deg_dscv/4568/dscv_tempdir/dscv/ri/43_1a/kernel-rules/files/engine-blast-assert.h"
6491void ldv_blast_assert(void)
6492{
6493
6494 {
6495 ERROR: ;
6496#line 6
6497 goto ERROR;
6498}
6499}
6500#line 6 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--43_1a--X--cpachecker/linux-3.4/csd_deg_dscv/4568/dscv_tempdir/dscv/ri/43_1a/kernel-rules/files/engine-blast.h"
6501extern int __VERIFIER_nondet_int(void) ;
6502#line 971 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--43_1a--X--cpachecker/linux-3.4/csd_deg_dscv/4568/dscv_tempdir/dscv/ri/43_1a/drivers/acpi/apei/einj.c.p"
6503int ldv_spin = 0;
6504#line 975 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--43_1a--X--cpachecker/linux-3.4/csd_deg_dscv/4568/dscv_tempdir/dscv/ri/43_1a/drivers/acpi/apei/einj.c.p"
6505void ldv_check_alloc_flags(gfp_t flags )