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