fact: Definition f_heapsort := {| fn_return := tvoid; fn_callconv := cc_default; fn_params := ((_arr, (tptr (Tstruct _edge noattr))) :: (_sz, tint) :: nil); fn_vars := nil; fn_temps := ((_size, tuint) :: (_active, tuint) :: nil); fn_body := (Ssequence (Sifthenelse (Ebinop Oeq (Etempvar _sz tint) (Econst_int (Int.repr 0) tint) tint) (Sreturn None) Sskip) (Ssequence (Sset _size (Ecast (Etempvar _sz tint) tuint)) (Ssequence (Scall None (Evar _build_heap (Tfunction (Tcons (tptr (Tstruct _edge noattr)) (Tcons tuint Tnil)) tvoid cc_default)) ((Etempvar _arr (tptr (Tstruct _edge noattr))) :: (Etempvar _size tuint) :: nil)) (Ssequence (Sset _active (Etempvar _size tuint)) (Swhile (Ebinop Ogt (Etempvar _active tuint) (Econst_int (Int.repr 1) tint) tint) (Ssequence (Sset _active (Ebinop Osub (Etempvar _active tuint) (Econst_int (Int.repr 1) tint) tuint)) (Ssequence (Scall None (Evar _exch (Tfunction (Tcons tuint (Tcons tuint (Tcons (tptr (Tstruct _edge noattr)) Tnil))) tvoid cc_default)) ((Econst_int (Int.repr 0) tuint) :: (Etempvar _active tuint) :: (Etempvar _arr (tptr (Tstruct _edge noattr))) :: nil)) (Scall None (Evar _sink (Tfunction (Tcons tuint (Tcons (tptr (Tstruct _edge noattr)) (Tcons tuint Tnil))) tvoid cc_default)) ((Econst_int (Int.repr 0) tuint) :: (Etempvar _arr (tptr (Tstruct _edge noattr))) :: (Etempvar _active tuint) :: nil))))))))) |}.
imports: Coq(String List ZArith) compcert(Coqlib Integers Floats AST Ctypes Cop Clight Clightdefs)