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