fact: Definition f_pq_make := {| fn_return := (tptr (Tstruct _structPQ noattr)); fn_callconv := cc_default; fn_params := ((_size, tuint) :: nil); fn_vars := nil; fn_temps := ((_pq, (tptr (Tstruct _structPQ noattr))) :: (_table, (tptr tuint)) :: (_arr, (tptr (Tstruct _structItem noattr))) :: (_i, tint) :: (_t'3, (tptr tvoid)) :: (_t'2, (tptr tvoid)) :: (_t'1, (tptr tvoid)) :: nil); fn_body := (Ssequence (Ssequence (Scall (Some _t'1) (Evar _mallocN (Tfunction (Tcons tint Tnil) (tptr tvoid) cc_default)) ((Esizeof (Tstruct _structPQ noattr) tulong) :: nil)) (Sset _pq (Ecast (Etempvar _t'1 (tptr tvoid)) (tptr (Tstruct _structPQ noattr))))) (Ssequence (Ssequence (Scall (Some _t'2) (Evar _mallocN (Tfunction (Tcons tint Tnil) (tptr tvoid) cc_default)) ((Ebinop Omul (Esizeof tuint tulong) (Etempvar _size tuint) tulong) :: nil)) (Sset _table (Ecast (Etempvar _t'2 (tptr tvoid)) (tptr tuint)))) (Ssequence (Ssequence (Scall (Some _t'3) (Evar _mallocN (Tfunction (Tcons tint Tnil) (tptr tvoid) cc_default)) ((Ebinop Omul (Esizeof (Tstruct _structItem noattr) tulong) (Etempvar _size tuint) tulong) :: nil)) (Sset _arr (Ecast (Etempvar _t'3 (tptr tvoid)) (tptr (Tstruct _structItem noattr))))) (Ssequence (Ssequence (Sset _i (Econst_int (Int.repr 0) tint)) (Sloop (Ssequence (Sifthenelse (Ebinop Olt (Etempvar _i tint) (Etempvar _size tuint) tint) Sskip Sbreak) (Ssequence (Sassign (Efield (Ederef (Ebinop Oadd (Etempvar _arr (tptr (Tstruct _structItem noattr))) (Etempvar _i tint) (tptr (Tstruct _structItem noattr))) (Tstruct _structItem noattr)) _key tuint) (Etempvar _i tint)) (Ssequence (Sassign (Efield (Ederef (Ebinop Oadd (Etempvar _arr (tptr (Tstruct _structItem noattr))) (Etempvar _i tint) (tptr (Tstruct _structItem noattr))) (Tstruct _structItem noattr)) _priority tint) (Econst_int (Int.repr 0) tint)) (Ssequence (Sassign (Efield (Ederef (Ebinop Oadd (Etempvar _arr (tptr (Tstruct _structItem noattr))) (Etempvar _i tint) (tptr (Tstruct _structItem noattr))) (Tstruct _structItem noattr)) _data tint) (Econst_int (Int.repr 0) tint)) (Sassign (Ederef (Ebinop Oadd (Etempvar _table (tptr tuint)) (Etempvar _i tint) (tptr tuint)) tuint) (Etempvar _i tint)))))) (Sset _i (Ebinop Oadd (Etempvar _i tint) (Econst_int (Int.repr 1) tint) tint)))) (Ssequence (Sassign (Efield (Ederef (Etempvar _pq (tptr (Tstruct _structPQ noattr))) (Tstruct _structPQ noattr)) _capacity tuint) (Etempvar _size tuint)) (Ssequence (Sassign (Efield (Ederef (Etempvar _pq (tptr (Tstruct _structPQ noattr))) (Tstruct _structPQ noattr)) _first_available tuint) (Econst_int (Int.repr 0) tint)) (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)))) (Ssequence (Sassign (Efield (Ederef (Etempvar _pq (tptr (Tstruct _structPQ noattr))) (Tstruct _structPQ noattr)) _key_table (tptr tuint)) (Etempvar _table (tptr tuint))) (Sreturn (Some (Etempvar _pq (tptr (Tstruct _structPQ noattr))))))))))))) |}.
imports: Coq(String List ZArith) compcert(Coqlib Integers Floats AST Ctypes Cop Clight Clightdefs)