fact: Definition f_build_heap := {| fn_return := tvoid; fn_callconv := cc_default; fn_params := ((_arr, (tptr (Tstruct _structItem noattr))) :: (_size__1, tuint) :: nil); fn_vars := nil; fn_temps := ((_start, tuint) :: nil); fn_body := (Ssequence (Sset _start (Ebinop Odiv (Ebinop Osub (Etempvar _size__1 tuint) (Econst_int (Int.repr 1) tuint) tuint) (Econst_int (Int.repr 2) tuint) tuint)) (Sloop (Ssequence Sskip (Ssequence (Scall None (Evar _sink (Tfunction (Tcons tuint (Tcons (tptr (Tstruct _structItem noattr)) (Tcons tuint Tnil))) tvoid cc_default)) ((Etempvar _start tuint) :: (Etempvar _arr (tptr (Tstruct _structItem noattr))) :: (Etempvar _size__1 tuint) :: nil)) (Ssequence (Sifthenelse (Ebinop Oeq (Etempvar _start tuint) (Econst_int (Int.repr 0) tint) tint) Sbreak Sskip) (Sset _start (Ebinop Osub (Etempvar _start tuint) (Econst_int (Int.repr 1) tint) tuint))))) Sskip)) |}.
imports: Coq(String List ZArith) compcert(Coqlib Integers Floats AST Ctypes Cop Clight Clightdefs)