fact: Definition f_pq_insert_nc := {| fn_return := tuint; fn_callconv := cc_default; fn_params := ((_pq, (tptr (Tstruct _structPQ noattr))) :: (_priority, tint) :: (_data, tint) :: nil); fn_vars := nil; fn_temps := ((_fa, tuint) :: (_cells, (tptr (Tstruct _structItem noattr))) :: (_key, tuint) :: (_t'1, (tptr tuint)) :: nil); fn_body := (Ssequence (Sset _fa (Efield (Ederef (Etempvar _pq (tptr (Tstruct _structPQ noattr))) (Tstruct _structPQ noattr)) _first_available tuint)) (Ssequence (Sset _cells (Efield (Ederef (Etempvar _pq (tptr (Tstruct _structPQ noattr))) (Tstruct _structPQ noattr)) _heap_cells (tptr (Tstruct _structItem noattr)))) (Ssequence (Sset _key (Efield (Ederef (Ebinop Oadd (Etempvar _cells (tptr (Tstruct _structItem noattr))) (Etempvar _fa tuint) (tptr (Tstruct _structItem noattr))) (Tstruct _structItem noattr)) _key tuint)) (Ssequence (Sassign (Efield (Ederef (Ebinop Oadd (Etempvar _cells (tptr (Tstruct _structItem noattr))) (Etempvar _fa tuint) (tptr (Tstruct _structItem noattr))) (Tstruct _structItem noattr)) _priority tint) (Etempvar _priority tint)) (Ssequence (Sassign (Efield (Ederef (Ebinop Oadd (Etempvar _cells (tptr (Tstruct _structItem noattr))) (Etempvar _fa tuint) (tptr (Tstruct _structItem noattr))) (Tstruct _structItem noattr)) _data tint) (Etempvar _data tint)) (Ssequence (Ssequence (Sset _t'1 (Efield (Ederef (Etempvar _pq (tptr (Tstruct _structPQ noattr))) (Tstruct _structPQ noattr)) _key_table (tptr tuint))) (Scall None (Evar _swim (Tfunction (Tcons tuint (Tcons (tptr (Tstruct _structItem noattr)) (Tcons (tptr tuint) Tnil))) tvoid cc_default)) ((Etempvar _fa tuint) :: (Etempvar _cells (tptr (Tstruct _structItem noattr))) :: (Etempvar _t'1 (tptr tuint)) :: nil))) (Ssequence (Sassign (Efield (Ederef (Etempvar _pq (tptr (Tstruct _structPQ noattr))) (Tstruct _structPQ noattr)) _first_available tuint) (Ebinop Oadd (Etempvar _fa tuint) (Econst_int (Int.repr 1) tint) tuint)) (Sreturn (Some (Etempvar _key tuint)))))))))) |}.
imports: Coq(String List ZArith) compcert(Coqlib Integers Floats AST Ctypes Cop Clight Clightdefs)