fact: Definition f_create_space := {| fn_return := tvoid; fn_callconv := cc_default; fn_params := ((_s, (tptr (Tstruct _space noattr))) :: (_n, tulong) :: nil); fn_vars := nil; fn_temps := ((_p, (tptr (talignas 3%N (tptr tvoid)))) :: (_t'1, (tptr tvoid)) :: (_t'2, (tptr (talignas 3%N (tptr tvoid)))) :: nil); fn_body := (Ssequence (Ssequence (Scall (Some _t'1) (Evar _malloc (Tfunction (Tcons tulong Tnil) (tptr tvoid) cc_default)) ((Ebinop Omul (Etempvar _n tulong) (Esizeof (talignas 3%N (tptr tvoid)) tulong) tulong) :: nil)) (Sset _p (Ecast (Etempvar _t'1 (tptr tvoid)) (tptr (talignas 3%N (tptr tvoid)))))) (Ssequence (Sifthenelse (Ebinop Oeq (Etempvar _p (tptr (talignas 3%N (tptr tvoid)))) (Ecast (Econst_int (Int.repr 0) tint) (tptr tvoid)) tint) (Scall None (Evar _abort_with (Tfunction (Tcons (tptr tschar) Tnil) tvoid cc_default)) ((Evar ___stringlit_7 (tarray tschar 38)) :: nil)) Sskip) (Ssequence (Sassign (Efield (Ederef (Etempvar _s (tptr (Tstruct _space noattr))) (Tstruct _space noattr)) _start (tptr (talignas 3%N (tptr tvoid)))) (Etempvar _p (tptr (talignas 3%N (tptr tvoid))))) (Ssequence (Sassign (Efield (Ederef (Etempvar _s (tptr (Tstruct _space noattr))) (Tstruct _space noattr)) _next (tptr (talignas 3%N (tptr tvoid)))) (Etempvar _p (tptr (talignas 3%N (tptr tvoid))))) (Ssequence (Sassign (Efield (Ederef (Etempvar _s (tptr (Tstruct _space noattr))) (Tstruct _space noattr)) _limit (tptr (talignas 3%N (tptr tvoid)))) (Ebinop Oadd (Etempvar _p (tptr (talignas 3%N (tptr tvoid)))) (Etempvar _n tulong) (tptr (talignas 3%N (tptr tvoid))))) (Ssequence (Sset _t'2 (Efield (Ederef (Etempvar _s (tptr (Tstruct _space noattr))) (Tstruct _space noattr)) _limit (tptr (talignas 3%N (tptr tvoid))))) (Sassign (Efield (Ederef (Etempvar _s (tptr (Tstruct _space noattr))) (Tstruct _space noattr)) _rem_limit (tptr (talignas 3%N (tptr tvoid)))) (Etempvar _t'2 (tptr (talignas 3%N (tptr tvoid))))))))))) |}.
imports: Coq(String List ZArith) compcert(Coqlib Integers Floats AST Ctypes Cop Clight Clightdefs)