fact: Definition f_find := {| fn_return := tint; fn_callconv := cc_default; fn_params := ((_subsets, (tptr (Tstruct _subset noattr))) :: (_i, tint) :: nil); fn_vars := nil; fn_temps := ((_p0, tint) :: (_p, tint) :: (_t'1, tint) :: nil); fn_body := (Ssequence (Sset _p0 (Econst_int (Int.repr 0) tint)) (Ssequence (Sset _p (Efield (Ederef (Ebinop Oadd (Etempvar _subsets (tptr (Tstruct _subset noattr))) (Etempvar _i tint) (tptr (Tstruct _subset noattr))) (Tstruct _subset noattr)) _parent tint)) (Ssequence (Sifthenelse (Ebinop One (Etempvar _p tint) (Etempvar _i tint) tint) (Ssequence (Ssequence (Scall (Some _t'1) (Evar _find (Tfunction (Tcons (tptr (Tstruct _subset noattr)) (Tcons tint Tnil)) tint cc_default)) ((Etempvar _subsets (tptr (Tstruct _subset noattr))) :: (Etempvar _p tint) :: nil)) (Sset _p0 (Etempvar _t'1 tint))) (Ssequence (Sset _p (Etempvar _p0 tint)) (Sassign (Efield (Ederef (Ebinop Oadd (Etempvar _subsets (tptr (Tstruct _subset noattr))) (Etempvar _i tint) (tptr (Tstruct _subset noattr))) (Tstruct _subset noattr)) _parent tint) (Etempvar _p tint)))) Sskip) (Sreturn (Some (Etempvar _p tint)))))) |}.
imports: Coq(String List ZArith) compcert(Coqlib Integers Floats AST Ctypes Cop Clight Clightdefs)