From ac93637516427dead9929acaf9a7ae61346da862 Mon Sep 17 00:00:00 2001 From: Claudio Sacerdoti Coen Date: Thu, 13 Apr 2006 11:06:29 +0000 Subject: [PATCH] Utime + Systime used in place of gettimeofday. --- .../components/binaries/utilities/test_library.ml | 13 +++++++++---- 1 file changed, 9 insertions(+), 4 deletions(-) diff --git a/helm/software/components/binaries/utilities/test_library.ml b/helm/software/components/binaries/utilities/test_library.ml index 635b6bbd4..98ade3adb 100644 --- a/helm/software/components/binaries/utilities/test_library.ml +++ b/helm/software/components/binaries/utilities/test_library.ml @@ -83,9 +83,14 @@ let _ = Printf.printf "%s " uri; flush stdout; let uri = UriManager.uri_of_string uri in - let before = Unix.gettimeofday () in + let obj,_ = CicEnvironment.get_obj CicUniv.empty_ugraph uri in ignore (Unix.alarm deadline); - ignore (CicTypeChecker.typecheck uri); + CicTypeChecker.typecheck_obj uri obj; + ignore (Unix.alarm 0); + CicEnvironment.remove_obj uri; + let before = Unix.times () in + ignore (Unix.alarm deadline); + ignore (CicTypeChecker.typecheck_obj uri obj); ignore (Unix.alarm 0); let memusage = (Gc.stat ()).Gc.live_words * 4 / 1024 / 1024 in if memusage > 500 then @@ -96,8 +101,8 @@ let _ = let memusage = (Gc.stat ()).Gc.live_words * 4 / 1024 / 1024 in prerr_endline ("DOPO CicEnvironment.empty: " ^ string_of_int memusage ^ "Mb"); end; - let after = Unix.gettimeofday () in - let diff = after -. before in + let after = Unix.times () in + let diff = after.Unix.tms_utime +. after.Unix.tms_stime -. before.Unix.tms_utime -. before.Unix.tms_stime in new_total := !new_total +. diff; Printf.printf "OK %.2f" diff; (match time with -- 2.39.2