fact: Definition f_free_heap := {| fn_return := tvoid; fn_callconv := cc_default; fn_params := ((_h, (tptr (Tstruct _heap noattr))) :: nil); fn_vars := nil; fn_temps := ((_i, tint) :: (_p, (tptr (talignas 3%N (tptr tvoid)))) :: (_t'1, (tptr (Tstruct ___sFILE noattr))) :: nil); fn_body := (Ssequence (Ssequence (Sset _t'1 (Evar ___stderrp (tptr (Tstruct ___sFILE noattr)))) (Scall None (Evar _fprintf (Tfunction (Tcons (tptr (Tstruct ___sFILE noattr)) (Tcons (tptr tschar) Tnil)) tint {|cc_vararg:=(Some 2); cc_unproto:=false; cc_structret:=false|})) ((Etempvar _t'1 (tptr (Tstruct ___sFILE noattr))) :: (Evar ___stringlit_16 (tarray tschar 21)) :: nil))) (Ssequence (Ssequence (Sset _i (Econst_int (Int.repr 0) tint)) (Sloop (Ssequence (Sifthenelse (Ebinop Olt (Etempvar _i tint) (Ebinop Osub (Ebinop Omul (Econst_int (Int.repr 8) tint) (Esizeof (talignas 3%N (tptr tvoid)) tulong) tulong) (Ebinop Oadd (Econst_int (Int.repr 3) tint) (Econst_int (Int.repr 16) tint) tint) tulong) tint) Sskip Sbreak) (Ssequence (Sset _p (Efield (Ederef (Ebinop Oadd (Efield (Ederef (Etempvar _h (tptr (Tstruct _heap noattr))) (Tstruct _heap noattr)) _spaces (tarray (Tstruct _space noattr) 45)) (Etempvar _i tint) (tptr (Tstruct _space noattr))) (Tstruct _space noattr)) _start (tptr (talignas 3%N (tptr tvoid))))) (Sifthenelse (Ebinop One (Etempvar _p (tptr (talignas 3%N (tptr tvoid)))) (Ecast (Econst_int (Int.repr 0) tint) (tptr tvoid)) tint) (Scall None (Evar _free (Tfunction (Tcons (tptr tvoid) Tnil) tvoid cc_default)) ((Etempvar _p (tptr (talignas 3%N (tptr tvoid)))) :: nil)) Sskip))) (Sset _i (Ebinop Oadd (Etempvar _i tint) (Econst_int (Int.repr 1) tint) tint)))) (Scall None (Evar _free (Tfunction (Tcons (tptr tvoid) Tnil) tvoid cc_default)) ((Etempvar _h (tptr (Tstruct _heap noattr))) :: nil)))) |}.
imports: Coq(String List ZArith) compcert(Coqlib Integers Floats AST Ctypes Cop Clight Clightdefs)