fact: Definition f_init := {| fn_return := (tptr tint); fn_callconv := cc_default; fn_params := ((_size, tint) :: nil); fn_vars := nil; fn_temps := ((_pq, (tptr tint)) :: (_t'1, (tptr tvoid)) :: nil); fn_body := (Ssequence (Ssequence (Scall (Some _t'1) (Evar _mallocN (Tfunction (Tcons tint Tnil) (tptr tvoid) cc_default)) ((Ebinop Omul (Etempvar _size tint) (Esizeof tint tuint) tuint) :: nil)) (Sset _pq (Etempvar _t'1 (tptr tvoid)))) (Sreturn (Some (Etempvar _pq (tptr tint))))) |}.
imports: Coq(String List ZArith) compcert(Coqlib Integers Floats AST Ctypes Cop Clight Clightdefs)