fact: Definition f_heapify := {| fn_return := (tptr (Tstruct _structPQ noattr)); fn_callconv := cc_default; fn_params := ((_arr, (tptr (Tstruct _structItem noattr))) :: (_size__1, tuint) :: nil); fn_vars := nil; fn_temps := ((_pq, (tptr (Tstruct _structPQ noattr))) :: (_t'1, (tptr tvoid)) :: nil); fn_body := (Ssequence (Scall None (Evar _build_heap (Tfunction (Tcons (tptr (Tstruct _structItem noattr)) (Tcons tuint Tnil)) tvoid cc_default)) ((Etempvar _arr (tptr (Tstruct _structItem noattr))) :: (Etempvar _size__1 tuint) :: nil)) (Ssequence (Ssequence (Scall (Some _t'1) (Evar _mallocN (Tfunction (Tcons tint Tnil) (tptr tvoid) cc_default)) ((Esizeof (Tstruct _structPQ noattr) tuint) :: nil)) (Sset _pq (Ecast (Etempvar _t'1 (tptr tvoid)) (tptr (Tstruct _structPQ noattr))))) (Ssequence (Sassign (Efield (Ederef (Etempvar _pq (tptr (Tstruct _structPQ noattr))) (Tstruct _structPQ noattr)) _capacity tuint) (Etempvar _size__1 tuint)) (Ssequence (Sassign (Efield (Ederef (Etempvar _pq (tptr (Tstruct _structPQ noattr))) (Tstruct _structPQ noattr)) _first_available tuint) (Etempvar _size__1 tuint)) (Ssequence (Sassign (Efield (Ederef (Etempvar _pq (tptr (Tstruct _structPQ noattr))) (Tstruct _structPQ noattr)) _heap_cells (tptr (Tstruct _structItem noattr))) (Etempvar _arr (tptr (Tstruct _structItem noattr)))) (Sreturn (Some (Etempvar _pq (tptr (Tstruct _structPQ noattr)))))))))) |}.
imports: Coq(String List ZArith) compcert(Coqlib Integers Floats AST Ctypes Cop Clight Clightdefs)