fact: Definition f_copy := {| fn_return := (tptr (Tstruct _Node noattr)); fn_callconv := cc_default; fn_params := ((_x, (tptr (Tstruct _Node noattr))) :: nil); fn_vars := nil; fn_temps := ((_l, (tptr (Tstruct _Node noattr))) :: (_r, (tptr (Tstruct _Node noattr))) :: (_x0, (tptr (Tstruct _Node noattr))) :: (_l0, (tptr (Tstruct _Node noattr))) :: (_r0, (tptr (Tstruct _Node noattr))) :: (_t'3, (tptr (Tstruct _Node noattr))) :: (_t'2, (tptr (Tstruct _Node noattr))) :: (_t'1, (tptr tvoid)) :: nil); fn_body := (Ssequence (Sifthenelse (Ebinop Oeq (Etempvar _x (tptr (Tstruct _Node noattr))) (Ecast (Econst_int (Int.repr 0) tint) (tptr tvoid)) tint) (Sreturn (Some (Econst_int (Int.repr 0) tint))) Sskip) (Ssequence (Sset _x0 (Efield (Ederef (Etempvar _x (tptr (Tstruct _Node noattr))) (Tstruct _Node noattr)) _m (talignas 4%N (tptr (Tstruct _Node noattr))))) (Ssequence (Sifthenelse (Ebinop One (Etempvar _x0 (tptr (Tstruct _Node noattr))) (Ecast (Econst_int (Int.repr 0) tint) (tptr tvoid)) tint) (Sreturn (Some (Etempvar _x0 (tptr (Tstruct _Node noattr))))) Sskip) (Ssequence (Ssequence (Scall (Some _t'1) (Evar _mallocN (Tfunction (Tcons tint Tnil) (tptr tvoid) cc_default)) ((Esizeof (Tstruct _Node noattr) tulong) :: nil)) (Sset _x0 (Ecast (Etempvar _t'1 (tptr tvoid)) (tptr (Tstruct _Node noattr))))) (Ssequence (Sset _l (Efield (Ederef (Etempvar _x (tptr (Tstruct _Node noattr))) (Tstruct _Node noattr)) _l (talignas 3%N (tptr (Tstruct _Node noattr))))) (Ssequence (Sset _r (Efield (Ederef (Etempvar _x (tptr (Tstruct _Node noattr))) (Tstruct _Node noattr)) _r (tptr (Tstruct _Node noattr)))) (Ssequence (Sassign (Efield (Ederef (Etempvar _x (tptr (Tstruct _Node noattr))) (Tstruct _Node noattr)) _m (talignas 4%N (tptr (Tstruct _Node noattr)))) (Etempvar _x0 (tptr (Tstruct _Node noattr)))) (Ssequence (Sassign (Efield (Ederef (Etempvar _x0 (tptr (Tstruct _Node noattr))) (Tstruct _Node noattr)) _m (talignas 4%N (tptr (Tstruct _Node noattr)))) (Econst_int (Int.repr 0) tint)) (Ssequence (Ssequence (Scall (Some _t'2) (Evar _copy (Tfunction (Tcons (tptr (Tstruct _Node noattr)) Tnil) (tptr (Tstruct _Node noattr)) cc_default)) ((Etempvar _l (tptr (Tstruct _Node noattr))) :: nil)) (Sset _l0 (Etempvar _t'2 (tptr (Tstruct _Node noattr))))) (Ssequence (Sassign (Efield (Ederef (Etempvar _x0 (tptr (Tstruct _Node noattr))) (Tstruct _Node noattr)) _l (talignas 3%N (tptr (Tstruct _Node noattr)))) (Etempvar _l0 (tptr (Tstruct _Node noattr)))) (Ssequence (Ssequence (Scall (Some _t'3) (Evar _copy (Tfunction (Tcons (tptr (Tstruct _Node noattr)) Tnil) (tptr (Tstruct _Node noattr)) cc_default)) ((Etempvar _r (tptr (Tstruct _Node noattr))) :: nil)) (Sset _r0 (Etempvar _t'3 (tptr (Tstruct _Node noattr))))) (Ssequence (Sassign (Efield (Ederef (Etempvar _x0 (tptr (Tstruct _Node noattr))) (Tstruct _Node noattr)) _r (tptr (Tstruct _Node noattr))) (Etempvar _r0 (tptr (Tstruct _Node noattr)))) (Sreturn (Some (Etempvar _x0 (tptr (Tstruct _Node noattr))))))))))))))))) |}.
imports: Coq(String List ZArith) compcert(Coqlib Integers Floats AST Ctypes Cop Clight Clightdefs)