fact: Definition f_do_scan := {| 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)))) :: (_scan, (tptr (talignas 3%N (tptr tvoid)))) :: (_next, (tptr (tptr (talignas 3%N (tptr tvoid))))) :: nil); fn_vars := nil; fn_temps := ((_s, (tptr (talignas 3%N (tptr tvoid)))) :: (_hd, tulong) :: (_sz, tulong) :: (_tag, tint) :: (_j, tlong) :: (_t'2, (tptr (talignas 3%N (tptr tvoid)))) :: (_t'1, (talignas 3%N (tptr tvoid))) :: nil); fn_body := (Ssequence (Sset _s (Etempvar _scan (tptr (talignas 3%N (tptr tvoid))))) (Sloop (Ssequence (Ssequence (Sset _t'2 (Ederef (Etempvar _next (tptr (tptr (talignas 3%N (tptr tvoid))))) (tptr (talignas 3%N (tptr tvoid))))) (Sifthenelse (Ebinop Olt (Etempvar _s (tptr (talignas 3%N (tptr tvoid)))) (Etempvar _t'2 (tptr (talignas 3%N (tptr tvoid)))) tint) Sskip Sbreak)) (Ssequence (Ssequence (Sset _t'1 (Ederef (Etempvar _s (tptr (talignas 3%N (tptr tvoid)))) (talignas 3%N (tptr tvoid)))) (Sset _hd (Ecast (Etempvar _t'1 (talignas 3%N (tptr tvoid))) tulong))) (Ssequence (Sset _sz (Ecast (Ebinop Oshr (Etempvar _hd tulong) (Econst_int (Int.repr 10) tint) tulong) tulong)) (Ssequence (Sset _tag (Ecast (Ebinop Oand (Etempvar _hd tulong) (Econst_int (Int.repr 255) tint) tulong) tuint)) (Ssequence (Sifthenelse (Eunop Onotbool (Ebinop Oge (Etempvar _tag tint) (Econst_int (Int.repr 251) tint) tint) tint) (Ssequence (Sset _j (Ecast (Econst_int (Int.repr 1) tint) tlong)) (Sloop (Ssequence (Sifthenelse (Ebinop Ole (Etempvar _j tlong) (Etempvar _sz tulong) 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 _s (tptr (talignas 3%N (tptr tvoid)))) (tptr (talignas 3%N (tptr tvoid)))) (Etempvar _j tlong) (tptr (talignas 3%N (tptr tvoid)))) :: (Econst_int (Int.repr 0) tint) :: nil))) (Sset _j (Ebinop Oadd (Etempvar _j tlong) (Econst_int (Int.repr 1) tint) tlong)))) Sskip) (Sset _s (Ebinop Oadd (Etempvar _s (tptr (talignas 3%N (tptr tvoid)))) (Ebinop Oadd (Econst_int (Int.repr 1) tint) (Etempvar _sz tulong) tulong) (tptr (talignas 3%N (tptr tvoid)))))))))) Sskip)) |}.
imports: Coq(String List ZArith) compcert(Coqlib Integers Floats AST Ctypes Cop Clight Clightdefs)