fact: Definition f_free_graph := {| fn_return := tvoid; fn_callconv := cc_default; fn_params := ((_graph__1, (tptr (Tstruct _graph noattr))) :: nil); fn_vars := nil; fn_temps := ((_t'1, (tptr (Tstruct _edge noattr))) :: nil); fn_body := (Ssequence (Ssequence (Sset _t'1 (Efield (Ederef (Etempvar _graph__1 (tptr (Tstruct _graph noattr))) (Tstruct _graph noattr)) _edge_list (tptr (Tstruct _edge noattr)))) (Scall None (Evar _free (Tfunction (Tcons (tptr tvoid) Tnil) tvoid cc_default)) ((Etempvar _t'1 (tptr (Tstruct _edge noattr))) :: nil))) (Scall None (Evar _free (Tfunction (Tcons (tptr tvoid) Tnil) tvoid cc_default)) ((Etempvar _graph__1 (tptr (Tstruct _graph noattr))) :: nil))) |}.
imports: Coq(String List ZArith) compcert(Coqlib Integers Floats AST Ctypes Cop Clight Clightdefs)