fact: Definition f_init_empty_graph := {| fn_return := (tptr (Tstruct _graph noattr)); fn_callconv := cc_default; fn_params := nil; fn_vars := nil; fn_temps := ((_empty_graph, (tptr (Tstruct _graph noattr))) :: (_edge_list, (tptr (Tstruct _edge noattr))) :: (_t'2, (tptr tvoid)) :: (_t'1, (tptr tvoid)) :: (_t'3, tint) :: nil); fn_body := (Ssequence (Ssequence (Scall (Some _t'1) (Evar _mallocK (Tfunction (Tcons tint Tnil) (tptr tvoid) cc_default)) ((Esizeof (Tstruct _graph noattr) tulong) :: nil)) (Sset _empty_graph (Ecast (Etempvar _t'1 (tptr tvoid)) (tptr (Tstruct _graph noattr))))) (Ssequence (Ssequence (Ssequence (Sset _t'3 (Evar _MAX_EDGES tint)) (Scall (Some _t'2) (Evar _mallocK (Tfunction (Tcons tint Tnil) (tptr tvoid) cc_default)) ((Ebinop Omul (Esizeof (Tstruct _edge noattr) tulong) (Etempvar _t'3 tint) tulong) :: nil))) (Sset _edge_list (Ecast (Etempvar _t'2 (tptr tvoid)) (tptr (Tstruct _edge noattr))))) (Ssequence (Sassign (Efield (Ederef (Etempvar _empty_graph (tptr (Tstruct _graph noattr))) (Tstruct _graph noattr)) _V tint) (Econst_int (Int.repr 0) tint)) (Ssequence (Sassign (Efield (Ederef (Etempvar _empty_graph (tptr (Tstruct _graph noattr))) (Tstruct _graph noattr)) _E tint) (Econst_int (Int.repr 0) tint)) (Ssequence (Sassign (Efield (Ederef (Etempvar _empty_graph (tptr (Tstruct _graph noattr))) (Tstruct _graph noattr)) _edge_list (tptr (Tstruct _edge noattr))) (Etempvar _edge_list (tptr (Tstruct _edge noattr)))) (Sreturn (Some (Etempvar _empty_graph (tptr (Tstruct _graph noattr)))))))))) |}.
imports: Coq(String List ZArith) compcert(Coqlib Integers Floats AST Ctypes Cop Clight Clightdefs)