fact: Definition f_setup := {| fn_return := tvoid; fn_callconv := cc_default; fn_params := ((_graph, (tptr (tptr tint))) :: (_size, tint) :: (_inf, tint) :: nil); fn_vars := nil; fn_temps := ((_i, tint) :: (_j, tint) :: (_random, tint) :: (_t'4, tint) :: (_t'3, tint) :: (_t'2, tint) :: (_t'1, tint) :: (_t'5, (tptr tint)) :: nil); fn_body := (Ssequence (Ssequence (Scall (Some _t'1) (Evar _time (Tfunction (Tcons (tptr tint) Tnil) tint cc_default)) ((Ecast (Econst_int (Int.repr 0) tint) (tptr tvoid)) :: nil)) (Scall None (Evar _srand (Tfunction (Tcons tuint Tnil) tvoid cc_default)) ((Ecast (Etempvar _t'1 tint) tuint) :: nil))) (Ssequence (Sset _i (Econst_int (Int.repr 0) tint)) (Sloop (Ssequence (Sifthenelse (Ebinop Olt (Etempvar _i tint) (Etempvar _size tint) tint) Sskip Sbreak) (Ssequence (Sset _j (Econst_int (Int.repr 0) tint)) (Sloop (Ssequence (Sifthenelse (Ebinop Ole (Etempvar _j tint) (Etempvar _size tint) tint) Sskip Sbreak) (Ssequence (Ssequence (Scall (Some _t'2) (Evar _rand (Tfunction Tnil tint cc_default)) nil) (Sset _random (Ebinop Omod (Etempvar _t'2 tint) (Ebinop Omul (Econst_int (Int.repr 3) tint) (Econst_int (Int.repr 50) tint) tint) tint))) (Ssequence (Sifthenelse (Ebinop Oeq (Etempvar _i tint) (Etempvar _j tint) tint) (Sset _t'3 (Ecast (Econst_int (Int.repr 0) tint) tint)) (Sifthenelse (Ebinop Ogt (Etempvar _random tint) (Econst_int (Int.repr 50) tint) tint) (Ssequence (Sset _t'4 (Ecast (Etempvar _inf tint) tint)) (Sset _t'3 (Ecast (Etempvar _t'4 tint) tint))) (Ssequence (Sset _t'4 (Ecast (Etempvar _random tint) tint)) (Sset _t'3 (Ecast (Etempvar _t'4 tint) tint))))) (Ssequence (Sset _t'5 (Ederef (Ebinop Oadd (Etempvar _graph (tptr (tptr tint))) (Etempvar _i tint) (tptr (tptr tint))) (tptr tint))) (Sassign (Ederef (Ebinop Oadd (Etempvar _t'5 (tptr tint)) (Etempvar _j tint) (tptr tint)) tint) (Etempvar _t'3 tint)))))) (Sset _j (Ebinop Oadd (Etempvar _j tint) (Econst_int (Int.repr 1) tint) tint))))) (Sset _i (Ebinop Oadd (Etempvar _i tint) (Econst_int (Int.repr 1) tint) tint))))) |}.
imports: Coq(String List ZArith) compcert(Coqlib Integers Floats AST Ctypes Cop Clight Clightdefs)