fact: Definition f_kruskal := {| fn_return := (tptr (Tstruct _graph noattr)); fn_callconv := cc_default; fn_params := ((_graph__1, (tptr (Tstruct _graph noattr))) :: nil); fn_vars := nil; fn_temps := ((_graph_V, tint) :: (_graph_E, tint) :: (_subsets, (tptr (Tstruct _subset noattr))) :: (_mst, (tptr (Tstruct _graph noattr))) :: (_i, tint) :: (_u, tint) :: (_v, tint) :: (_ufind, tint) :: (_vfind, tint) :: (_w, tint) :: (_t'4, tint) :: (_t'3, tint) :: (_t'2, (tptr (Tstruct _graph noattr))) :: (_t'1, (tptr (Tstruct _subset noattr))) :: (_t'11, (tptr (Tstruct _edge noattr))) :: (_t'10, (tptr (Tstruct _edge noattr))) :: (_t'9, (tptr (Tstruct _edge noattr))) :: (_t'8, (tptr (Tstruct _edge noattr))) :: (_t'7, tint) :: (_t'6, (tptr (Tstruct _edge noattr))) :: (_t'5, tint) :: nil); fn_body := (Ssequence (Sset _graph_V (Efield (Ederef (Etempvar _graph__1 (tptr (Tstruct _graph noattr))) (Tstruct _graph noattr)) _V tint)) (Ssequence (Sset _graph_E (Efield (Ederef (Etempvar _graph__1 (tptr (Tstruct _graph noattr))) (Tstruct _graph noattr)) _E tint)) (Ssequence (Ssequence (Scall (Some _t'1) (Evar _makeSet (Tfunction (Tcons tint Tnil) (tptr (Tstruct _subset noattr)) cc_default)) ((Etempvar _graph_V tint) :: nil)) (Sset _subsets (Etempvar _t'1 (tptr (Tstruct _subset noattr))))) (Ssequence (Ssequence (Scall (Some _t'2) (Evar _init_empty_graph (Tfunction Tnil (tptr (Tstruct _graph noattr)) cc_default)) nil) (Sset _mst (Etempvar _t'2 (tptr (Tstruct _graph noattr))))) (Ssequence (Sassign (Efield (Ederef (Etempvar _mst (tptr (Tstruct _graph noattr))) (Tstruct _graph noattr)) _V tint) (Etempvar _graph_V tint)) (Ssequence (Ssequence (Sset _t'11 (Efield (Ederef (Etempvar _graph__1 (tptr (Tstruct _graph noattr))) (Tstruct _graph noattr)) _edge_list (tptr (Tstruct _edge noattr)))) (Scall None (Evar _heapsort (Tfunction (Tcons (tptr (Tstruct _edge noattr)) (Tcons tint Tnil)) tvoid cc_default)) ((Etempvar _t'11 (tptr (Tstruct _edge noattr))) :: (Etempvar _graph_E tint) :: nil))) (Ssequence (Ssequence (Sset _i (Econst_int (Int.repr 0) tint)) (Sloop (Ssequence (Sifthenelse (Ebinop Olt (Etempvar _i tint) (Etempvar _graph_E tint) tint) Sskip Sbreak) (Ssequence (Ssequence (Sset _t'10 (Efield (Ederef (Etempvar _graph__1 (tptr (Tstruct _graph noattr))) (Tstruct _graph noattr)) _edge_list (tptr (Tstruct _edge noattr)))) (Sset _u (Efield (Ederef (Ebinop Oadd (Etempvar _t'10 (tptr (Tstruct _edge noattr))) (Etempvar _i tint) (tptr (Tstruct _edge noattr))) (Tstruct _edge noattr)) _src tint))) (Ssequence (Ssequence (Sset _t'9 (Efield (Ederef (Etempvar _graph__1 (tptr (Tstruct _graph noattr))) (Tstruct _graph noattr)) _edge_list (tptr (Tstruct _edge noattr)))) (Sset _v (Efield (Ederef (Ebinop Oadd (Etempvar _t'9 (tptr (Tstruct _edge noattr))) (Etempvar _i tint) (tptr (Tstruct _edge noattr))) (Tstruct _edge noattr)) _dst tint))) (Ssequence (Ssequence (Scall (Some _t'3) (Evar _find (Tfunction (Tcons (tptr (Tstruct _subset noattr)) (Tcons tint Tnil)) tint cc_default)) ((Etempvar _subsets (tptr (Tstruct _subset noattr))) :: (Etempvar _u tint) :: nil)) (Sset _ufind (Etempvar _t'3 tint))) (Ssequence (Ssequence (Scall (Some _t'4) (Evar _find (Tfunction (Tcons (tptr (Tstruct _subset noattr)) (Tcons tint Tnil)) tint cc_default)) ((Etempvar _subsets (tptr (Tstruct _subset noattr))) :: (Etempvar _v tint) :: nil)) (Sset _vfind (Etempvar _t'4 tint))) (Sifthenelse (Ebinop One (Etempvar _ufind tint) (Etempvar _vfind tint) tint) (Ssequence (Ssequence (Sset _t'8 (Efield (Ederef (Etempvar _graph__1 (tptr (Tstruct _graph noattr))) (Tstruct _graph noattr)) _edge_list (tptr (Tstruct _edge noattr)))) (Sset _w (Efield (Ederef (Ebinop Oadd (Etempvar _t'8 (tptr (Tstruct _edge noattr))) (Etempvar _i tint) (tptr (Tstruct _edge noattr))) (Tstruct _edge noattr)) _weight tint))) (Ssequence (Ssequence (Sset _t'6 (Efield (Ederef (Etempvar _mst (tptr (Tstruct _graph noattr))) (Tstruct _graph noattr)) _edge_list (tptr (Tstruct _edge noattr)))) (Ssequence (Sset _t'7 (Efield (Ederef (Etempvar _mst (tptr (Tstruct _graph noattr))) (Tstruct _graph noattr)) _E tint)) (Scall None (Evar _fill_edge (Tfunction (Tcons (tptr (Tstruct _edge noattr)) (Tcons tint (Tcons tint (Tcons tint Tnil)))) tvoid cc_default)) ((Ebinop Oadd (Etempvar _t'6 (tptr (Tstruct _edge noattr))) (Etempvar _t'7 tint) (tptr (Tstruct _edge noattr))) :: (Etempvar _w tint) :: (Etempvar _u tint) :: (Etempvar _v tint) :: nil)))) (Ssequence (Ssequence (Sset _t'5 (Efield (Ederef (Etempvar _mst (tptr (Tstruct _graph noattr))) (Tstruct _graph noattr)) _E tint)) (Sassign (Efield (Ederef (Etempvar _mst (tptr (Tstruct _graph noattr))) (Tstruct _graph noattr)) _E tint) (Ebinop Oadd (Etempvar _t'5 tint) (Econst_int (Int.repr 1) tint) tint))) (Scall None (Evar _Union (Tfunction (Tcons (tptr (Tstruct _subset noattr)) (Tcons tint (Tcons tint Tnil))) tvoid cc_default)) ((Etempvar _subsets (tptr (Tstruct _subset noattr))) :: (Etempvar _u tint) :: (Etempvar _v tint) :: nil))))) Sskip)))))) (Sset _i (Ebinop Oadd (Etempvar _i tint) (Econst_int (Int.repr 1) tint) tint)))) (Ssequence (Scall None (Evar _freeSet (Tfunction (Tcons (tptr (Tstruct _subset noattr)) Tnil) tvoid cc_default)) ((Etempvar _subsets (tptr (Tstruct _subset noattr))) :: nil)) (Sreturn (Some (Etempvar _mst (tptr (Tstruct _graph noattr))))))))))))) |}.
imports: Coq(String List ZArith) compcert(Coqlib Integers Floats AST Ctypes Cop Clight Clightdefs)