fact: Definition f_spanning := {| fn_return := tvoid; 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))) :: (_root_mark, tint) :: nil); fn_body := (Ssequence (Sset _l (Efield (Ederef (Etempvar _x (tptr (Tstruct _Node noattr))) (Tstruct _Node noattr)) _l (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 tint) (Econst_int (Int.repr 1) tint)) (Ssequence (Sifthenelse (Etempvar _l (tptr (Tstruct _Node noattr))) (Ssequence (Sset _root_mark (Efield (Ederef (Etempvar _l (tptr (Tstruct _Node noattr))) (Tstruct _Node noattr)) _m tint)) (Sifthenelse (Ebinop Oeq (Etempvar _root_mark tint) (Econst_int (Int.repr 0) tint) tint) (Scall None (Evar _spanning (Tfunction (Tcons (tptr (Tstruct _Node noattr)) Tnil) tvoid cc_default)) ((Etempvar _l (tptr (Tstruct _Node noattr))) :: nil)) (Sassign (Efield (Ederef (Etempvar _x (tptr (Tstruct _Node noattr))) (Tstruct _Node noattr)) _l (tptr (Tstruct _Node noattr))) (Econst_int (Int.repr 0) tint)))) Sskip) (Sifthenelse (Etempvar _r (tptr (Tstruct _Node noattr))) (Ssequence (Sset _root_mark (Efield (Ederef (Etempvar _r (tptr (Tstruct _Node noattr))) (Tstruct _Node noattr)) _m tint)) (Sifthenelse (Ebinop Oeq (Etempvar _root_mark tint) (Econst_int (Int.repr 0) tint) tint) (Scall None (Evar _spanning (Tfunction (Tcons (tptr (Tstruct _Node noattr)) Tnil) tvoid cc_default)) ((Etempvar _r (tptr (Tstruct _Node noattr))) :: nil)) (Sassign (Efield (Ederef (Etempvar _x (tptr (Tstruct _Node noattr))) (Tstruct _Node noattr)) _r (tptr (Tstruct _Node noattr))) (Econst_int (Int.repr 0) tint)))) Sskip))))) |}.
imports: Coq(String List ZArith) compcert(Coqlib Integers Floats AST Ctypes Cop Clight Clightdefs)