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