fact: Definition f_summatrix := {| fn_return := tuint; fn_callconv := cc_default; fn_params := ((_a, (tptr (tarray tuint 2))) :: (_n, tint) :: nil); fn_vars := nil; fn_temps := ((_i, tint) :: (_j, tint) :: (_s, tuint) :: (_t'1, tuint) :: nil); fn_body := (Ssequence (Sset _i (Econst_int (Int.repr 0) tint)) (Ssequence (Sset _j (Econst_int (Int.repr 0) tint)) (Ssequence (Sset _s (Econst_int (Int.repr 0) tint)) (Ssequence (Swhile (Ebinop Olt (Etempvar _i tint) (Etempvar _n tint) tint) (Ssequence (Sset _j (Econst_int (Int.repr 0) tint)) (Ssequence (Swhile (Ebinop Olt (Etempvar _j tint) (Etempvar _n tint) tint) (Ssequence (Ssequence (Sset _t'1 (Ederef (Ebinop Oadd (Ederef (Ebinop Oadd (Etempvar _a (tptr (tarray tuint 2))) (Etempvar _i tint) (tptr (tarray tuint 2))) (tarray tuint 2)) (Etempvar _j tint) (tptr tuint)) tuint)) (Sset _s (Ebinop Oadd (Etempvar _s tuint) (Etempvar _t'1 tuint) tuint))) (Sset _j (Ebinop Oadd (Etempvar _j tint) (Econst_int (Int.repr 1) tint) tint)))) (Sset _i (Ebinop Oadd (Etempvar _i tint) (Econst_int (Int.repr 1) tint) tint))))) (Sreturn (Some (Etempvar _s tuint))))))) |}.
imports: Coq(String List ZArith) compcert(Coqlib Integers Floats AST Ctypes Cop Clight Clightdefs)