28011 goto ldv_33029;
28012 } else
28013#line 4577
28014 if (ldv_s_adpt_fops_file_operations != 0) {
28015#line 4579
28016 goto ldv_33029;
28017 } else {
28018#line 4581
28019 goto ldv_33031;
28020 }
28021 ldv_33031: ;
28022 ldv_module_exit:
28023 {
28024#line 5516
28025 adpt_exit();
28026 }
28027 ldv_final:
28028 {
28029#line 5519
28030 ldv_check_final_state();
28031 }
28032#line 5522
28033 return;
28034}
28035}
28036#line 5 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--43_1a--X--cpachecker/linux-3.4/csd_deg_dscv/3986/dscv_tempdir/dscv/ri/43_1a/kernel-rules/files/engine-blast-assert.h"
28037void ldv_blast_assert(void)
28038{
28039
28040 {
28041 ERROR: ;
28042#line 6
28043 goto ERROR;
28044}
28045}
28046#line 6 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--43_1a--X--cpachecker/linux-3.4/csd_deg_dscv/3986/dscv_tempdir/dscv/ri/43_1a/kernel-rules/files/engine-blast.h"
28047extern int __VERIFIER_nondet_int(void) ;
28048#line 5543 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--43_1a--X--cpachecker/linux-3.4/csd_deg_dscv/3986/dscv_tempdir/dscv/ri/43_1a/drivers/scsi/dpt_i2o.c.p"
28049int ldv_spin = 0;
28050#line 5547 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--43_1a--X--cpachecker/linux-3.4/csd_deg_dscv/3986/dscv_tempdir/dscv/ri/43_1a/drivers/scsi/dpt_i2o.c.p"
28051void ldv_check_alloc_flags(gfp_t flags )