fact: Definition f_greater := {| fn_return := tint; fn_callconv := cc_default; fn_params := ((_j, tuint) :: (_k, tuint) :: (_arr, (tptr (Tstruct _edge noattr))) :: nil); fn_vars := nil; fn_temps := ((_t'2, tint) :: (_t'1, tint) :: nil); fn_body := (Ssequence (Sset _t'1 (Efield (Ederef (Ebinop Oadd (Etempvar _arr (tptr (Tstruct _edge noattr))) (Etempvar _j tuint) (tptr (Tstruct _edge noattr))) (Tstruct _edge noattr)) _weight tint)) (Ssequence (Sset _t'2 (Efield (Ederef (Ebinop Oadd (Etempvar _arr (tptr (Tstruct _edge noattr))) (Etempvar _k tuint) (tptr (Tstruct _edge noattr))) (Tstruct _edge noattr)) _weight tint)) (Sreturn (Some (Ebinop Oge (Etempvar _t'1 tint) (Etempvar _t'2 tint) tint))))) |}.
imports: Coq(String List ZArith) compcert(Coqlib Integers Floats AST Ctypes Cop Clight Clightdefs)