fact: Definition f_garbage_collect := {| fn_return := tvoid; fn_callconv := cc_default; fn_params := ((_fi, (tptr tuint)) :: (_ti, (tptr (Tstruct _thread_info noattr))) :: nil); fn_vars := nil; fn_temps := ((_h, (tptr (Tstruct _heap noattr))) :: (_i, tint) :: (_w, tint) :: (_t'1, (tptr (Tstruct __reent noattr))) :: (_t'10, (tptr (talignas 2%N (tptr tvoid)))) :: (_t'9, (tptr (talignas 2%N (tptr tvoid)))) :: (_t'8, (tptr (talignas 2%N (tptr tvoid)))) :: (_t'7, (tptr (talignas 2%N (tptr tvoid)))) :: (_t'6, (tptr (Tstruct ___sFILE64 noattr))) :: (_t'5, (tptr (talignas 2%N (tptr tvoid)))) :: (_t'4, (tptr (talignas 2%N (tptr tvoid)))) :: (_t'3, (tptr (talignas 2%N (tptr tvoid)))) :: (_t'2, (tptr (talignas 2%N (tptr tvoid)))) :: nil); fn_body := (Ssequence (Sset _h (Efield (Ederef (Etempvar _ti (tptr (Tstruct _thread_info noattr))) (Tstruct _thread_info noattr)) _heap (tptr (Tstruct _heap noattr)))) (Ssequence (Ssequence (Sset _t'10 (Efield (Ederef (Etempvar _ti (tptr (Tstruct _thread_info noattr))) (Tstruct _thread_info noattr)) _alloc (tptr (talignas 2%N (tptr tvoid))))) (Sassign (Efield (Ederef (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))) (Tstruct _space noattr)) _next (tptr (talignas 2%N (tptr tvoid)))) (Etempvar _t'10 (tptr (talignas 2%N (tptr tvoid)))))) (Ssequence (Ssequence (Sset _i (Econst_int (Int.repr 0) tint)) (Sloop (Ssequence (Sifthenelse (Ebinop Olt (Etempvar _i tint) (Ebinop Osub (Econst_int (Int.repr 12) tint) (Econst_int (Int.repr 1) tint) tint) tint) Sskip Sbreak) (Ssequence (Ssequence (Sset _t'7 (Efield (Ederef (Ebinop Oadd (Efield (Ederef (Etempvar _h (tptr (Tstruct _heap noattr))) (Tstruct _heap noattr)) _spaces (tarray (Tstruct _space noattr) 12)) (Ebinop Oadd (Etempvar _i tint) (Econst_int (Int.repr 1) tint) tint) (tptr (Tstruct _space noattr))) (Tstruct _space noattr)) _start (tptr (talignas 2%N (tptr tvoid))))) (Sifthenelse (Ebinop Oeq (Etempvar _t'7 (tptr (talignas 2%N (tptr tvoid)))) (Ecast (Econst_int (Int.repr 0) tint) (tptr tvoid)) tint) (Ssequence (Ssequence (Sset _t'8 (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))))) (Ssequence (Sset _t'9 (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))))) (Sset _w (Ebinop Osub (Etempvar _t'8 (tptr (talignas 2%N (tptr tvoid)))) (Etempvar _t'9 (tptr (talignas 2%N (tptr tvoid)))) tint)))) (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)) (Ebinop Oadd (Etempvar _i tint) (Econst_int (Int.repr 1) tint) tint) (tptr (Tstruct _space noattr))) :: (Ebinop Omul (Econst_int (Int.repr 2) tint) (Etempvar _w tint) tint) :: nil))) Sskip)) (Ssequence (Sifthenelse (Econst_int (Int.repr 0) tint) (Ssequence (Scall (Some _t'1) (Evar ___getreent (Tfunction Tnil (tptr (Tstruct __reent noattr)) cc_default)) nil) (Ssequence (Sset _t'6 (Efield (Ederef (Etempvar _t'1 (tptr (Tstruct __reent noattr))) (Tstruct __reent noattr)) __stderr (tptr (Tstruct ___sFILE64 noattr)))) (Scall None (Evar _fprintf (Tfunction (Tcons (tptr (Tstruct ___sFILE64 noattr)) (Tcons (tptr tschar) Tnil)) tint {|cc_vararg:=(Some 2); cc_unproto:=false; cc_structret:=false|})) ((Etempvar _t'6 (tptr (Tstruct ___sFILE64 noattr))) :: (Evar ___stringlit_11 (tarray tschar 17)) :: (Etempvar _i tint) :: nil)))) Sskip) (Ssequence (Scall None (Evar _do_generation (Tfunction (Tcons (tptr (Tstruct _space noattr)) (Tcons (tptr (Tstruct _space noattr)) (Tcons (tptr tuint) (Tcons (tptr (Tstruct _thread_info noattr)) Tnil)))) tvoid cc_default)) ((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))) :: (Ebinop Oadd (Efield (Ederef (Etempvar _h (tptr (Tstruct _heap noattr))) (Tstruct _heap noattr)) _spaces (tarray (Tstruct _space noattr) 12)) (Ebinop Oadd (Etempvar _i tint) (Econst_int (Int.repr 1) tint) tint) (tptr (Tstruct _space noattr))) :: (Etempvar _fi (tptr tuint)) :: (Etempvar _ti (tptr (Tstruct _thread_info noattr))) :: nil)) (Ssequence (Sset _t'2 (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))))) (Ssequence (Sset _t'3 (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))))) (Ssequence (Sset _t'4 (Efield (Ederef (Ebinop Oadd (Efield (Ederef (Etempvar _h (tptr (Tstruct _heap noattr))) (Tstruct _heap noattr)) _spaces (tarray (Tstruct _space noattr) 12)) (Ebinop Oadd (Etempvar _i tint) (Econst_int (Int.repr 1) tint) tint) (tptr (Tstruct _space noattr))) (Tstruct _space noattr)) _limit (tptr (talignas 2%N (tptr tvoid))))) (Ssequence (Sset _t'5 (Efield (Ederef (Ebinop Oadd (Efield (Ederef (Etempvar _h (tptr (Tstruct _heap noattr))) (Tstruct _heap noattr)) _spaces (tarray (Tstruct _space noattr) 12)) (Ebinop Oadd (Etempvar _i tint) (Econst_int (Int.repr 1) tint) tint) (tptr (Tstruct _space noattr))) (Tstruct _space noattr)) _next (tptr (talignas 2%N (tptr tvoid))))) (Sifthenelse (Ebinop Ole (Ebinop Osub (Etempvar _t'2 (tptr (talignas 2%N (tptr tvoid)))) (Etempvar _t'3 (tptr (talignas 2%N (tptr tvoid)))) tint) (Ebinop Osub (Etempvar _t'4 (tptr (talignas 2%N (tptr tvoid)))) (Etempvar _t'5 (tptr (talignas 2%N (tptr tvoid)))) tint) tint) (Ssequence (Scall None (Evar _resume (Tfunction (Tcons (tptr tuint) (Tcons (tptr (Tstruct _thread_info noattr)) Tnil)) tvoid cc_default)) ((Etempvar _fi (tptr tuint)) :: (Etempvar _ti (tptr (Tstruct _thread_info noattr))) :: nil)) (Sreturn None)) Sskip))))))))) (Sset _i (Ebinop Oadd (Etempvar _i tint) (Econst_int (Int.repr 1) tint) tint)))) (Ssequence (Scall None (Evar _abort_with (Tfunction (Tcons (tptr tschar) Tnil) tvoid cc_default)) ((Evar ___stringlit_12 (tarray tschar 24)) :: nil)) (Scall None (Evar ___assert_func (Tfunction (Tcons (tptr tschar) (Tcons tint (Tcons (tptr tschar) (Tcons (tptr tschar) Tnil)))) tvoid cc_default)) ((Evar ___stringlit_2 (tarray tschar 13)) :: (Econst_int (Int.repr 386) tint) :: (Ecast (Econst_int (Int.repr 0) tint) (tptr tvoid)) :: (Evar ___stringlit_13 (tarray tschar 2)) :: nil)))))) |}.
imports: Coq(String List ZArith) compcert(Coqlib Integers Floats AST Ctypes Cop Clight Clightdefs)