fact: Definition f_getCell := {| fn_return := tint; fn_callconv := cc_default; fn_params := ((_graph, (tptr (tptr tint))) :: (_u, tint) :: (_i, tint) :: nil); fn_vars := nil; fn_temps := ((_t'2, tint) :: (_t'1, (tptr tint)) :: nil); fn_body := (Ssequence (Sset _t'1 (Ederef (Ebinop Oadd (Etempvar _graph (tptr (tptr tint))) (Etempvar _u tint) (tptr (tptr tint))) (tptr tint))) (Ssequence (Sset _t'2 (Ederef (Ebinop Oadd (Etempvar _t'1 (tptr tint)) (Etempvar _i tint) (tptr tint)) tint)) (Sreturn (Some (Etempvar _t'2 tint))))) |}.
imports: Coq(String List ZArith) compcert(Coqlib Integers Floats AST Ctypes Cop Clight Clightdefs)