fact: Definition f_forward_remset := {| fn_return := tvoid; fn_callconv := cc_default; fn_params := ((_from, (tptr (Tstruct _space noattr))) :: (_to, (tptr (Tstruct _space noattr))) :: (_next, (tptr (tptr (talignas 3%N (tptr tvoid))))) :: nil); fn_vars := nil; fn_temps := ((_from_start, (tptr (talignas 3%N (tptr tvoid)))) :: (_from_limit, (tptr (talignas 3%N (tptr tvoid)))) :: (_from_rem_limit, (tptr (talignas 3%N (tptr tvoid)))) :: (_q, (tptr (talignas 3%N (tptr tvoid)))) :: (_p, (tptr (talignas 3%N (tptr tvoid)))) :: (_oldp, (talignas 3%N (tptr tvoid))) :: (_newp, (talignas 3%N (tptr tvoid))) :: (_t'2, tint) :: (_t'1, (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)))) :: nil); fn_body := (Ssequence (Sset _from_start (Efield (Ederef (Etempvar _from (tptr (Tstruct _space noattr))) (Tstruct _space noattr)) _start (tptr (talignas 3%N (tptr tvoid))))) (Ssequence (Sset _from_limit (Efield (Ederef (Etempvar _from (tptr (Tstruct _space noattr))) (Tstruct _space noattr)) _limit (tptr (talignas 3%N (tptr tvoid))))) (Ssequence (Sset _from_rem_limit (Efield (Ederef (Etempvar _from (tptr (Tstruct _space noattr))) (Tstruct _space noattr)) _rem_limit (tptr (talignas 3%N (tptr tvoid))))) (Ssequence (Sset _q (Etempvar _from_limit (tptr (talignas 3%N (tptr tvoid))))) (Ssequence (Ssequence (Sset _t'4 (Efield (Ederef (Etempvar _to (tptr (Tstruct _space noattr))) (Tstruct _space noattr)) _limit (tptr (talignas 3%N (tptr tvoid))))) (Ssequence (Sset _t'5 (Efield (Ederef (Etempvar _to (tptr (Tstruct _space noattr))) (Tstruct _space noattr)) _start (tptr (talignas 3%N (tptr tvoid))))) (Sifthenelse (Ebinop Ole (Ebinop Osub (Etempvar _from_rem_limit (tptr (talignas 3%N (tptr tvoid)))) (Etempvar _from_limit (tptr (talignas 3%N (tptr tvoid)))) tlong) (Ebinop Osub (Etempvar _t'4 (tptr (talignas 3%N (tptr tvoid)))) (Etempvar _t'5 (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 214) tint) :: (Evar ___stringlit_3 (tarray tschar 49)) :: nil)) (Scall None (Evar _abort (Tfunction Tnil tvoid cc_default)) nil))))) (Swhile (Ebinop One (Etempvar _q (tptr (talignas 3%N (tptr tvoid)))) (Etempvar _from_rem_limit (tptr (talignas 3%N (tptr tvoid)))) tint) (Ssequence (Sset _p (Ederef (Ecast (Etempvar _q (tptr (talignas 3%N (tptr tvoid)))) (tptr (tptr (talignas 3%N (tptr tvoid))))) (tptr (talignas 3%N (tptr tvoid))))) (Ssequence (Ssequence (Sifthenelse (Ebinop Ole (Etempvar _from_start (tptr (talignas 3%N (tptr tvoid)))) (Etempvar _p (tptr (talignas 3%N (tptr tvoid)))) tint) (Sset _t'2 (Ecast (Ebinop Olt (Etempvar _p (tptr (talignas 3%N (tptr tvoid)))) (Etempvar _from_limit (tptr (talignas 3%N (tptr tvoid)))) tint) tbool)) (Sset _t'2 (Econst_int (Int.repr 0) tint))) (Sifthenelse (Eunop Onotbool (Etempvar _t'2 tint) tint) (Ssequence (Sset _oldp (Ederef (Etempvar _p (tptr (talignas 3%N (tptr tvoid)))) (talignas 3%N (tptr tvoid)))) (Ssequence (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 _p (tptr (talignas 3%N (tptr tvoid)))) :: (Econst_int (Int.repr 0) tint) :: nil)) (Ssequence (Sset _newp (Ederef (Etempvar _p (tptr (talignas 3%N (tptr tvoid)))) (talignas 3%N (tptr tvoid)))) (Sifthenelse (Ebinop One (Etempvar _oldp (talignas 3%N (tptr tvoid))) (Etempvar _newp (talignas 3%N (tptr tvoid))) tint) (Ssequence (Ssequence (Ssequence (Sset _t'3 (Efield (Ederef (Etempvar _to (tptr (Tstruct _space noattr))) (Tstruct _space noattr)) _limit (tptr (talignas 3%N (tptr tvoid))))) (Sset _t'1 (Ecast (Ebinop Osub (Etempvar _t'3 (tptr (talignas 3%N (tptr tvoid)))) (Econst_int (Int.repr 1) tint) (tptr (talignas 3%N (tptr tvoid)))) (tptr (talignas 3%N (tptr tvoid)))))) (Sassign (Efield (Ederef (Etempvar _to (tptr (Tstruct _space noattr))) (Tstruct _space noattr)) _limit (tptr (talignas 3%N (tptr tvoid)))) (Etempvar _t'1 (tptr (talignas 3%N (tptr tvoid)))))) (Sassign (Ederef (Etempvar _t'1 (tptr (talignas 3%N (tptr tvoid)))) (talignas 3%N (tptr tvoid))) (Ecast (Etempvar _q (tptr (talignas 3%N (tptr tvoid)))) (talignas 3%N (tptr tvoid))))) Sskip)))) Sskip)) (Sset _q (Ebinop Oadd (Etempvar _q (tptr (talignas 3%N (tptr tvoid)))) (Econst_int (Int.repr 1) tint) (tptr (talignas 3%N (tptr tvoid))))))))))))) |}.
imports: Coq(String List ZArith) compcert(Coqlib Integers Floats AST Ctypes Cop Clight Clightdefs)