fact: Definition f_main := {| fn_return := tint; fn_callconv := cc_default; fn_params := ((_argc, tint) :: (_argv, (tptr (tptr tschar))) :: nil); fn_vars := nil; fn_temps := ((_i, tint) :: (_size, tint) :: (_inf, tint) :: (_src, tint) :: (_graph, (tptr (tptr tint))) :: (_prev, (tptr tint)) :: (_dist, (tptr tint)) :: (_t'7, (tptr tvoid)) :: (_t'6, (tptr tvoid)) :: (_t'5, (tptr tvoid)) :: (_t'4, (tptr tvoid)) :: (_t'3, tint) :: (_t'2, tint) :: (_t'1, tint) :: (_t'8, (tptr tint)) :: nil); fn_body := (Ssequence (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 (Ssequence (Scall (Some _t'2) (Evar _rand (Tfunction Tnil tint cc_default)) nil) (Sset _size (Ebinop Oadd (Econst_int (Int.repr 1) tint) (Ebinop Omod (Etempvar _t'2 tint) (Econst_int (Int.repr 20) tint) tint) tint))) (Ssequence (Sset _inf (Ebinop Osub (Econst_int (Int.repr 2147483647) tint) (Ebinop Odiv (Econst_int (Int.repr 2147483647) tint) (Etempvar _size tint) tint) tint)) (Ssequence (Ssequence (Scall (Some _t'3) (Evar _rand (Tfunction Tnil tint cc_default)) nil) (Sset _src (Ebinop Omod (Etempvar _t'3 tint) (Etempvar _size tint) tint))) (Ssequence (Ssequence (Scall (Some _t'4) (Evar _malloc (Tfunction (Tcons tuint Tnil) (tptr tvoid) cc_default)) ((Ebinop Omul (Etempvar _size tint) (Esizeof (tptr tint) tuint) tuint) :: nil)) (Sset _graph (Etempvar _t'4 (tptr tvoid)))) (Ssequence (Ssequence (Sset _i (Econst_int (Int.repr 0) tint)) (Sloop (Ssequence (Sifthenelse (Ebinop Olt (Etempvar _i tint) (Etempvar _size tint) tint) Sskip Sbreak) (Ssequence (Scall (Some _t'5) (Evar _malloc (Tfunction (Tcons tuint Tnil) (tptr tvoid) cc_default)) ((Ebinop Omul (Etempvar _size tint) (Esizeof tint tuint) tuint) :: nil)) (Sassign (Ederef (Ebinop Oadd (Etempvar _graph (tptr (tptr tint))) (Etempvar _i tint) (tptr (tptr tint))) (tptr tint)) (Etempvar _t'5 (tptr tvoid))))) (Sset _i (Ebinop Oadd (Etempvar _i tint) (Econst_int (Int.repr 1) tint) tint)))) (Ssequence (Scall None (Evar _setup (Tfunction (Tcons (tptr (tptr tint)) (Tcons tint (Tcons tint Tnil))) tvoid cc_default)) ((Etempvar _graph (tptr (tptr tint))) :: (Etempvar _size tint) :: (Etempvar _inf tint) :: nil)) (Ssequence (Scall None (Evar _print_graph (Tfunction (Tcons (tptr (tptr tint)) (Tcons tint (Tcons tint (Tcons tint Tnil)))) tvoid cc_default)) ((Etempvar _graph (tptr (tptr tint))) :: (Etempvar _size tint) :: (Etempvar _inf tint) :: (Etempvar _src tint) :: nil)) (Ssequence (Ssequence (Scall (Some _t'6) (Evar _malloc (Tfunction (Tcons tuint Tnil) (tptr tvoid) cc_default)) ((Ebinop Omul (Etempvar _size tint) (Esizeof tint tuint) tuint) :: nil)) (Sset _prev (Etempvar _t'6 (tptr tvoid)))) (Ssequence (Ssequence (Scall (Some _t'7) (Evar _malloc (Tfunction (Tcons tuint Tnil) (tptr tvoid) cc_default)) ((Ebinop Omul (Etempvar _size tint) (Esizeof tint tuint) tuint) :: nil)) (Sset _dist (Etempvar _t'7 (tptr tvoid)))) (Ssequence (Scall None (Evar _dijkstra (Tfunction (Tcons (tptr (tptr tint)) (Tcons tint (Tcons (tptr tint) (Tcons (tptr tint) (Tcons tint (Tcons tint Tnil)))))) tvoid cc_default)) ((Etempvar _graph (tptr (tptr tint))) :: (Etempvar _src tint) :: (Etempvar _dist (tptr tint)) :: (Etempvar _prev (tptr tint)) :: (Etempvar _size tint) :: (Etempvar _inf tint) :: nil)) (Ssequence (Scall None (Evar _getPaths (Tfunction (Tcons tint (Tcons (tptr tint) (Tcons (tptr tint) (Tcons tint (Tcons tint Tnil))))) tvoid cc_default)) ((Etempvar _src tint) :: (Etempvar _dist (tptr tint)) :: (Etempvar _prev (tptr tint)) :: (Etempvar _size tint) :: (Etempvar _inf tint) :: nil)) (Ssequence (Scall None (Evar _free (Tfunction (Tcons (tptr tvoid) Tnil) tvoid cc_default)) ((Etempvar _prev (tptr tint)) :: nil)) (Ssequence (Scall None (Evar _free (Tfunction (Tcons (tptr tvoid) Tnil) tvoid cc_default)) ((Etempvar _dist (tptr tint)) :: nil)) (Ssequence (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 _t'8 (Ederef (Ebinop Oadd (Etempvar _graph (tptr (tptr tint))) (Etempvar _i tint) (tptr (tptr tint))) (tptr tint))) (Scall None (Evar _free (Tfunction (Tcons (tptr tvoid) Tnil) tvoid cc_default)) ((Etempvar _t'8 (tptr tint)) :: nil)))) (Sset _i (Ebinop Oadd (Etempvar _i tint) (Econst_int (Int.repr 1) tint) tint)))) (Ssequence (Scall None (Evar _free (Tfunction (Tcons (tptr tvoid) Tnil) tvoid cc_default)) ((Etempvar _graph (tptr (tptr tint))) :: nil)) (Sreturn (Some (Econst_int (Int.repr 0) tint))))))))))))))))))) (Sreturn (Some (Econst_int (Int.repr 0) tint)))) |}.
imports: Coq(String List ZArith) compcert(Coqlib Integers Floats AST Ctypes Cop Clight Clightdefs)