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, (tptr (talignas 3%N (tptr tvoid)))) :: (_va, (talignas 3%N (tptr tvoid))) :: (_hd, tulong) :: (_i, tlong) :: (_sz, tlong) :: (_newv, (tptr (talignas 3%N (tptr tvoid)))) :: (_t'5, tint) :: (_t'4, tint) :: (_t'3, (talignas 3%N (tptr tvoid))) :: (_t'2, (talignas 3%N (tptr tvoid))) :: (_t'1, (tptr tvoid)) :: (_t'8, (talignas 3%N (tptr tvoid))) :: (_t'7, (tptr (talignas 3%N (tptr tvoid)))) :: (_t'6, (talignas 3%N (tptr tvoid))) :: nil); fn_body := (Ssequence (Sset _va (Ederef (Etempvar _p (tptr (talignas 3%N (tptr tvoid)))) (talignas 3%N (tptr tvoid)))) (Ssequence (Scall (Some _t'5) (Evar _is_ptr (Tfunction (Tcons (talignas 3%N (tptr tvoid)) Tnil) tint cc_default)) ((Etempvar _va (talignas 3%N (tptr tvoid))) :: nil)) (Sifthenelse (Etempvar _t'5 tint) (Ssequence (Ssequence (Scall (Some _t'1) (Evar _int_or_ptr_to_ptr (Tfunction (Tcons (talignas 3%N (tptr tvoid)) Tnil) (tptr tvoid) cc_default)) ((Etempvar _va (talignas 3%N (tptr tvoid))) :: nil)) (Sset _v (Ecast (Etempvar _t'1 (tptr tvoid)) (tptr (talignas 3%N (tptr tvoid)))))) (Ssequence (Scall (Some _t'4) (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 (tptr (talignas 3%N (tptr tvoid)))) :: nil)) (Sifthenelse (Etempvar _t'4 tint) (Ssequence (Sset _hd (Ederef (Ebinop Oadd (Ecast (Etempvar _v (tptr (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'8 (Ederef (Ebinop Oadd (Ecast (Etempvar _v (tptr (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'8 (talignas 3%N (tptr tvoid))))) (Ssequence (Sset _sz (Ecast (Ebinop Oshr (Etempvar _hd tulong) (Econst_int (Int.repr 10) tint) tulong) tulong)) (Ssequence (Ssequence (Sset _t'7 (Ederef (Etempvar _next (tptr (tptr (talignas 3%N (tptr tvoid))))) (tptr (talignas 3%N (tptr tvoid))))) (Sset _newv (Ebinop Oadd (Etempvar _t'7 (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 _newv (tptr (talignas 3%N (tptr tvoid)))) (Etempvar _sz tlong) (tptr (talignas 3%N (tptr tvoid))))) (Ssequence (Sassign (Ederef (Ebinop Oadd (Ecast (Etempvar _newv (tptr (talignas 3%N (tptr tvoid)))) (tptr tulong)) (Eunop Oneg (Econst_int (Int.repr 1) tint) tint) (tptr tulong)) tulong) (Etempvar _hd tulong)) (Ssequence (Ssequence (Sset _i (Ecast (Econst_int (Int.repr 0) tint) tlong)) (Sloop (Ssequence (Sifthenelse (Ebinop Olt (Etempvar _i tlong) (Etempvar _sz tlong) tint) Sskip Sbreak) (Ssequence (Sset _t'6 (Ederef (Ebinop Oadd (Ecast (Etempvar _v (tptr (talignas 3%N (tptr tvoid)))) (tptr (talignas 3%N (tptr tvoid)))) (Etempvar _i tlong) (tptr (talignas 3%N (tptr tvoid)))) (talignas 3%N (tptr tvoid)))) (Sassign (Ederef (Ebinop Oadd (Ecast (Etempvar _newv (tptr (talignas 3%N (tptr tvoid)))) (tptr (talignas 3%N (tptr tvoid)))) (Etempvar _i tlong) (tptr (talignas 3%N (tptr tvoid)))) (talignas 3%N (tptr tvoid))) (Etempvar _t'6 (talignas 3%N (tptr tvoid)))))) (Sset _i (Ebinop Oadd (Etempvar _i tlong) (Econst_int (Int.repr 1) tint) tlong)))) (Ssequence (Sassign (Ederef (Ebinop Oadd (Ecast (Etempvar _v (tptr (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 (Ssequence (Scall (Some _t'2) (Evar _ptr_to_int_or_ptr (Tfunction (Tcons (tptr tvoid) Tnil) (talignas 3%N (tptr tvoid)) cc_default)) ((Ecast (Etempvar _newv (tptr (talignas 3%N (tptr tvoid)))) (tptr tvoid)) :: nil)) (Sassign (Ederef (Ebinop Oadd (Ecast (Etempvar _v (tptr (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))) (Etempvar _t'2 (talignas 3%N (tptr tvoid))))) (Ssequence (Ssequence (Scall (Some _t'3) (Evar _ptr_to_int_or_ptr (Tfunction (Tcons (tptr tvoid) Tnil) (talignas 3%N (tptr tvoid)) cc_default)) ((Ecast (Etempvar _newv (tptr (talignas 3%N (tptr tvoid)))) (tptr tvoid)) :: nil)) (Sassign (Ederef (Etempvar _p (tptr (talignas 3%N (tptr tvoid)))) (talignas 3%N (tptr tvoid))) (Etempvar _t'3 (talignas 3%N (tptr tvoid))))) (Sifthenelse (Ebinop Ogt (Etempvar _depth tint) (Econst_int (Int.repr 0) tint) tint) (Sifthenelse (Eunop Onotbool (Ebinop Oge (Ecast (Ebinop Oand (Etempvar _hd tulong) (Econst_int (Int.repr 255) tint) tulong) tuint) (Econst_int (Int.repr 251) tint) tint) tint) (Ssequence (Sset _i (Ecast (Econst_int (Int.repr 0) tint) tlong)) (Sloop (Ssequence (Sifthenelse (Ebinop Olt (Etempvar _i tlong) (Etempvar _sz tlong) 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 _newv (tptr (talignas 3%N (tptr tvoid)))) (tptr (talignas 3%N (tptr tvoid)))) (Etempvar _i tlong) (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 tlong) (Econst_int (Int.repr 1) tint) tlong)))) Sskip) Sskip))))))))))) Sskip))) Sskip))) |}.
imports: Coq(String List ZArith) compcert(Coqlib Integers Floats AST Ctypes Cop Clight Clightdefs)