diff options
Diffstat (limited to 'lib')
| -rw-r--r-- | lib/flags.ml | 6 | ||||
| -rw-r--r-- | lib/flags.mli | 2 | ||||
| -rw-r--r-- | lib/profile.ml | 29 |
3 files changed, 21 insertions, 16 deletions
diff --git a/lib/flags.ml b/lib/flags.ml index 5d9d9dcf50..0bce22f584 100644 --- a/lib/flags.ml +++ b/lib/flags.ml @@ -106,7 +106,7 @@ let we_are_parsing = ref false (* Current means no particular compatibility consideration. For correct comparisons, this constructor should remain the last one. *) -type compat_version = VOld | V8_5 | V8_6 | Current +type compat_version = VOld | V8_5 | V8_6 | V8_7 | Current let compat_version = ref Current @@ -120,6 +120,9 @@ let version_compare v1 v2 = match v1, v2 with | V8_6, V8_6 -> 0 | V8_6, _ -> -1 | _, V8_6 -> 1 + | V8_7, V8_7 -> 0 + | V8_7, _ -> -1 + | _, V8_7 -> 1 | Current, Current -> 0 let version_strictly_greater v = version_compare !compat_version v > 0 @@ -129,6 +132,7 @@ let pr_version = function | VOld -> "old" | V8_5 -> "8.5" | V8_6 -> "8.6" + | V8_7 -> "8.7" | Current -> "current" (* Translate *) diff --git a/lib/flags.mli b/lib/flags.mli index e63f1ec26d..eb4c37a548 100644 --- a/lib/flags.mli +++ b/lib/flags.mli @@ -77,7 +77,7 @@ val raw_print : bool ref (* Univ print flag, never set anywere. Maybe should belong to Univ? *) val univ_print : bool ref -type compat_version = VOld | V8_5 | V8_6 | Current +type compat_version = VOld | V8_5 | V8_6 | V8_7 | Current val compat_version : compat_version ref val version_compare : compat_version -> compat_version -> int val version_strictly_greater : compat_version -> bool diff --git a/lib/profile.ml b/lib/profile.ml index b669161858..0bc226a450 100644 --- a/lib/profile.ml +++ b/lib/profile.ml @@ -85,6 +85,9 @@ let init_alloc = ref 0.0 let reset_profile () = List.iter reset_record !prof_table let init_profile () = + (* We test Flags.profile as a way to support declaring profiled + functions in plugins *) + if !prof_table <> [] || Flags.profile then begin let outside = create_record () in stack := [outside]; last_alloc := get_alloc (); @@ -92,6 +95,7 @@ let init_profile () = init_time := get_time (); outside.tottime <- - !init_time; outside.owntime <- - !init_time + end let ajoute n o = o.owntime <- o.owntime + n.owntime; @@ -317,15 +321,15 @@ let adjust_time ov_bc ov_ad e = owntime = e.owntime - int_of_float (ad_imm +. bc_imm) } let close_profile print = - let dw = spent_alloc () in - let t = get_time () in - match !stack with - | [outside] -> - outside.tottime <- outside.tottime + t; - outside.owntime <- outside.owntime + t; - ajoute_ownalloc outside dw; - ajoute_totalloc outside dw; - if !prof_table <> [] then begin + if !prof_table <> [] then begin + let dw = spent_alloc () in + let t = get_time () in + match !stack with + | [outside] -> + outside.tottime <- outside.tottime + t; + outside.owntime <- outside.owntime + t; + ajoute_ownalloc outside dw; + ajoute_totalloc outside dw; let ov_bc = time_overhead_B_C () (* B+C overhead *) in let ov_ad = time_overhead_A_D () (* A+D overhead *) in let adjust (n,e) = (n, adjust_time ov_bc ov_ad e) in @@ -346,8 +350,8 @@ let close_profile print = in if print then format_profile updated_data; init_profile () - end - | _ -> failwith "Inconsistency" + | _ -> failwith "Inconsistency" + end let print_profile () = close_profile true @@ -358,9 +362,6 @@ let declare_profile name = prof_table := (name,e)::!prof_table; e -(* Default initialization, may be overridden *) -let _ = init_profile () - (******************************) (* Entry points for profiling *) let profile1 e f a = |