fact: Definition f_fill_edge := {| fn_return := tvoid; fn_callconv := cc_default; fn_params := ((_wedge, (tptr (Tstruct _edge noattr))) :: (_w, tint) :: (_u, tint) :: (_v, tint) :: nil); fn_vars := nil; fn_temps := nil; fn_body := (Ssequence (Sassign (Efield (Ederef (Etempvar _wedge (tptr (Tstruct _edge noattr))) (Tstruct _edge noattr)) _weight tint) (Etempvar _w tint)) (Ssequence (Sassign (Efield (Ederef (Etempvar _wedge (tptr (Tstruct _edge noattr))) (Tstruct _edge noattr)) _src tint) (Etempvar _u tint)) (Sassign (Efield (Ederef (Etempvar _wedge (tptr (Tstruct _edge noattr))) (Tstruct _edge noattr)) _dst tint) (Etempvar _v tint)))) |}.
imports: Coq(String List ZArith) compcert(Coqlib Integers Floats AST Ctypes Cop Clight Clightdefs)