fact: Definition f_pq_remove_min := {| fn_return := (tptr (Tstruct _structItem noattr)); fn_callconv := cc_default; fn_params := ((_pq, (tptr (Tstruct _structPQ noattr))) :: nil); fn_vars := nil; fn_temps := ((_item, (tptr (Tstruct _structItem noattr))) :: (_t'1, (tptr tvoid)) :: (_t'2, tuint) :: nil); fn_body := (Ssequence (Ssequence (Sset _t'2 (Efield (Ederef (Etempvar _pq (tptr (Tstruct _structPQ noattr))) (Tstruct _structPQ noattr)) _first_available tuint)) (Sifthenelse (Ebinop Oeq (Etempvar _t'2 tuint) (Econst_int (Int.repr 0) tuint) tint) (Sreturn (Some (Econst_int (Int.repr 0) tint))) Sskip)) (Ssequence (Ssequence (Scall (Some _t'1) (Evar _malloc (Tfunction (Tcons tulong Tnil) (tptr tvoid) cc_default)) ((Esizeof (Tstruct _structItem noattr) tulong) :: nil)) (Sset _item (Ecast (Etempvar _t'1 (tptr tvoid)) (tptr (Tstruct _structItem noattr))))) (Ssequence (Scall None (Evar _pq_remove_min_nc (Tfunction (Tcons (tptr (Tstruct _structPQ noattr)) (Tcons (tptr (Tstruct _structItem noattr)) Tnil)) tvoid cc_default)) ((Etempvar _pq (tptr (Tstruct _structPQ noattr))) :: (Etempvar _item (tptr (Tstruct _structItem noattr))) :: nil)) (Sreturn (Some (Etempvar _item (tptr (Tstruct _structItem noattr)))))))) |}.
imports: Coq(String List ZArith) compcert(Coqlib Integers Floats AST Ctypes Cop Clight Clightdefs)