fact: Definition f_print_graph := {| fn_return := tvoid; fn_callconv := cc_default; fn_params := ((_graph, (tptr (tarray tint 8))) :: (_src, tint) :: nil); fn_vars := nil; fn_temps := ((_i, tint) :: (_j, tint) :: (_t'2, tint) :: (_t'1, 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 (Ssequence (Sset _j (Econst_int (Int.repr 0) tint)) (Sloop (Ssequence (Sifthenelse (Ebinop Olt (Etempvar _j tint) (Econst_int (Int.repr 8) tint) tint) Sskip Sbreak) (Ssequence (Sset _t'1 (Ederef (Ebinop Oadd (Ederef (Ebinop Oadd (Etempvar _graph (tptr (tarray tint 8))) (Etempvar _i tint) (tptr (tarray tint 8))) (tarray tint 8)) (Etempvar _j tint) (tptr tint)) tint)) (Sifthenelse (Ebinop Oeq (Etempvar _t'1 tint) (Econst_int (Int.repr 2147483647) 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 3)) :: nil)) (Ssequence (Sset _t'2 (Ederef (Ebinop Oadd (Ederef (Ebinop Oadd (Etempvar _graph (tptr (tarray tint 8))) (Etempvar _i tint) (tptr (tarray tint 8))) (tarray tint 8)) (Etempvar _j 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_1 (tarray tschar 4)) :: (Etempvar _t'2 tint) :: nil)))))) (Sset _j (Ebinop Oadd (Etempvar _j 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_3 (tarray tschar 2)) :: nil)))) (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_4 (tarray tschar 22)) :: (Econst_int (Int.repr 8) tint) :: (Etempvar _src tint) :: nil))) |}.
imports: Coq(String List ZArith) compcert(Coqlib Integers Floats AST Ctypes Cop Clight Clightdefs)