fact: Definition f_main := {| fn_return := tint; fn_callconv := cc_default; fn_params := nil; fn_vars := nil; fn_temps := ((_s, tuint) :: (_t'1, tuint) :: nil); fn_body := (Ssequence (Ssequence (Ssequence (Scall (Some _t'1) (Evar _summatrix (Tfunction (Tcons (tptr (tarray tuint 2)) (Tcons tint Tnil)) tuint cc_default)) ((Evar _twobytwo (tarray (tarray tuint 2) 2)) :: (Econst_int (Int.repr 2) tint) :: nil)) (Sset _s (Etempvar _t'1 tuint))) (Sreturn (Some (Ecast (Etempvar _s tuint) tint)))) (Sreturn (Some (Econst_int (Int.repr 0) tint)))) |}.
imports: Coq(String List ZArith) compcert(Coqlib Integers Floats AST Ctypes Cop Clight Clightdefs)