fact: Definition f_garbage_collect_all := {| fn_return := tint; fn_callconv := cc_default; fn_params := ((_ti, (tptr (Tstruct _thread_info noattr))) :: nil); fn_vars := nil; fn_temps := ((_h, (tptr (Tstruct _heap noattr))) :: (_i, tint) :: (_t'2, tint) :: (_t'1, (tptr (Tstruct _heap noattr))) :: (_t'6, (tptr (talignas 3%N (tptr tvoid)))) :: (_t'5, (tptr (talignas 3%N (tptr tvoid)))) :: (_t'4, (tptr (talignas 3%N (tptr tvoid)))) :: (_t'3, (tptr (Tstruct _stack_frame noattr))) :: 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 (Sifthenelse (Ebinop Oeq (Etempvar _h (tptr (Tstruct _heap noattr))) (Ecast (Econst_int (Int.repr 0) tint) (tptr tvoid)) tint) (Ssequence (Ssequence (Scall (Some _t'1) (Evar _create_heap (Tfunction Tnil (tptr (Tstruct _heap noattr)) cc_default)) nil) (Sset _h (Etempvar _t'1 (tptr (Tstruct _heap noattr))))) (Sassign (Efield (Ederef (Etempvar _ti (tptr (Tstruct _thread_info noattr))) (Tstruct _thread_info noattr)) _heap (tptr (Tstruct _heap noattr))) (Etempvar _h (tptr (Tstruct _heap noattr))))) Sskip) (Ssequence (Ssequence (Sset _t'6 (Efield (Ederef (Etempvar _ti (tptr (Tstruct _thread_info noattr))) (Tstruct _thread_info noattr)) _limit (tptr (talignas 3%N (tptr tvoid))))) (Sassign (Efield (Ederef (Ebinop Oadd (Efield (Ederef (Etempvar _h (tptr (Tstruct _heap noattr))) (Tstruct _heap noattr)) _spaces (tarray (Tstruct _space noattr) 43)) (Econst_int (Int.repr 0) tint) (tptr (Tstruct _space noattr))) (Tstruct _space noattr)) _limit (tptr (talignas 3%N (tptr tvoid)))) (Etempvar _t'6 (tptr (talignas 3%N (tptr tvoid)))))) (Ssequence (Ssequence (Sset _t'5 (Efield (Ederef (Etempvar _ti (tptr (Tstruct _thread_info noattr))) (Tstruct _thread_info noattr)) _alloc (tptr (talignas 3%N (tptr tvoid))))) (Sassign (Efield (Ederef (Ebinop Oadd (Efield (Ederef (Etempvar _h (tptr (Tstruct _heap noattr))) (Tstruct _heap noattr)) _spaces (tarray (Tstruct _space noattr) 43)) (Econst_int (Int.repr 0) tint) (tptr (Tstruct _space noattr))) (Tstruct _space noattr)) _next (tptr (talignas 3%N (tptr tvoid)))) (Etempvar _t'5 (tptr (talignas 3%N (tptr tvoid)))))) (Ssequence (Ssequence (Sset _i (Econst_int (Int.repr 0) tint)) (Sloop (Ssequence (Ssequence (Sifthenelse (Ebinop Olt (Etempvar _i tint) (Ebinop Osub (Ebinop Osub (Ebinop Omul (Econst_int (Int.repr 8) tint) (Esizeof (talignas 3%N (tptr tvoid)) tulong) tulong) (Ebinop Oadd (Ebinop Oadd (Econst_int (Int.repr 2) tint) (Econst_int (Int.repr 3) tint) tint) (Econst_int (Int.repr 16) tint) tint) tulong) (Econst_int (Int.repr 1) tint) tulong) tint) (Ssequence (Sset _t'4 (Efield (Ederef (Ebinop Oadd (Efield (Ederef (Etempvar _h (tptr (Tstruct _heap noattr))) (Tstruct _heap noattr)) _spaces (tarray (Tstruct _space noattr) 43)) (Ebinop Oadd (Etempvar _i tint) (Econst_int (Int.repr 1) tint) tint) (tptr (Tstruct _space noattr))) (Tstruct _space noattr)) _start (tptr (talignas 3%N (tptr tvoid))))) (Sset _t'2 (Ecast (Ebinop One (Etempvar _t'4 (tptr (talignas 3%N (tptr tvoid)))) (Ecast (Econst_int (Int.repr 0) tint) (tptr tvoid)) tint) tbool))) (Sset _t'2 (Econst_int (Int.repr 0) tint))) (Sifthenelse (Etempvar _t'2 tint) Sskip Sbreak)) (Ssequence (Sset _t'3 (Efield (Ederef (Etempvar _ti (tptr (Tstruct _thread_info noattr))) (Tstruct _thread_info noattr)) _fp (tptr (Tstruct _stack_frame noattr)))) (Scall None (Evar _do_generation (Tfunction (Tcons (tptr (Tstruct _space noattr)) (Tcons (tptr (Tstruct _space noattr)) (Tcons (tptr (Tstruct _stack_frame noattr)) Tnil))) tvoid cc_default)) ((Ebinop Oadd (Efield (Ederef (Etempvar _h (tptr (Tstruct _heap noattr))) (Tstruct _heap noattr)) _spaces (tarray (Tstruct _space noattr) 43)) (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) 43)) (Ebinop Oadd (Etempvar _i tint) (Econst_int (Int.repr 1) tint) tint) (tptr (Tstruct _space noattr))) :: (Etempvar _t'3 (tptr (Tstruct _stack_frame noattr))) :: nil)))) (Sset _i (Ebinop Oadd (Etempvar _i tint) (Econst_int (Int.repr 1) tint) tint)))) (Sreturn (Some (Etempvar _i tint)))))))) |}.
imports: Coq(String List ZArith) compcert(Coqlib Integers Floats AST Ctypes Cop Clight Clightdefs)