fact: Definition f_create_heap := {| fn_return := (tptr (Tstruct _heap noattr)); fn_callconv := cc_default; fn_params := nil; fn_vars := nil; fn_temps := ((_i, tint) :: (_h, (tptr (Tstruct _heap noattr))) :: (_t'1, (tptr tvoid)) :: nil); fn_body := (Ssequence (Ssequence (Scall (Some _t'1) (Evar _malloc (Tfunction (Tcons tuint Tnil) (tptr tvoid) cc_default)) ((Esizeof (Tstruct _heap noattr) tuint) :: nil)) (Sset _h (Ecast (Etempvar _t'1 (tptr tvoid)) (tptr (Tstruct _heap noattr))))) (Ssequence (Sifthenelse (Ebinop Oeq (Etempvar _h (tptr (Tstruct _heap noattr))) (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 27)) :: nil)) Sskip) (Ssequence (Scall None (Evar _create_space (Tfunction (Tcons (tptr (Tstruct _space noattr)) (Tcons tuint Tnil)) tvoid cc_default)) ((Ebinop Oadd (Efield (Ederef (Etempvar _h (tptr (Tstruct _heap noattr))) (Tstruct _heap noattr)) _spaces (tarray (Tstruct _space noattr) 12)) (Econst_int (Int.repr 0) tint) (tptr (Tstruct _space noattr))) :: (Ebinop Oshl (Econst_int (Int.repr 1) tint) (Econst_int (Int.repr 16) tint) tint) :: nil)) (Ssequence (Ssequence (Sset _i (Econst_int (Int.repr 1) tint)) (Sloop (Ssequence (Sifthenelse (Ebinop Olt (Etempvar _i tint) (Econst_int (Int.repr 12) tint) tint) Sskip Sbreak) (Ssequence (Sassign (Efield (Ederef (Ebinop Oadd (Efield (Ederef (Etempvar _h (tptr (Tstruct _heap noattr))) (Tstruct _heap noattr)) _spaces (tarray (Tstruct _space noattr) 12)) (Etempvar _i tint) (tptr (Tstruct _space noattr))) (Tstruct _space noattr)) _start (tptr (talignas 2%N (tptr tvoid)))) (Ecast (Econst_int (Int.repr 0) tint) (tptr tvoid))) (Ssequence (Sassign (Efield (Ederef (Ebinop Oadd (Efield (Ederef (Etempvar _h (tptr (Tstruct _heap noattr))) (Tstruct _heap noattr)) _spaces (tarray (Tstruct _space noattr) 12)) (Etempvar _i tint) (tptr (Tstruct _space noattr))) (Tstruct _space noattr)) _next (tptr (talignas 2%N (tptr tvoid)))) (Ecast (Econst_int (Int.repr 0) tint) (tptr tvoid))) (Sassign (Efield (Ederef (Ebinop Oadd (Efield (Ederef (Etempvar _h (tptr (Tstruct _heap noattr))) (Tstruct _heap noattr)) _spaces (tarray (Tstruct _space noattr) 12)) (Etempvar _i tint) (tptr (Tstruct _space noattr))) (Tstruct _space noattr)) _limit (tptr (talignas 2%N (tptr tvoid)))) (Ecast (Econst_int (Int.repr 0) tint) (tptr tvoid)))))) (Sset _i (Ebinop Oadd (Etempvar _i tint) (Econst_int (Int.repr 1) tint) tint)))) (Sreturn (Some (Etempvar _h (tptr (Tstruct _heap noattr))))))))) |}.
imports: Coq(String List ZArith) compcert(Coqlib Integers Floats AST Ctypes Cop Clight Clightdefs)