Require Import Coqlib.
Require Import AST.
Require Import Integers.
Require Import Values.
Require Import Cop.
Require Import Clight.
Require Import CDataTypes.
Require Import Ctypes.
Require Import Ident.
Local Open Scope Z_scope.
Definition _Rd : ident := 999%positive.
Definition _addr := 1%positive.
Definition _arg := 2%positive.
Definition _base := 3%positive.
Definition _cbndx := 4%positive.
Definition _cnt := 5%positive.
Definition _count := 6%positive.
Definition _cur_vcpuid := 7%positive.
Definition _cur_vmid := 8%positive.
Definition _end := 9%positive.
Definition _esr := 10%positive.
Definition _gfn := 11%positive.
Definition _gpa := 12%positive.
Definition _i := 13%positive.
Definition _index := 14%positive.
Definition _iova := 15%positive.
Definition _kvm := 16%positive.
Definition _level := 17%positive.
Definition _load_addr := 18%positive.
Definition _load_idx := 19%positive.
Definition _load_info_cnt := 20%positive.
Definition _main := 21%positive.
Definition _map := 22%positive.
Definition _mapped := 23%positive.
Definition _num := 24%positive.
Definition _owner := 25%positive.
Definition _pa := 26%positive.
Definition _paddr := 27%positive.
Definition _page_count := 28%positive.
Definition _pass_lock := 29%positive.
Definition _perm := 30%positive.
Definition _pfn := 31%positive.
Definition _pgnum := 32%positive.
Definition _power := 33%positive.
Definition _prot := 34%positive.
Definition _pte := 35%positive.
Definition _remap := 36%positive.
Definition _remap_addr := 37%positive.
Definition _res := 38%positive.
Definition _ret := 39%positive.
Definition _size := 40%positive.
Definition _start := 41%positive.
Definition _state := 42%positive.
Definition _target := 43%positive.
Definition _target_addr := 44%positive.
Definition _valid := 45%positive.
Definition _vcpu := 46%positive.
Definition _vcpu_state := 47%positive.
Definition _vcpuid := 48%positive.
Definition _vm_state := 49%positive.
Definition _vmid := 50%positive.
Definition _wait_lock := 51%positive.
Definition _t'1 := 52%positive.
Definition _t'2 := 53%positive.
Definition _t'3 := 54%positive.
Definition _t'4 := 55%positive.
Definition mem_region_search_body :=
(Ssequence
(Ssequence
(Scall (Some _t'1)
(Evar get_mem_region_cnt (Tfunction Tnil tuint cc_default)) nil)
(Sset _cnt (Etempvar _t'1 tuint)))
(Ssequence
(Sset _i (Econst_int (Int.repr 0) tuint))
(Ssequence
(Sset _res (Econst_int (Int.repr (-1)) tuint))
(Ssequence
(Swhile
(Ebinop Olt (Etempvar _i tuint) (Etempvar _cnt tuint) tint)
(Ssequence
(Ssequence
(Scall (Some _t'2)
(Evar get_mem_region_base (Tfunction (Tcons tuint Tnil)
tulong cc_default))
((Etempvar _i tuint) :: nil))
(Sset _base (Etempvar _t'2 tulong)))
(Ssequence
(Ssequence
(Scall (Some _t'3)
(Evar get_mem_region_size (Tfunction (Tcons tuint Tnil)
tulong cc_default))
((Etempvar _i tuint) :: nil))
(Sset _size (Etempvar _t'3 tulong)))
(Ssequence
(Ssequence
(Sifthenelse (Ebinop Ole (Etempvar _base tulong)
(Etempvar _addr tulong) tint)
(Sset _t'4
(Ecast
(Ebinop Olt (Etempvar _addr tulong)
(Ebinop Oadd (Etempvar _base tulong)
(Etempvar _size tulong) tulong) tint) tbool))
(Sset _t'4 (Econst_int (Int.repr 0) tint)))
(Sifthenelse (Etempvar _t'4 tint)
(Sset _res (Etempvar _i tuint))
Sskip))
(Sset _i
(Ebinop Oadd (Etempvar _i tuint)
(Econst_int (Int.repr 1) tuint) tuint))))))
(Sreturn (Some (Etempvar _res tuint))))))).
Definition f_mem_region_search := {|
fn_return := tuint;
fn_callconv := cc_default;
fn_params := ((_addr, tulong) :: nil);
fn_vars := nil;
fn_temps := ((_base, tulong) :: (_size, tulong) :: (_cnt, tuint) ::
(_i, tuint) :: (_res, tuint) :: (_t'4, tint) ::
(_t'3, tulong) :: (_t'2, tulong) :: (_t'1, tuint) :: nil);
fn_body := mem_region_search_body
|}.