fact: Definition f_forward_roots := {| fn_return := tvoid; fn_callconv := cc_default; fn_params := ((_from_start, (tptr (talignas 2%N (tptr tvoid)))) :: (_from_limit, (tptr (talignas 2%N (tptr tvoid)))) :: (_next, (tptr (tptr (talignas 2%N (tptr tvoid))))) :: (_fi, (tptr tuint)) :: (_ti, (tptr (Tstruct _thread_info noattr))) :: nil); fn_vars := nil; fn_temps := ((_args, (tptr (talignas 2%N (tptr tvoid)))) :: (_n, tuint) :: (_i, tuint) :: (_roots, (tptr tuint)) :: (_t'2, tuint) :: (_t'1, tuint) :: nil); fn_body := (Ssequence (Sset _roots (Ebinop Oadd (Etempvar _fi (tptr tuint)) (Econst_int (Int.repr 2) tint) (tptr tuint))) (Ssequence (Sset _n (Ederef (Ebinop Oadd (Etempvar _fi (tptr tuint)) (Econst_int (Int.repr 1) tint) (tptr tuint)) tuint)) (Ssequence (Sset _args (Efield (Ederef (Etempvar _ti (tptr (Tstruct _thread_info noattr))) (Tstruct _thread_info noattr)) _args (tarray (talignas 2%N (tptr tvoid)) 1024))) (Ssequence (Sset _i (Econst_int (Int.repr 0) tint)) (Sloop (Ssequence (Sifthenelse (Ebinop Olt (Etempvar _i tuint) (Etempvar _n tuint) tint) Sskip Sbreak) (Ssequence (Ssequence (Sset _t'2 (Ederef (Ebinop Oadd (Etempvar _roots (tptr tuint)) (Etempvar _i tuint) (tptr tuint)) tuint)) (Sifthenelse (Ebinop Olt (Etempvar _t'2 tuint) (Econst_int (Int.repr 1024) tint) tint) Sskip (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 210) tint) :: (Ecast (Econst_int (Int.repr 0) tint) (tptr tvoid)) :: (Evar ___stringlit_1 (tarray tschar 20)) :: nil)))) (Ssequence (Sset _t'1 (Ederef (Ebinop Oadd (Etempvar _roots (tptr tuint)) (Etempvar _i tuint) (tptr tuint)) tuint)) (Scall None (Evar _forward (Tfunction (Tcons (tptr (talignas 2%N (tptr tvoid))) (Tcons (tptr (talignas 2%N (tptr tvoid))) (Tcons (tptr (tptr (talignas 2%N (tptr tvoid)))) (Tcons (tptr (talignas 2%N (tptr tvoid))) (Tcons tint Tnil))))) tvoid cc_default)) ((Etempvar _from_start (tptr (talignas 2%N (tptr tvoid)))) :: (Etempvar _from_limit (tptr (talignas 2%N (tptr tvoid)))) :: (Etempvar _next (tptr (tptr (talignas 2%N (tptr tvoid))))) :: (Ebinop Oadd (Etempvar _args (tptr (talignas 2%N (tptr tvoid)))) (Etempvar _t'1 tuint) (tptr (talignas 2%N (tptr tvoid)))) :: (Econst_int (Int.repr 0) tint) :: nil))))) (Sset _i (Ebinop Oadd (Etempvar _i tuint) (Econst_int (Int.repr 1) tint) tuint))))))) |}.
imports: Coq(String List ZArith) compcert(Coqlib Integers Floats AST Ctypes Cop Clight Clightdefs)