fact: Definition f_append := {| fn_return := (tptr (Tstruct _list noattr)); fn_callconv := cc_default; fn_params := ((_x, (tptr (Tstruct _list noattr))) :: (_y, (tptr (Tstruct _list noattr))) :: nil); fn_vars := nil; fn_temps := ((_t, (tptr (Tstruct _list noattr))) :: (_u, (tptr (Tstruct _list noattr))) :: nil); fn_body := (Sifthenelse (Ebinop Oeq (Etempvar _x (tptr (Tstruct _list noattr))) (Ecast (Econst_int (Int.repr 0) tint) (tptr tvoid)) tint) (Sreturn (Some (Etempvar _y (tptr (Tstruct _list noattr))))) (Ssequence (Sset _t (Etempvar _x (tptr (Tstruct _list noattr)))) (Ssequence (Sset _u (Efield (Ederef (Etempvar _t (tptr (Tstruct _list noattr))) (Tstruct _list noattr)) _tail (tptr (Tstruct _list noattr)))) (Ssequence (Swhile (Ebinop One (Etempvar _u (tptr (Tstruct _list noattr))) (Ecast (Econst_int (Int.repr 0) tint) (tptr tvoid)) tint) (Ssequence (Sset _t (Etempvar _u (tptr (Tstruct _list noattr)))) (Sset _u (Efield (Ederef (Etempvar _t (tptr (Tstruct _list noattr))) (Tstruct _list noattr)) _tail (tptr (Tstruct _list noattr)))))) (Ssequence (Sassign (Efield (Ederef (Etempvar _t (tptr (Tstruct _list noattr))) (Tstruct _list noattr)) _tail (tptr (Tstruct _list noattr))) (Etempvar _y (tptr (Tstruct _list noattr)))) (Sreturn (Some (Etempvar _x (tptr (Tstruct _list noattr)))))))))) |}.
imports: Coq(String List ZArith) compcert(Coqlib Integers Floats AST Ctypes Cop Clight Clightdefs)