fact: Definition f_find := {| fn_return := (tptr (Tstruct _Node noattr)); fn_callconv := cc_default; fn_params := ((_x, (tptr (Tstruct _Node noattr))) :: nil); fn_vars := nil; fn_temps := ((_tmp, (tptr (Tstruct _Node noattr))) :: (_p, (tptr (Tstruct _Node noattr))) :: nil); fn_body := (Ssequence (Sset _tmp (Etempvar _x (tptr (Tstruct _Node noattr)))) (Ssequence (Sset _p (Efield (Ederef (Etempvar _tmp (tptr (Tstruct _Node noattr))) (Tstruct _Node noattr)) _parent (tptr (Tstruct _Node noattr)))) (Ssequence (Swhile (Ebinop One (Etempvar _tmp (tptr (Tstruct _Node noattr))) (Etempvar _p (tptr (Tstruct _Node noattr))) tint) (Ssequence (Sset _tmp (Etempvar _p (tptr (Tstruct _Node noattr)))) (Sset _p (Efield (Ederef (Etempvar _tmp (tptr (Tstruct _Node noattr))) (Tstruct _Node noattr)) _parent (tptr (Tstruct _Node noattr)))))) (Ssequence (Swhile (Ebinop One (Etempvar _x (tptr (Tstruct _Node noattr))) (Etempvar _p (tptr (Tstruct _Node noattr))) tint) (Ssequence (Sset _tmp (Efield (Ederef (Etempvar _x (tptr (Tstruct _Node noattr))) (Tstruct _Node noattr)) _parent (tptr (Tstruct _Node noattr)))) (Ssequence (Sassign (Efield (Ederef (Etempvar _x (tptr (Tstruct _Node noattr))) (Tstruct _Node noattr)) _parent (tptr (Tstruct _Node noattr))) (Etempvar _p (tptr (Tstruct _Node noattr)))) (Sset _x (Etempvar _tmp (tptr (Tstruct _Node noattr))))))) (Sreturn (Some (Etempvar _p (tptr (Tstruct _Node noattr))))))))) |}.
imports: Coq(String List ZArith) compcert(Coqlib Integers Floats AST Ctypes Cop Clight Clightdefs)