fact: Definition f_do_generation := {| fn_return := tvoid; fn_callconv := cc_default; fn_params := ((_from, (tptr (Tstruct _space noattr))) :: (_to, (tptr (Tstruct _space noattr))) :: (_ti, (tptr (Tstruct _thread_info noattr))) :: nil); fn_vars := nil; fn_temps := ((_p, (tptr (talignas 3%N (tptr tvoid)))) :: (_t'12, (tptr (talignas 3%N (tptr tvoid)))) :: (_t'11, (tptr (talignas 3%N (tptr tvoid)))) :: (_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)))) :: (_t'4, (tptr (talignas 3%N (tptr tvoid)))) :: (_t'3, (tptr (talignas 3%N (tptr tvoid)))) :: (_t'2, (tptr (talignas 3%N (tptr tvoid)))) :: (_t'1, (tptr (talignas 3%N (tptr tvoid)))) :: nil); fn_body := (Ssequence (Sset _p (Efield (Ederef (Etempvar _to (tptr (Tstruct _space noattr))) (Tstruct _space noattr)) _next (tptr (talignas 3%N (tptr tvoid))))) (Ssequence (Ssequence (Sset _t'7 (Efield (Ederef (Etempvar _from (tptr (Tstruct _space noattr))) (Tstruct _space noattr)) _next (tptr (talignas 3%N (tptr tvoid))))) (Ssequence (Sset _t'8 (Efield (Ederef (Etempvar _from (tptr (Tstruct _space noattr))) (Tstruct _space noattr)) _start (tptr (talignas 3%N (tptr tvoid))))) (Ssequence (Sset _t'9 (Efield (Ederef (Etempvar _from (tptr (Tstruct _space noattr))) (Tstruct _space noattr)) _rem_limit (tptr (talignas 3%N (tptr tvoid))))) (Ssequence (Sset _t'10 (Efield (Ederef (Etempvar _from (tptr (Tstruct _space noattr))) (Tstruct _space noattr)) _limit (tptr (talignas 3%N (tptr tvoid))))) (Ssequence (Sset _t'11 (Efield (Ederef (Etempvar _to (tptr (Tstruct _space noattr))) (Tstruct _space noattr)) _limit (tptr (talignas 3%N (tptr tvoid))))) (Ssequence (Sset _t'12 (Efield (Ederef (Etempvar _to (tptr (Tstruct _space noattr))) (Tstruct _space noattr)) _next (tptr (talignas 3%N (tptr tvoid))))) (Sifthenelse (Ebinop Ole (Ebinop Osub (Ebinop Oadd (Ebinop Osub (Etempvar _t'7 (tptr (talignas 3%N (tptr tvoid)))) (Etempvar _t'8 (tptr (talignas 3%N (tptr tvoid)))) tlong) (Etempvar _t'9 (tptr (talignas 3%N (tptr tvoid)))) (tptr (talignas 3%N (tptr tvoid)))) (Etempvar _t'10 (tptr (talignas 3%N (tptr tvoid)))) tlong) (Ebinop Osub (Etempvar _t'11 (tptr (talignas 3%N (tptr tvoid)))) (Etempvar _t'12 (tptr (talignas 3%N (tptr tvoid)))) tlong) tint) Sskip (Ssequence (Scall None (Evar _printf (Tfunction (Tcons (tptr tschar) Tnil) tint {|cc_vararg:=(Some 1); cc_unproto:=false; cc_structret:=false|})) ((Evar ___stringlit_5 (tarray tschar 30)) :: (Evar ___stringlit_4 (tarray tschar 5)) :: (Econst_int (Int.repr 281) tint) :: (Evar ___stringlit_6 (tarray tschar 75)) :: nil)) (Scall None (Evar _abort (Tfunction Tnil tvoid cc_default)) nil))))))))) (Ssequence (Scall None (Evar _forward_remset (Tfunction (Tcons (tptr (Tstruct _space noattr)) (Tcons (tptr (Tstruct _space noattr)) (Tcons (tptr (tptr (talignas 3%N (tptr tvoid)))) Tnil))) tvoid cc_default)) ((Etempvar _from (tptr (Tstruct _space noattr))) :: (Etempvar _to (tptr (Tstruct _space noattr))) :: (Eaddrof (Efield (Ederef (Etempvar _to (tptr (Tstruct _space noattr))) (Tstruct _space noattr)) _next (tptr (talignas 3%N (tptr tvoid)))) (tptr (tptr (talignas 3%N (tptr tvoid))))) :: nil)) (Ssequence (Ssequence (Sset _t'5 (Efield (Ederef (Etempvar _from (tptr (Tstruct _space noattr))) (Tstruct _space noattr)) _start (tptr (talignas 3%N (tptr tvoid))))) (Ssequence (Sset _t'6 (Efield (Ederef (Etempvar _from (tptr (Tstruct _space noattr))) (Tstruct _space noattr)) _limit (tptr (talignas 3%N (tptr tvoid))))) (Scall None (Evar _forward_roots (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 (Tstruct _thread_info noattr)) Tnil)))) tvoid cc_default)) ((Etempvar _t'5 (tptr (talignas 3%N (tptr tvoid)))) :: (Etempvar _t'6 (tptr (talignas 3%N (tptr tvoid)))) :: (Eaddrof (Efield (Ederef (Etempvar _to (tptr (Tstruct _space noattr))) (Tstruct _space noattr)) _next (tptr (talignas 3%N (tptr tvoid)))) (tptr (tptr (talignas 3%N (tptr tvoid))))) :: (Etempvar _ti (tptr (Tstruct _thread_info noattr))) :: nil)))) (Ssequence (Ssequence (Sset _t'3 (Efield (Ederef (Etempvar _from (tptr (Tstruct _space noattr))) (Tstruct _space noattr)) _start (tptr (talignas 3%N (tptr tvoid))))) (Ssequence (Sset _t'4 (Efield (Ederef (Etempvar _from (tptr (Tstruct _space noattr))) (Tstruct _space noattr)) _limit (tptr (talignas 3%N (tptr tvoid))))) (Scall None (Evar _do_scan (Tfunction (Tcons (tptr (talignas 3%N (tptr tvoid))) (Tcons (tptr (talignas 3%N (tptr tvoid))) (Tcons (tptr (talignas 3%N (tptr tvoid))) (Tcons (tptr (tptr (talignas 3%N (tptr tvoid)))) Tnil)))) tvoid cc_default)) ((Etempvar _t'3 (tptr (talignas 3%N (tptr tvoid)))) :: (Etempvar _t'4 (tptr (talignas 3%N (tptr tvoid)))) :: (Etempvar _p (tptr (talignas 3%N (tptr tvoid)))) :: (Eaddrof (Efield (Ederef (Etempvar _to (tptr (Tstruct _space noattr))) (Tstruct _space noattr)) _next (tptr (talignas 3%N (tptr tvoid)))) (tptr (tptr (talignas 3%N (tptr tvoid))))) :: nil)))) (Ssequence (Ssequence (Sset _t'2 (Efield (Ederef (Etempvar _from (tptr (Tstruct _space noattr))) (Tstruct _space noattr)) _start (tptr (talignas 3%N (tptr tvoid))))) (Sassign (Efield (Ederef (Etempvar _from (tptr (Tstruct _space noattr))) (Tstruct _space noattr)) _next (tptr (talignas 3%N (tptr tvoid)))) (Etempvar _t'2 (tptr (talignas 3%N (tptr tvoid)))))) (Ssequence (Sset _t'1 (Efield (Ederef (Etempvar _from (tptr (Tstruct _space noattr))) (Tstruct _space noattr)) _rem_limit (tptr (talignas 3%N (tptr tvoid))))) (Sassign (Efield (Ederef (Etempvar _from (tptr (Tstruct _space noattr))) (Tstruct _space noattr)) _limit (tptr (talignas 3%N (tptr tvoid)))) (Etempvar _t'1 (tptr (talignas 3%N (tptr tvoid)))))))))))) |}.
imports: Coq(String List ZArith) compcert(Coqlib Integers Floats AST Ctypes Cop Clight Clightdefs)