fact: Definition f_makeSet := {| fn_return := (tptr (Tstruct _subset noattr)); fn_callconv := cc_default; fn_params := ((_V, tint) :: nil); fn_vars := nil; fn_temps := ((_subsets, (tptr (Tstruct _subset noattr))) :: (_v, tint) :: (_t'1, (tptr tvoid)) :: nil); fn_body := (Ssequence (Ssequence (Scall (Some _t'1) (Evar _mallocN (Tfunction (Tcons tint Tnil) (tptr tvoid) cc_default)) ((Ebinop Omul (Etempvar _V tint) (Esizeof (Tstruct _subset noattr) tulong) tulong) :: nil)) (Sset _subsets (Ecast (Etempvar _t'1 (tptr tvoid)) (tptr (Tstruct _subset noattr))))) (Ssequence (Ssequence (Sset _v (Econst_int (Int.repr 0) tint)) (Sloop (Ssequence (Sifthenelse (Ebinop Olt (Etempvar _v tint) (Etempvar _V tint) tint) Sskip Sbreak) (Ssequence (Sassign (Efield (Ederef (Ebinop Oadd (Etempvar _subsets (tptr (Tstruct _subset noattr))) (Etempvar _v tint) (tptr (Tstruct _subset noattr))) (Tstruct _subset noattr)) _parent tint) (Etempvar _v tint)) (Sassign (Efield (Ederef (Ebinop Oadd (Etempvar _subsets (tptr (Tstruct _subset noattr))) (Etempvar _v tint) (tptr (Tstruct _subset noattr))) (Tstruct _subset noattr)) _rank tuint) (Econst_int (Int.repr 0) tint)))) (Sset _v (Ebinop Oadd (Etempvar _v tint) (Econst_int (Int.repr 1) tint) tint)))) (Sreturn (Some (Etempvar _subsets (tptr (Tstruct _subset noattr))))))) |}.
imports: Coq(String List ZArith) compcert(Coqlib Integers Floats AST Ctypes Cop Clight Clightdefs)