From 5e8237152cad0cf08d3eea0d5de8cd8bc499df69 Mon Sep 17 00:00:00 2001
From: xleroy <xleroy@fca1b0fc-160b-0410-b1d3-a4f43f01ea2e>
Date: Mon, 11 Sep 2006 14:24:49 +0000
Subject: Code de timing

git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@93 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
---
 caml/Camlcoq.ml | 26 ++++++++++++++++++++++++++
 1 file changed, 26 insertions(+)

(limited to 'caml')

diff --git a/caml/Camlcoq.ml b/caml/Camlcoq.ml
index ab111c11..c2115dfb 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
+*)
-- 
cgit