fact: Definition f_forward := {| 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))))) :: (_p, (tptr (talignas 3%N (tptr tvoid)))) :: (_depth, tint) :: nil); fn_vars := nil; fn_temps := ((_v, (talignas 3%N (tptr tvoid))) :: (_hd, tulong) :: (_i, tint) :: (_sz, tint) :: (_new, (tptr (talignas 3%N (tptr tvoid)))) :: (_t'2, tint) :: (_t'1, tint) :: (_t'5, (talignas 3%N (tptr tvoid))) :: (_t'4, (tptr (talignas 3%N (tptr tvoid)))) :: (_t'3, (talignas 3%N (tptr tvoid))) :: nil); fn_body := (Ssequence (Sset _v (Ederef (Etempvar _p (tptr (talignas 3%N (tptr tvoid)))) (talignas 3%N (tptr tvoid)))) (Ssequence (Scall (Some _t'2) (Evar _Is_block (Tfunction (Tcons (talignas 3%N (tptr tvoid)) Tnil) tint cc_default)) ((Etempvar _v (talignas 3%N (tptr tvoid))) :: nil)) (Sifthenelse (Etempvar _t'2 tint) (Ssequence (Scall (Some _t'1) (Evar _Is_from (Tfunction (Tcons (tptr (talignas 3%N (tptr tvoid))) (Tcons (tptr (talignas 3%N (tptr tvoid))) (Tcons (tptr (talignas 3%N (tptr tvoid))) Tnil))) tint cc_default)) ((Etempvar _from_start (tptr (talignas 3%N (tptr tvoid)))) :: (Etempvar _from_limit (tptr (talignas 3%N (tptr tvoid)))) :: (Etempvar _v (talignas 3%N (tptr tvoid))) :: nil)) (Sifthenelse (Etempvar _t'1 tint) (Ssequence (Sset _hd (Ederef (Ebinop Oadd (Ecast (Etempvar _v (talignas 3%N (tptr tvoid))) (tptr tulong)) (Eunop Oneg (Econst_int (Int.repr 1) tint) tint) (tptr tulong)) tulong)) (Sifthenelse (Ebinop Oeq (Etempvar _hd tulong) (Econst_int (Int.repr 0) tint) tint) (Ssequence (Sset _t'5 (Ederef (Ebinop Oadd (Ecast (Etempvar _v (talignas 3%N (tptr tvoid))) (tptr (talignas 3%N (tptr tvoid)))) (Econst_int (Int.repr 0) tint) (tptr (talignas 3%N (tptr tvoid)))) (talignas 3%N (tptr tvoid)))) (Sassign (Ederef (Etempvar _p (tptr (talignas 3%N (tptr tvoid)))) (talignas 3%N (tptr tvoid))) (Etempvar _t'5 (talignas 3%N (tptr tvoid))))) (Ssequence (Sset _sz (Ecast (Ecast (Ebinop Oshr (Etempvar _hd tulong) (Econst_int (Int.repr 10) tint) tulong) tulong) tint)) (Ssequence (Ssequence (Sset _t'4 (Ederef (Etempvar _next (tptr (tptr (talignas 3%N (tptr tvoid))))) (tptr (talignas 3%N (tptr tvoid))))) (Sset _new (Ebinop Oadd (Etempvar _t'4 (tptr (talignas 3%N (tptr tvoid)))) (Econst_int (Int.repr 1) tint) (tptr (talignas 3%N (tptr tvoid)))))) (Ssequence (Sassign (Ederef (Etempvar _next (tptr (tptr (talignas 3%N (tptr tvoid))))) (tptr (talignas 3%N (tptr tvoid)))) (Ebinop Oadd (Etempvar _new (tptr (talignas 3%N (tptr tvoid)))) (Etempvar _sz tint) (tptr (talignas 3%N (tptr tvoid))))) (Ssequence (Sifthenelse (Ebinop Ogt (Etempvar _sz tint) (Econst_int (Int.repr 50) tint) tint) (Scall None (Evar _printf (Tfunction (Tcons (tptr tschar) Tnil) tint {|cc_vararg:=(Some 1); cc_unproto:=false; cc_structret:=false|})) ((Evar ___stringlit_2 (tarray tschar 45)) :: (Ecast (Etempvar _v (talignas 3%N (tptr tvoid))) (tptr tvoid)) :: (Etempvar _hd tulong) :: (Etempvar _sz tint) :: nil)) Sskip) (Ssequence (Ssequence (Sset _i (Eunop Oneg (Econst_int (Int.repr 1) tint) tint)) (Sloop (Ssequence (Sifthenelse (Ebinop Olt (Etempvar _i tint) (Etempvar _sz tint) tint) Sskip Sbreak) (Ssequence (Sset _t'3 (Ederef (Ebinop Oadd (Ecast (Etempvar _v (talignas 3%N (tptr tvoid))) (tptr (talignas 3%N (tptr tvoid)))) (Etempvar _i tint) (tptr (talignas 3%N (tptr tvoid)))) (talignas 3%N (tptr tvoid)))) (Sassign (Ederef (Ebinop Oadd (Ecast (Etempvar _new (tptr (talignas 3%N (tptr tvoid)))) (tptr (talignas 3%N (tptr tvoid)))) (Etempvar _i tint) (tptr (talignas 3%N (tptr tvoid)))) (talignas 3%N (tptr tvoid))) (Etempvar _t'3 (talignas 3%N (tptr tvoid)))))) (Sset _i (Ebinop Oadd (Etempvar _i tint) (Econst_int (Int.repr 1) tint) tint)))) (Ssequence (Sassign (Ederef (Ebinop Oadd (Ecast (Etempvar _v (talignas 3%N (tptr tvoid))) (tptr tulong)) (Eunop Oneg (Econst_int (Int.repr 1) tint) tint) (tptr tulong)) tulong) (Econst_int (Int.repr 0) tint)) (Ssequence (Sassign (Ederef (Ebinop Oadd (Ecast (Etempvar _v (talignas 3%N (tptr tvoid))) (tptr (talignas 3%N (tptr tvoid)))) (Econst_int (Int.repr 0) tint) (tptr (talignas 3%N (tptr tvoid)))) (talignas 3%N (tptr tvoid))) (Ecast (Etempvar _new (tptr (talignas 3%N (tptr tvoid)))) (talignas 3%N (tptr tvoid)))) (Ssequence (Sassign (Ederef (Etempvar _p (tptr (talignas 3%N (tptr tvoid)))) (talignas 3%N (tptr tvoid))) (Ecast (Etempvar _new (tptr (talignas 3%N (tptr tvoid)))) (talignas 3%N (tptr tvoid)))) (Sifthenelse (Ebinop Ogt (Etempvar _depth tint) (Econst_int (Int.repr 0) tint) tint) (Ssequence (Sset _i (Econst_int (Int.repr 0) tint)) (Sloop (Ssequence (Sifthenelse (Ebinop Olt (Etempvar _i tint) (Etempvar _sz tint) 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))))) :: (Ebinop Oadd (Ecast (Etempvar _new (tptr (talignas 3%N (tptr tvoid)))) (tptr (talignas 3%N (tptr tvoid)))) (Etempvar _i tint) (tptr (talignas 3%N (tptr tvoid)))) :: (Ebinop Osub (Etempvar _depth tint) (Econst_int (Int.repr 1) tint) tint) :: nil))) (Sset _i (Ebinop Oadd (Etempvar _i tint) (Econst_int (Int.repr 1) tint) tint)))) Sskip))))))))))) Sskip)) Sskip))) |}.
imports: Coq(String List ZArith) compcert(Coqlib Integers Floats AST Ctypes Cop Clight Clightdefs)