diff options
author | xleroy <xleroy@fca1b0fc-160b-0410-b1d3-a4f43f01ea2e> | 2006-09-11 14:24:49 +0000 |
---|---|---|
committer | xleroy <xleroy@fca1b0fc-160b-0410-b1d3-a4f43f01ea2e> | 2006-09-11 14:24:49 +0000 |
commit | 5e8237152cad0cf08d3eea0d5de8cd8bc499df69 (patch) | |
tree | c95657bfdfa099dde79a79dcf653cee2a53fcca6 /caml | |
parent | 035e249ab21833170f6f3c71f5767c88d457efca (diff) |
Code de timing
git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@93 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
Diffstat (limited to 'caml')
-rw-r--r-- | caml/Camlcoq.ml | 26 |
1 files changed, 26 insertions, 0 deletions
diff --git a/caml/Camlcoq.ml b/caml/Camlcoq.ml index ab111c1..c2115df 100644 --- a/caml/Camlcoq.ml +++ b/caml/Camlcoq.ml @@ -100,3 +100,29 @@ let array_of_coqlist = function | Coq_cons(hd, tl) -> a.(i) <- hd; fill (i + 1) tl in fill 1 tl +(* Timing facility *) + +(* +let timers = (Hashtbl.create 9 : (string, float) Hashtbl.t) + +let add_to_timer name time = + let old = try Hashtbl.find timers name with Not_found -> 0.0 in + Hashtbl.replace timers name (old +. time) + +let time name fn arg = + let start = Unix.gettimeofday() in + try + let res = fn arg in + add_to_timer name (Unix.gettimeofday() -. start); + res + with x -> + add_to_timer name (Unix.gettimeofday() -. start); + raise x + +let print_timers () = + Hashtbl.iter + (fun name time -> Printf.printf "%-20s %.3f\n" name time) + timers + +let _ = at_exit print_timers +*) |