fact: Definition f_main := {| fn_return := tint; fn_callconv := cc_default; fn_params := nil; fn_vars := nil; fn_temps := ((_t'2, (tptr (Tstruct _Node noattr))) :: (_t'1, (tptr (Tstruct _Node noattr))) :: nil); fn_body := (Ssequence (Ssequence (Sassign (Evar _hd (tptr (Tstruct _Node noattr))) (Eaddrof (Evar _n (Tstruct _Node noattr)) (tptr (Tstruct _Node noattr)))) (Ssequence (Sassign (Efield (Evar _n (Tstruct _Node noattr)) _m (talignas 4%N tint)) (Econst_int (Int.repr 0) tint)) (Ssequence (Ssequence (Sset _t'2 (Evar _hd (tptr (Tstruct _Node noattr)))) (Sassign (Efield (Evar _n (Tstruct _Node noattr)) _l (talignas 3%N (tptr (Tstruct _Node noattr)))) (Etempvar _t'2 (tptr (Tstruct _Node noattr))))) (Ssequence (Sassign (Efield (Evar _n (Tstruct _Node noattr)) _r (tptr (Tstruct _Node noattr))) (Econst_int (Int.repr 0) tint)) (Ssequence (Sset _t'1 (Evar _hd (tptr (Tstruct _Node noattr)))) (Scall None (Evar _mark (Tfunction (Tcons (tptr (Tstruct _Node noattr)) Tnil) tvoid cc_default)) ((Etempvar _t'1 (tptr (Tstruct _Node noattr))) :: nil))))))) (Sreturn (Some (Econst_int (Int.repr 0) tint)))) |}.
imports: Coq(String List ZArith) compcert(Coqlib Integers Floats AST Ctypes Cop Clight Clightdefs)