2565 goto ldv_17779;
2566 } else
2567#line 247
2568 if (ldv_s_capabilities_file_ops_file_operations != 0) {
2569#line 249
2570 goto ldv_17779;
2571 } else {
2572#line 251
2573 goto ldv_17781;
2574 }
2575 ldv_17781: ;
2576 ldv_module_exit:
2577 {
2578#line 300
2579 xenfs_exit();
2580 }
2581 ldv_final:
2582 {
2583#line 303
2584 ldv_check_final_state();
2585 }
2586#line 306
2587 return;
2588}
2589}
2590#line 5 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--43_1a--X--cpachecker/linux-3.4/csd_deg_dscv/4542/dscv_tempdir/dscv/ri/43_1a/kernel-rules/files/engine-blast-assert.h"
2591void ldv_blast_assert(void)
2592{
2593
2594 {
2595 ERROR: ;
2596#line 6
2597 goto ERROR;
2598}
2599}
2600#line 6 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--43_1a--X--cpachecker/linux-3.4/csd_deg_dscv/4542/dscv_tempdir/dscv/ri/43_1a/kernel-rules/files/engine-blast.h"
2601extern int __VERIFIER_nondet_int(void) ;
2602#line 327 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--43_1a--X--cpachecker/linux-3.4/csd_deg_dscv/4542/dscv_tempdir/dscv/ri/43_1a/drivers/xen/xenfs/super.c.p"
2603int ldv_spin = 0;
2604#line 331 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--43_1a--X--cpachecker/linux-3.4/csd_deg_dscv/4542/dscv_tempdir/dscv/ri/43_1a/drivers/xen/xenfs/super.c.p"
2605void ldv_check_alloc_flags(gfp_t flags )