fact: Definition f_Union := {| fn_return := tvoid; fn_callconv := cc_default; fn_params := ((_subsets, (tptr (Tstruct _subset noattr))) :: (_x, tint) :: (_y, tint) :: nil); fn_vars := nil; fn_temps := ((_xroot, tint) :: (_yroot, tint) :: (_xRank, tuint) :: (_yRank, tuint) :: (_t'2, tint) :: (_t'1, tint) :: nil); fn_body := (Ssequence (Ssequence (Scall (Some _t'1) (Evar _find (Tfunction (Tcons (tptr (Tstruct _subset noattr)) (Tcons tint Tnil)) tint cc_default)) ((Etempvar _subsets (tptr (Tstruct _subset noattr))) :: (Etempvar _x tint) :: nil)) (Sset _xroot (Etempvar _t'1 tint))) (Ssequence (Ssequence (Scall (Some _t'2) (Evar _find (Tfunction (Tcons (tptr (Tstruct _subset noattr)) (Tcons tint Tnil)) tint cc_default)) ((Etempvar _subsets (tptr (Tstruct _subset noattr))) :: (Etempvar _y tint) :: nil)) (Sset _yroot (Etempvar _t'2 tint))) (Ssequence (Sifthenelse (Ebinop Oeq (Etempvar _xroot tint) (Etempvar _yroot tint) tint) (Sreturn None) Sskip) (Ssequence (Sset _xRank (Efield (Ederef (Ebinop Oadd (Etempvar _subsets (tptr (Tstruct _subset noattr))) (Etempvar _xroot tint) (tptr (Tstruct _subset noattr))) (Tstruct _subset noattr)) _rank tuint)) (Ssequence (Sset _yRank (Efield (Ederef (Ebinop Oadd (Etempvar _subsets (tptr (Tstruct _subset noattr))) (Etempvar _yroot tint) (tptr (Tstruct _subset noattr))) (Tstruct _subset noattr)) _rank tuint)) (Sifthenelse (Ebinop Olt (Etempvar _xRank tuint) (Etempvar _yRank tuint) tint) (Sassign (Efield (Ederef (Ebinop Oadd (Etempvar _subsets (tptr (Tstruct _subset noattr))) (Etempvar _xroot tint) (tptr (Tstruct _subset noattr))) (Tstruct _subset noattr)) _parent tint) (Etempvar _yroot tint)) (Sifthenelse (Ebinop Ogt (Etempvar _xRank tuint) (Etempvar _yRank tuint) tint) (Sassign (Efield (Ederef (Ebinop Oadd (Etempvar _subsets (tptr (Tstruct _subset noattr))) (Etempvar _yroot tint) (tptr (Tstruct _subset noattr))) (Tstruct _subset noattr)) _parent tint) (Etempvar _xroot tint)) (Ssequence (Sassign (Efield (Ederef (Ebinop Oadd (Etempvar _subsets (tptr (Tstruct _subset noattr))) (Etempvar _yroot tint) (tptr (Tstruct _subset noattr))) (Tstruct _subset noattr)) _parent tint) (Etempvar _xroot tint)) (Sassign (Efield (Ederef (Ebinop Oadd (Etempvar _subsets (tptr (Tstruct _subset noattr))) (Etempvar _xroot tint) (tptr (Tstruct _subset noattr))) (Tstruct _subset noattr)) _rank tuint) (Ebinop Oadd (Etempvar _xRank tuint) (Econst_int (Int.repr 1) tint) tuint)))))))))) |}.
imports: Coq(String List ZArith) compcert(Coqlib Integers Floats AST Ctypes Cop Clight Clightdefs)