fact: Definition f_forward_roots := {| fn_return := tvoid; fn_callconv := cc_default; fn_params := ((_from_start, (tptr (talignas 3%N (tptr tvoid)))) :: (_from_limit, (tptr (talignas 3%N (tptr tvoid)))) :: (_next, (tptr (tptr (talignas 3%N (tptr tvoid))))) :: (_ti, (tptr (Tstruct _thread_info noattr))) :: nil); fn_vars := nil; fn_temps := ((_frame, (tptr (Tstruct _stack_frame noattr))) :: (_curr, (tptr (talignas 3%N (tptr tvoid)))) :: (_limit, (tptr (talignas 3%N (tptr tvoid)))) :: nil); fn_body := (Ssequence (Sset _frame (Efield (Ederef (Etempvar _ti (tptr (Tstruct _thread_info noattr))) (Tstruct _thread_info noattr)) _fp (tptr (Tstruct _stack_frame noattr)))) (Swhile (Ebinop One (Etempvar _frame (tptr (Tstruct _stack_frame noattr))) (Ecast (Econst_int (Int.repr 0) tint) (tptr tvoid)) tint) (Ssequence (Sset _curr (Efield (Ederef (Etempvar _frame (tptr (Tstruct _stack_frame noattr))) (Tstruct _stack_frame noattr)) _root (tptr (talignas 3%N (tptr tvoid))))) (Ssequence (Sset _limit (Efield (Ederef (Etempvar _frame (tptr (Tstruct _stack_frame noattr))) (Tstruct _stack_frame noattr)) _next (tptr (talignas 3%N (tptr tvoid))))) (Ssequence (Ssequence (Sset _curr (Efield (Ederef (Etempvar _frame (tptr (Tstruct _stack_frame noattr))) (Tstruct _stack_frame noattr)) _root (tptr (talignas 3%N (tptr tvoid))))) (Sloop (Ssequence (Sifthenelse (Ebinop Olt (Etempvar _curr (tptr (talignas 3%N (tptr tvoid)))) (Etempvar _limit (tptr (talignas 3%N (tptr tvoid)))) tint) Sskip Sbreak) (Scall None (Evar _forward (Tfunction (Tcons (tptr (talignas 3%N (tptr tvoid))) (Tcons (tptr (talignas 3%N (tptr tvoid))) (Tcons (tptr (tptr (talignas 3%N (tptr tvoid)))) (Tcons (tptr (talignas 3%N (tptr tvoid))) (Tcons tint Tnil))))) tvoid cc_default)) ((Etempvar _from_start (tptr (talignas 3%N (tptr tvoid)))) :: (Etempvar _from_limit (tptr (talignas 3%N (tptr tvoid)))) :: (Etempvar _next (tptr (tptr (talignas 3%N (tptr tvoid))))) :: (Etempvar _curr (tptr (talignas 3%N (tptr tvoid)))) :: (Econst_int (Int.repr 0) tint) :: nil))) (Sset _curr (Ebinop Oadd (Etempvar _curr (tptr (talignas 3%N (tptr tvoid)))) (Econst_int (Int.repr 1) tint) (tptr (talignas 3%N (tptr tvoid))))))) (Sset _frame (Efield (Ederef (Etempvar _frame (tptr (Tstruct _stack_frame noattr))) (Tstruct _stack_frame noattr)) _prev (tptr (Tstruct _stack_frame noattr))))))))) |}.
imports: Coq(String List ZArith) compcert(Coqlib Integers Floats AST Ctypes Cop Clight Clightdefs)