fact: Definition f_getPaths := {| fn_return := tvoid; fn_callconv := cc_default; fn_params := ((_src, tint) :: (_dist, (tptr tint)) :: (_prev, (tptr tint)) :: nil); fn_vars := nil; fn_temps := ((_i, tint) :: (_t'1, tint) :: (_t'3, tint) :: (_t'2, tint) :: nil); fn_body := (Ssequence (Ssequence (Sset _i (Econst_int (Int.repr 0) tint)) (Sloop (Ssequence (Sifthenelse (Ebinop Olt (Etempvar _i tint) (Econst_int (Int.repr 8) tint) tint) Sskip Sbreak) (Ssequence (Sifthenelse (Ebinop One (Etempvar _i tint) (Etempvar _src tint) tint) (Ssequence (Sset _t'3 (Ederef (Ebinop Oadd (Etempvar _dist (tptr tint)) (Etempvar _i tint) (tptr tint)) tint)) (Sset _t'1 (Ecast (Ebinop Olt (Etempvar _t'3 tint) (Econst_int (Int.repr 2147483647) tint) tint) tbool))) (Sset _t'1 (Econst_int (Int.repr 0) tint))) (Sifthenelse (Etempvar _t'1 tint) (Ssequence (Ssequence (Sset _t'2 (Ederef (Ebinop Oadd (Etempvar _dist (tptr tint)) (Etempvar _i tint) (tptr tint)) tint)) (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 39)) :: (Etempvar _src tint) :: (Etempvar _i tint) :: (Etempvar _t'2 tint) :: nil))) (Scall None (Evar _printPath (Tfunction (Tcons tint (Tcons tint (Tcons (tptr tint) Tnil))) tvoid cc_default)) ((Etempvar _i tint) :: (Etempvar _src tint) :: (Etempvar _prev (tptr tint)) :: nil))) Sskip))) (Sset _i (Ebinop Oadd (Etempvar _i tint) (Econst_int (Int.repr 1) tint) tint)))) (Scall None (Evar _printf (Tfunction (Tcons (tptr tschar) Tnil) tint {|cc_vararg:=(Some 1); cc_unproto:=false; cc_structret:=false|})) ((Evar ___stringlit_6 (tarray tschar 28)) :: nil))) |}.
imports: Coq(String List ZArith) compcert(Coqlib Integers Floats AST Ctypes Cop Clight Clightdefs)