fact: Definition f_dijkstra := {| fn_return := tvoid; fn_callconv := cc_default; fn_params := ((_graph, (tptr tint)) :: (_src, tint) :: (_dist, (tptr tint)) :: (_prev, (tptr tint)) :: nil); fn_vars := nil; fn_temps := ((_temp, (tptr (Tstruct _structItem noattr))) :: (_keys, (tptr tint)) :: (_pq, (tptr (Tstruct _structPQ noattr))) :: (_i, tint) :: (_j, tint) :: (_u, tint) :: (_cost, tint) :: (_t'6, tint) :: (_t'5, tuint) :: (_t'4, tuint) :: (_t'3, (tptr (Tstruct _structPQ noattr))) :: (_t'2, (tptr tvoid)) :: (_t'1, (tptr tvoid)) :: (_t'12, tint) :: (_t'11, tint) :: (_t'10, tint) :: (_t'9, tint) :: (_t'8, tint) :: (_t'7, tint) :: nil); fn_body := (Ssequence (Ssequence (Scall (Some _t'1) (Evar _mallocN (Tfunction (Tcons tint Tnil) (tptr tvoid) cc_default)) ((Esizeof (Tstruct _structItem noattr) tuint) :: nil)) (Sset _temp (Ecast (Etempvar _t'1 (tptr tvoid)) (tptr (Tstruct _structItem noattr))))) (Ssequence (Ssequence (Scall (Some _t'2) (Evar _mallocN (Tfunction (Tcons tint Tnil) (tptr tvoid) cc_default)) ((Ebinop Omul (Econst_int (Int.repr 8) tint) (Esizeof tint tuint) tuint) :: nil)) (Sset _keys (Etempvar _t'2 (tptr tvoid)))) (Ssequence (Ssequence (Scall (Some _t'3) (Evar _pq_make (Tfunction (Tcons tuint Tnil) (tptr (Tstruct _structPQ noattr)) cc_default)) ((Econst_int (Int.repr 8) tint) :: nil)) (Sset _pq (Etempvar _t'3 (tptr (Tstruct _structPQ noattr))))) (Ssequence (Ssequence (Sset _i (Econst_int (Int.repr 0) tint)) (Sloop (Ssequence (Sifthenelse (Ebinop Olt (Etempvar _i tint) (Econst_int (Int.repr 8) tint) tint) Sskip Sbreak) (Ssequence (Sassign (Ederef (Ebinop Oadd (Etempvar _dist (tptr tint)) (Etempvar _i tint) (tptr tint)) tint) (Econst_int (Int.repr 2147483647) tint)) (Ssequence (Sassign (Ederef (Ebinop Oadd (Etempvar _prev (tptr tint)) (Etempvar _i tint) (tptr tint)) tint) (Econst_int (Int.repr 2147483647) tint)) (Ssequence (Scall (Some _t'4) (Evar _pq_insert_nc (Tfunction (Tcons (tptr (Tstruct _structPQ noattr)) (Tcons tint (Tcons tint Tnil))) tuint cc_default)) ((Etempvar _pq (tptr (Tstruct _structPQ noattr))) :: (Econst_int (Int.repr 2147483647) tint) :: (Etempvar _i tint) :: nil)) (Sassign (Ederef (Ebinop Oadd (Etempvar _keys (tptr tint)) (Etempvar _i tint) (tptr tint)) tint) (Etempvar _t'4 tuint)))))) (Sset _i (Ebinop Oadd (Etempvar _i tint) (Econst_int (Int.repr 1) tint) tint)))) (Ssequence (Sassign (Ederef (Ebinop Oadd (Etempvar _dist (tptr tint)) (Etempvar _src tint) (tptr tint)) tint) (Econst_int (Int.repr 0) tint)) (Ssequence (Sassign (Ederef (Ebinop Oadd (Etempvar _prev (tptr tint)) (Etempvar _src tint) (tptr tint)) tint) (Etempvar _src tint)) (Ssequence (Ssequence (Sset _t'12 (Ederef (Ebinop Oadd (Etempvar _keys (tptr tint)) (Etempvar _src tint) (tptr tint)) tint)) (Scall None (Evar _pq_edit_priority (Tfunction (Tcons (tptr (Tstruct _structPQ noattr)) (Tcons tint (Tcons tint Tnil))) tvoid cc_default)) ((Etempvar _pq (tptr (Tstruct _structPQ noattr))) :: (Etempvar _t'12 tint) :: (Econst_int (Int.repr 0) tint) :: nil))) (Ssequence (Sloop (Ssequence (Ssequence (Scall (Some _t'5) (Evar _pq_size (Tfunction (Tcons (tptr (Tstruct _structPQ noattr)) Tnil) tuint cc_default)) ((Etempvar _pq (tptr (Tstruct _structPQ noattr))) :: nil)) (Sifthenelse (Ebinop Ogt (Etempvar _t'5 tuint) (Econst_int (Int.repr 0) tint) tint) Sskip Sbreak)) (Ssequence (Scall None (Evar _pq_remove_min_nc (Tfunction (Tcons (tptr (Tstruct _structPQ noattr)) (Tcons (tptr (Tstruct _structItem noattr)) Tnil)) tvoid cc_default)) ((Etempvar _pq (tptr (Tstruct _structPQ noattr))) :: (Etempvar _temp (tptr (Tstruct _structItem noattr))) :: nil)) (Ssequence (Sset _u (Efield (Ederef (Etempvar _temp (tptr (Tstruct _structItem noattr))) (Tstruct _structItem noattr)) _data tint)) (Ssequence (Sset _i (Econst_int (Int.repr 0) tint)) (Sloop (Ssequence (Sifthenelse (Ebinop Olt (Etempvar _i tint) (Econst_int (Int.repr 8) tint) tint) Sskip Sbreak) (Ssequence (Ssequence (Scall (Some _t'6) (Evar _getCell (Tfunction (Tcons (tptr tint) (Tcons tint (Tcons tint Tnil))) tint cc_default)) ((Etempvar _graph (tptr tint)) :: (Etempvar _u tint) :: (Etempvar _i tint) :: nil)) (Sset _cost (Etempvar _t'6 tint))) (Sifthenelse (Ebinop Olt (Etempvar _cost tint) (Econst_int (Int.repr 2147483647) tint) tint) (Ssequence (Sset _t'7 (Ederef (Ebinop Oadd (Etempvar _dist (tptr tint)) (Etempvar _i tint) (tptr tint)) tint)) (Ssequence (Sset _t'8 (Ederef (Ebinop Oadd (Etempvar _dist (tptr tint)) (Etempvar _u tint) (tptr tint)) tint)) (Sifthenelse (Ebinop Ogt (Etempvar _t'7 tint) (Ebinop Oadd (Etempvar _t'8 tint) (Etempvar _cost tint) tint) tint) (Ssequence (Ssequence (Sset _t'11 (Ederef (Ebinop Oadd (Etempvar _dist (tptr tint)) (Etempvar _u tint) (tptr tint)) tint)) (Sassign (Ederef (Ebinop Oadd (Etempvar _dist (tptr tint)) (Etempvar _i tint) (tptr tint)) tint) (Ebinop Oadd (Etempvar _t'11 tint) (Etempvar _cost tint) tint))) (Ssequence (Sassign (Ederef (Ebinop Oadd (Etempvar _prev (tptr tint)) (Etempvar _i tint) (tptr tint)) tint) (Etempvar _u tint)) (Ssequence (Sset _t'9 (Ederef (Ebinop Oadd (Etempvar _keys (tptr tint)) (Etempvar _i tint) (tptr tint)) tint)) (Ssequence (Sset _t'10 (Ederef (Ebinop Oadd (Etempvar _dist (tptr tint)) (Etempvar _i tint) (tptr tint)) tint)) (Scall None (Evar _pq_edit_priority (Tfunction (Tcons (tptr (Tstruct _structPQ noattr)) (Tcons tint (Tcons tint Tnil))) tvoid cc_default)) ((Etempvar _pq (tptr (Tstruct _structPQ noattr))) :: (Etempvar _t'9 tint) :: (Etempvar _t'10 tint) :: nil)))))) Sskip))) Sskip))) (Sset _i (Ebinop Oadd (Etempvar _i tint) (Econst_int (Int.repr 1) tint) tint))))))) Sskip) (Ssequence (Scall None (Evar _freeN (Tfunction (Tcons (tptr tvoid) Tnil) tvoid cc_default)) ((Etempvar _temp (tptr (Tstruct _structItem noattr))) :: nil)) (Ssequence (Scall None (Evar _pq_free (Tfunction (Tcons (tptr (Tstruct _structPQ noattr)) Tnil) tvoid cc_default)) ((Etempvar _pq (tptr (Tstruct _structPQ noattr))) :: nil)) (Ssequence (Scall None (Evar _freeN (Tfunction (Tcons (tptr tvoid) Tnil) tvoid cc_default)) ((Etempvar _keys (tptr tint)) :: nil)) (Sreturn None)))))))))))) |}.
imports: Coq(String List ZArith) compcert(Coqlib Integers Floats AST Ctypes Cop Clight Clightdefs)