fact: Definition f_main := {| fn_return := tint; fn_callconv := cc_default; fn_params := ((_argc, tint) :: (_argv, (tptr (tptr tschar))) :: nil); fn_vars := ((_graph, (tarray (tarray tint 8) 8)) :: nil); fn_temps := ((_src, tint) :: (_prev, (tptr tint)) :: (_dist, (tptr tint)) :: (_t'4, (tptr tvoid)) :: (_t'3, (tptr tvoid)) :: (_t'2, tint) :: (_t'1, 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 _src (Ebinop Omod (Etempvar _t'2 tint) (Econst_int (Int.repr 8) tint) tint))) (Ssequence (Scall None (Evar _setup (Tfunction (Tcons (tptr (tarray tint 8)) Tnil) tvoid cc_default)) ((Evar _graph (tarray (tarray tint 8) 8)) :: nil)) (Ssequence (Scall None (Evar _print_graph (Tfunction (Tcons (tptr (tarray tint 8)) (Tcons tint Tnil)) tvoid cc_default)) ((Evar _graph (tarray (tarray tint 8) 8)) :: (Etempvar _src tint) :: nil)) (Ssequence (Ssequence (Scall (Some _t'3) (Evar _mallocN (Tfunction (Tcons tint Tnil) (tptr tvoid) cc_default)) ((Ebinop Omul (Econst_int (Int.repr 8) tint) (Esizeof tint tuint) tuint) :: nil)) (Sset _prev (Etempvar _t'3 (tptr tvoid)))) (Ssequence (Ssequence (Scall (Some _t'4) (Evar _mallocN (Tfunction (Tcons tint Tnil) (tptr tvoid) cc_default)) ((Ebinop Omul (Econst_int (Int.repr 8) tint) (Esizeof tint tuint) tuint) :: nil)) (Sset _dist (Etempvar _t'4 (tptr tvoid)))) (Ssequence (Scall None (Evar _dijkstra (Tfunction (Tcons (tptr (tarray tint 8)) (Tcons tint (Tcons (tptr tint) (Tcons (tptr tint) Tnil)))) tvoid cc_default)) ((Evar _graph (tarray (tarray tint 8) 8)) :: (Etempvar _src tint) :: (Etempvar _dist (tptr tint)) :: (Etempvar _prev (tptr tint)) :: nil)) (Ssequence (Scall None (Evar _getPaths (Tfunction (Tcons tint (Tcons (tptr tint) (Tcons (tptr tint) Tnil))) tvoid cc_default)) ((Etempvar _src tint) :: (Etempvar _dist (tptr tint)) :: (Etempvar _prev (tptr 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)) (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)