fact: Definition f_export := {| fn_return := (tptr tvoid); fn_callconv := cc_default; fn_params := ((_ti, (tptr (Tstruct _thread_info noattr))) :: (_root, (talignas 3%N (tptr tvoid))) :: nil); fn_vars := ((_frame, (Tstruct _stack_frame noattr)) :: (_roots, (tarray (talignas 3%N (tptr tvoid)) 1)) :: nil); fn_temps := ((_gen_level, tint) :: (_sp, (tptr (Tstruct _space noattr))) :: (_fake_sp, (tptr (Tstruct _space noattr))) :: (_value_sp, (tptr (Tstruct _space noattr))) :: (_result_block, (tptr tvoid)) :: (_t'4, (tptr tvoid)) :: (_t'3, (tptr tvoid)) :: (_t'2, tint) :: (_t'1, tint) :: (_t'11, (tptr (Tstruct _heap noattr))) :: (_t'10, (tptr (talignas 3%N (tptr tvoid)))) :: (_t'9, (tptr (talignas 3%N (tptr tvoid)))) :: (_t'8, (tptr (talignas 3%N (tptr tvoid)))) :: (_t'7, (tptr (talignas 3%N (tptr tvoid)))) :: (_t'6, (tptr (talignas 3%N (tptr tvoid)))) :: (_t'5, (tptr (talignas 3%N (tptr tvoid)))) :: nil); fn_body := (Ssequence (Sassign (Ederef (Ebinop Oadd (Evar _roots (tarray (talignas 3%N (tptr tvoid)) 1)) (Econst_int (Int.repr 0) tint) (tptr (talignas 3%N (tptr tvoid)))) (talignas 3%N (tptr tvoid))) (Etempvar _root (talignas 3%N (tptr tvoid)))) (Ssequence (Sassign (Efield (Evar _frame (Tstruct _stack_frame noattr)) _root (tptr (talignas 3%N (tptr tvoid)))) (Evar _roots (tarray (talignas 3%N (tptr tvoid)) 1))) (Ssequence (Sassign (Efield (Evar _frame (Tstruct _stack_frame noattr)) _next (tptr (talignas 3%N (tptr tvoid)))) (Ebinop Oadd (Evar _roots (tarray (talignas 3%N (tptr tvoid)) 1)) (Econst_int (Int.repr 1) tint) (tptr (talignas 3%N (tptr tvoid))))) (Ssequence (Sassign (Efield (Evar _frame (Tstruct _stack_frame noattr)) _prev (tptr (Tstruct _stack_frame noattr))) (Ecast (Econst_int (Int.repr 0) tint) (tptr tvoid))) (Ssequence (Sassign (Efield (Ederef (Etempvar _ti (tptr (Tstruct _thread_info noattr))) (Tstruct _thread_info noattr)) _fp (tptr (Tstruct _stack_frame noattr))) (Eaddrof (Evar _frame (Tstruct _stack_frame noattr)) (tptr (Tstruct _stack_frame noattr)))) (Ssequence (Ssequence (Scall (Some _t'1) (Evar _Is_block (Tfunction (Tcons (talignas 3%N (tptr tvoid)) Tnil) tint cc_default)) ((Etempvar _root (talignas 3%N (tptr tvoid))) :: nil)) (Sifthenelse (Eunop Onotbool (Etempvar _t'1 tint) tint) (Sreturn (Some (Ecast (Etempvar _root (talignas 3%N (tptr tvoid))) (tptr tvoid)))) Sskip)) (Ssequence (Ssequence (Scall (Some _t'2) (Evar _garbage_collect_all (Tfunction (Tcons (tptr (Tstruct _thread_info noattr)) Tnil) tint cc_default)) ((Etempvar _ti (tptr (Tstruct _thread_info noattr))) :: nil)) (Sset _gen_level (Etempvar _t'2 tint))) (Ssequence (Ssequence (Sset _t'11 (Efield (Ederef (Etempvar _ti (tptr (Tstruct _thread_info noattr))) (Tstruct _thread_info noattr)) _heap (tptr (Tstruct _heap noattr)))) (Sset _sp (Ebinop Oadd (Efield (Ederef (Etempvar _t'11 (tptr (Tstruct _heap noattr))) (Tstruct _heap noattr)) _spaces (tarray (Tstruct _space noattr) 45)) (Etempvar _gen_level tint) (tptr (Tstruct _space noattr))))) (Ssequence (Ssequence (Scall (Some _t'3) (Evar _malloc (Tfunction (Tcons tulong Tnil) (tptr tvoid) cc_default)) ((Esizeof (Tstruct _space noattr) tulong) :: nil)) (Sset _fake_sp (Ecast (Etempvar _t'3 (tptr tvoid)) (tptr (Tstruct _space noattr))))) (Ssequence (Ssequence (Sset _t'9 (Efield (Ederef (Etempvar _sp (tptr (Tstruct _space noattr))) (Tstruct _space noattr)) _next (tptr (talignas 3%N (tptr tvoid))))) (Ssequence (Sset _t'10 (Efield (Ederef (Etempvar _sp (tptr (Tstruct _space noattr))) (Tstruct _space noattr)) _start (tptr (talignas 3%N (tptr tvoid))))) (Scall None (Evar _create_space (Tfunction (Tcons (tptr (Tstruct _space noattr)) (Tcons tulong Tnil)) tvoid cc_default)) ((Etempvar _fake_sp (tptr (Tstruct _space noattr))) :: (Ebinop Osub (Etempvar _t'9 (tptr (talignas 3%N (tptr tvoid)))) (Etempvar _t'10 (tptr (talignas 3%N (tptr tvoid)))) tlong) :: nil)))) (Ssequence (Scall None (Evar _do_generation (Tfunction (Tcons (tptr (Tstruct _space noattr)) (Tcons (tptr (Tstruct _space noattr)) (Tcons (tptr (Tstruct _thread_info noattr)) Tnil))) tvoid cc_default)) ((Etempvar _sp (tptr (Tstruct _space noattr))) :: (Etempvar _fake_sp (tptr (Tstruct _space noattr))) :: (Etempvar _ti (tptr (Tstruct _thread_info noattr))) :: nil)) (Ssequence (Ssequence (Scall (Some _t'4) (Evar _malloc (Tfunction (Tcons tulong Tnil) (tptr tvoid) cc_default)) ((Esizeof (Tstruct _space noattr) tulong) :: nil)) (Sset _value_sp (Ecast (Etempvar _t'4 (tptr tvoid)) (tptr (Tstruct _space noattr))))) (Ssequence (Ssequence (Sset _t'7 (Efield (Ederef (Etempvar _fake_sp (tptr (Tstruct _space noattr))) (Tstruct _space noattr)) _next (tptr (talignas 3%N (tptr tvoid))))) (Ssequence (Sset _t'8 (Efield (Ederef (Etempvar _fake_sp (tptr (Tstruct _space noattr))) (Tstruct _space noattr)) _start (tptr (talignas 3%N (tptr tvoid))))) (Scall None (Evar _create_space (Tfunction (Tcons (tptr (Tstruct _space noattr)) (Tcons tulong Tnil)) tvoid cc_default)) ((Etempvar _value_sp (tptr (Tstruct _space noattr))) :: (Ebinop Osub (Etempvar _t'7 (tptr (talignas 3%N (tptr tvoid)))) (Etempvar _t'8 (tptr (talignas 3%N (tptr tvoid)))) tlong) :: nil)))) (Ssequence (Scall None (Evar _do_generation (Tfunction (Tcons (tptr (Tstruct _space noattr)) (Tcons (tptr (Tstruct _space noattr)) (Tcons (tptr (Tstruct _thread_info noattr)) Tnil))) tvoid cc_default)) ((Etempvar _fake_sp (tptr (Tstruct _space noattr))) :: (Etempvar _value_sp (tptr (Tstruct _space noattr))) :: (Etempvar _ti (tptr (Tstruct _thread_info noattr))) :: nil)) (Ssequence (Ssequence (Sset _t'6 (Efield (Ederef (Etempvar _value_sp (tptr (Tstruct _space noattr))) (Tstruct _space noattr)) _start (tptr (talignas 3%N (tptr tvoid))))) (Sset _result_block (Ecast (Ebinop Oadd (Etempvar _t'6 (tptr (talignas 3%N (tptr tvoid)))) (Econst_int (Int.repr 1) tint) (tptr (talignas 3%N (tptr tvoid)))) (tptr tvoid)))) (Ssequence (Ssequence (Sset _t'5 (Efield (Ederef (Etempvar _fake_sp (tptr (Tstruct _space noattr))) (Tstruct _space noattr)) _start (tptr (talignas 3%N (tptr tvoid))))) (Scall None (Evar _free (Tfunction (Tcons (tptr tvoid) Tnil) tvoid cc_default)) ((Etempvar _t'5 (tptr (talignas 3%N (tptr tvoid)))) :: nil))) (Ssequence (Scall None (Evar _free (Tfunction (Tcons (tptr tvoid) Tnil) tvoid cc_default)) ((Etempvar _fake_sp (tptr (Tstruct _space noattr))) :: nil)) (Ssequence (Scall None (Evar _free (Tfunction (Tcons (tptr tvoid) Tnil) tvoid cc_default)) ((Etempvar _value_sp (tptr (Tstruct _space noattr))) :: nil)) (Sreturn (Some (Etempvar _result_block (tptr tvoid)))))))))))))))))))))) |}.
imports: Coq(String List ZArith) compcert(Coqlib Integers Floats AST Ctypes Cop Clight Clightdefs)