fact: Definition f_Is_from := {| fn_return := tint; fn_callconv := cc_default; fn_params := ((_from_start, (tptr (talignas 3%N (tptr tvoid)))) :: (_from_limit, (tptr (talignas 3%N (tptr tvoid)))) :: (_v, (tptr (talignas 3%N (tptr tvoid)))) :: nil); fn_vars := nil; fn_temps := ((_t'1, tint) :: nil); fn_body := (Ssequence (Sifthenelse (Ebinop Ole (Etempvar _from_start (tptr (talignas 3%N (tptr tvoid)))) (Etempvar _v (tptr (talignas 3%N (tptr tvoid)))) tint) (Sset _t'1 (Ecast (Ebinop Olt (Etempvar _v (tptr (talignas 3%N (tptr tvoid)))) (Etempvar _from_limit (tptr (talignas 3%N (tptr tvoid)))) tint) tbool)) (Sset _t'1 (Econst_int (Int.repr 0) tint))) (Sreturn (Some (Etempvar _t'1 tint)))) |}.
imports: Coq(String List ZArith) compcert(Coqlib Integers Floats AST Ctypes Cop Clight Clightdefs)