|
(************************************************************************)
(* * The Coq Proof Assistant / The Coq Development Team *)
(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *)
(* <O___,, * (see CREDITS file for the list of authors) *)
(* \VV/ **************************************************************)
(* // * This file is distributed under the terms of the *)
(* * GNU Lesser General Public License Version 2.1 *)
(* * (see LICENSE file for the text of the license) *)
(************************************************************************)
let word_length = Sys.word_size / 8
let float_of_time t = float_of_int t /. 100.
let time_of_float f = int_of_float (f *. 100.)
let get_time () =
time_of_float (Sys.time ())
(* Since ocaml 3.01, gc statistics are in float *)
let get_alloc () =
(* If you are unlucky, a minor collection can occur between the *)
(* measurements and produces allocation; we trigger a minor *)
(* collection in advance to be sure the measure is not corrupted *)
Gc.minor ();
Gc.allocated_bytes ()
(* Rem: overhead was 16 bytes in ocaml 3.00 (long int) *)
(* Rem: overhead is 100 bytes in ocaml 3.01 (double) *)
let get_alloc_overhead =
let mark1 = get_alloc () in
let mark2 = get_alloc () in
let mark3 = get_alloc () in
(* If you are unlucky, a major collection can occur between the *)
(* measurements; with two measures the risk decreases *)
min (mark2 -. mark1) (mark3 -. mark2)
let last_alloc = ref 0.0 (* set by init_profile () *)
let spent_alloc () =
let now = get_alloc () in
let before = !last_alloc in
last_alloc := now;
now -. before -. get_alloc_overhead
(* Profile records *)
type profile_key = {
mutable owntime : int;
mutable tottime : int;
mutable ownalloc : float;
mutable totalloc : float;
mutable owncount : int;
mutable intcount : int;
mutable immcount : int;
}
let create_record () = {
owntime=0;
tottime=0;
ownalloc=0.0;
totalloc=0.0;
owncount=0;
intcount=0;
immcount=0
}
let ajoute_totalloc e dw = e.totalloc <- e.totalloc +. dw
let ajoute_ownalloc e dw = e.ownalloc <- e.ownalloc +. dw
let reset_record (n,e) =
e.owntime <- 0;
e.tottime <- 0;
e.ownalloc <- 0.0;
e.totalloc <- 0.0;
e.owncount <- 0;
e.intcount <- 0;
e.immcount <- 0
(* Profile tables *)
let prof_table = ref []
let stack = ref []
let init_time = ref 0
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 ();
init_alloc := !last_alloc;
init_time := get_time ();
outside.tottime <- - !init_time;
outside.owntime <- - !init_time
end
let ajoute n o =
o.owntime <- o.owntime + n.owntime;
o.tottime <- o.tottime + n.tottime;
ajoute_ownalloc o n.ownalloc;
ajoute_totalloc o n.totalloc;
o.owncount <- o.owncount + n.owncount;
o.intcount <- o.intcount + n.intcount;
o.immcount <- o.immcount + n.immcount
let ajoute_to_list ((name,n) as e) l =
try ajoute n (List.assoc name l); l
with Not_found -> e::l
let magic = 1249
let merge_profile filename (curr_table, curr_outside, curr_total as new_data) =
let (old_table, old_outside, old_total) =
try
let c = open_in filename in
if input_binary_int c <> magic
then Printf.printf "Incompatible recording file: %s\n" filename;
let old_data = input_value c in
close_in c;
old_data
with Sys_error msg ->
(Printf.printf "Unable to open %s: %s\n" filename msg;
new_data) in
let updated_data =
let updated_table = List.fold_right ajoute_to_list curr_table old_table in
ajoute curr_outside old_outside;
ajoute curr_total old_total;
(updated_table, old_outside, old_total) in
begin
(try
let c =
open_out_gen
[Open_creat;Open_wronly;Open_trunc;Open_binary] 0o644 filename in
output_binary_int c magic;
output_value c updated_data;
close_out c
with Sys_error _ -> Printf.printf "Unable to create recording file");
updated_data
end
(************************************************)
(* Compute a rough estimation of time overheads *)
(* Time and space are not measured in the same way *)
(* Byte allocation is an exact number and for long runs, the total
number of allocated bytes may exceed the maximum integer capacity
(2^31 on 32-bits architectures); therefore, allocation is measured
by small steps, total allocations are computed by adding elementary
measures and carries are controlled from step to step *)
(* Unix measure of time is approximate and short delays are often
unperceivable; therefore, total times are measured in one (big)
step to avoid rounding errors and to get the best possible
approximation.
Note: Sys.time is the same as:
Unix.(let x = times () in x.tms_utime +. x.tms_stime)
*)
(*
---------- start profile for f1
overheadA| ...
---------- [1w1] 1st call to get_time for f1
overheadB| ...
---------- start f1
real 1 | ...
---------- start profile for 1st call to f2 inside f1
overheadA| ...
---------- [2w1] 1st call to get_time for 1st f2
overheadB| ...
---------- start 1st f2
real 2 | ...
---------- end 1st f2
overheadC| ...
---------- [2w1] 2nd call to get_time for 1st f2
overheadD| ...
---------- end profile for 1st f2
real 1 | ...
---------- start profile for 2nd call to f2 inside f1
overheadA| ...
---------- [2'w1] 1st call to get_time for 2nd f2
overheadB| ...
---------- start 2nd f2
real 2' | ...
---------- end 2nd f2
overheadC| ...
---------- [2'w2] 2nd call to get_time for 2nd f2
overheadD| ...
---------- end profile for f2
real 1 | ...
---------- end f1
overheadC| ...
---------- [1w1'] 2nd call to get_time for f1
overheadD| ...
---------- end profile for f1
When profiling f2, overheadB + overheadC should be subtracted from measure
and overheadA + overheadB + overheadC + overheadD should be subtracted from
the amount for f1
Then the relevant overheads are :
"overheadB + overheadC" to be subtracted to the measure of f as many time as f is called and
"overheadA + overheadB + overheadC + overheadD" to be subtracted to
the measure of f as many time as f calls a profiled function (itself
included)
*)
let dummy_last_alloc = ref 0.0
let dummy_spent_alloc () =
let now = get_alloc () in
let before = !last_alloc in
last_alloc := now;
now -. before
let dummy_f x = x
let dummy_stack = ref [create_record ()]
let dummy_ov = 0
let loops = 10000
let time_overhead_A_D () =
let e = create_record () in
let before = get_time () in
for _i = 1 to loops do
(* This is a copy of profile1 for overhead estimation *)
let dw = dummy_spent_alloc () in
match !dummy_stack with [] -> assert false | p::_ ->
ajoute_ownalloc p dw;
ajoute_totalloc p dw;
e.owncount <- e.owncount + 1;
if not (p==e) then stack := e::!stack;
let totalloc0 = e.totalloc in
let intcount0 = e.intcount in
let dt = get_time () - 1 in
e.tottime <- dt + dummy_ov; e.owntime <- e.owntime + e.tottime;
ajoute_ownalloc p dw;
ajoute_totalloc p dw;
p.owntime <- p.owntime - e.tottime;
ajoute_totalloc p (e.totalloc-.totalloc0);
p.intcount <- p.intcount + e.intcount - intcount0 + 1;
p.immcount <- p.immcount + 1;
if not (p==e) then
(match !dummy_stack with [] -> assert false | _::s -> stack := s);
dummy_last_alloc := get_alloc ()
done;
let after = get_time () in
let beforeloop = get_time () in
for _i = 1 to loops do () done;
let afterloop = get_time () in
float_of_int ((after - before) - (afterloop - beforeloop))
/. float_of_int loops
let time_overhead_B_C () =
let dummy_x = 0 in
let before = get_time () in
for _i = 1 to loops do
try
dummy_last_alloc := get_alloc ();
let _r = dummy_f dummy_x in
let _dw = dummy_spent_alloc () in
let _dt = get_time () in
()
with e when CErrors.noncritical e -> assert false
done;
let after = get_time () in
let beforeloop = get_time () in
for _i = 1 to loops do () done;
let afterloop = get_time () in
float_of_int ((after - before) - (afterloop - beforeloop))
/. float_of_int loops
let compute_alloc lo = lo /. (float_of_int word_length)
(************************************************)
(* End a profiling session and print the result *)
let format_profile (table, outside, total) =
print_newline ();
Printf.printf
"%-23s %9s %9s %10s %10s %10s\n"
"Function name" "Own time" "Tot. time" "Own alloc" "Tot. alloc" "Calls ";
let l = List.sort (fun (_,{tottime=p}) (_,{tottime=p'}) -> p' - p) table in
List.iter (fun (name,e) ->
Printf.printf
"%-23s %9.2f %9.2f %10.0f %10.0f %6d %6d\n"
name
(float_of_time e.owntime) (float_of_time e.tottime)
(compute_alloc e.ownalloc)
(compute_alloc e.totalloc)
e.owncount e.intcount)
l;
Printf.printf "%-23s %9.2f %9.2f %10.0f %10.0f %6d\n"
"others"
(float_of_time outside.owntime) (float_of_time outside.tottime)
(compute_alloc outside.ownalloc)
(compute_alloc outside.totalloc)
outside.intcount;
(* Here, own contains overhead time/alloc *)
Printf.printf "%-23s %9.2f %9.2f %10.0f %10.0f\n"
"Est. overhead/total"
(float_of_time total.owntime) (float_of_time total.tottime)
(compute_alloc total.ownalloc)
(compute_alloc total.totalloc);
Printf.printf
"Time in seconds and allocation in words (1 word = %d bytes)\n"
word_length
let recording_file = ref ""
let set_recording s = recording_file := s
let adjust_time ov_bc ov_ad e =
let bc_imm = float_of_int e.owncount *. ov_bc in
let ad_imm = float_of_int e.immcount *. ov_ad in
let abcd_all = float_of_int e.intcount *. (ov_ad +. ov_bc) in
{e with
tottime = e.tottime - int_of_float (abcd_all +. bc_imm);
owntime = e.owntime - int_of_float (ad_imm +. bc_imm) }
let close_profile print =
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
let adjtable = List.map adjust !prof_table in
let adjoutside = adjust_time ov_bc ov_ad outside in
let totalloc = !last_alloc -. !init_alloc in
let total = create_record () in
total.tottime <- outside.tottime;
total.totalloc <- totalloc;
(* We compute estimations of overhead, put into "own" fields *)
total.owntime <- outside.tottime - adjoutside.tottime;
total.ownalloc <- totalloc -. outside.totalloc;
let current_data = (adjtable, adjoutside, total) in
let updated_data =
match !recording_file with
| "" -> current_data
| name -> merge_profile !recording_file current_data
in
if print then format_profile updated_data;
init_profile ()
| _ -> failwith "Inconsistency"
end
let print_profile () = close_profile true
let declare_profile name =
if name = "___outside___" || name = "___total___" then
failwith ("Error: "^name^" is a reserved keyword");
let e = create_record () in
prof_table := (name,e)::!prof_table;
e
(******************************)
(* Entry points for profiling *)
let profile1 e f a =
let dw = spent_alloc () in
match !stack with [] -> assert false | p::_ ->
(* We add spent alloc since last measure to current caller own/total alloc *)
ajoute_ownalloc p dw;
ajoute_totalloc p dw;
e.owncount <- e.owncount + 1;
if not (p==e) then stack := e::!stack;
let totalloc0 = e.totalloc in
let intcount0 = e.intcount in
let t = get_time () in
try
last_alloc := get_alloc ();
let r = f a in
let dw = spent_alloc () in
let dt = get_time () - t in
e.tottime <- e.tottime + dt; e.owntime <- e.owntime + dt;
ajoute_ownalloc e dw;
ajoute_totalloc e dw;
p.owntime <- p.owntime - dt;
ajoute_totalloc p (e.totalloc -. totalloc0);
p.intcount <- p.intcount + e.intcount - intcount0 + 1;
p.immcount <- p.immcount + 1;
if not (p==e) then
(match !stack with [] -> assert false | _::s -> stack := s);
last_alloc := get_alloc ();
r
with reraise ->
let dw = spent_alloc () in
let dt = get_time () - t in
e.tottime <- e.tottime + dt; e.owntime <- e.owntime + dt;
ajoute_ownalloc e dw;
ajoute_totalloc e dw;
p.owntime <- p.owntime - dt;
ajoute_totalloc p (e.totalloc -. totalloc0);
p.intcount <- p.intcount + e.intcount - intcount0 + 1;
p.immcount <- p.immcount + 1;
if not (p==e) then
(match !stack with [] -> assert false | _::s -> stack := s);
last_alloc := get_alloc ();
raise reraise
let profile2 e f a b =
let dw = spent_alloc () in
match !stack with [] -> assert false | p::_ ->
(* We add spent alloc since last measure to current caller own/total alloc *)
ajoute_ownalloc p dw;
ajoute_totalloc p dw;
e.owncount <- e.owncount + 1;
if not (p==e) then stack := e::!stack;
let totalloc0 = e.totalloc in
let intcount0 = e.intcount in
let t = get_time () in
try
last_alloc := get_alloc ();
let r = f a b in
let dw = spent_alloc () in
let dt = get_time () - t in
e.tottime <- e.tottime + dt; e.owntime <- e.owntime + dt;
ajoute_ownalloc e dw;
ajoute_totalloc e dw;
p.owntime <- p.owntime - dt;
ajoute_totalloc p (e.totalloc -. totalloc0);
p.intcount <- p.intcount + e.intcount - intcount0 + 1;
p.immcount <- p.immcount + 1;
if not (p==e) then
(match !stack with [] -> assert false | _::s -> stack := s);
last_alloc := get_alloc ();
r
with reraise ->
let dw = spent_alloc () in
let dt = get_time () - t in
e.tottime <- e.tottime + dt; e.owntime <- e.owntime + dt;
ajoute_ownalloc e dw;
ajoute_totalloc e dw;
p.owntime <- p.owntime - dt;
ajoute_totalloc p (e.totalloc -. totalloc0);
p.intcount <- p.intcount + e.intcount - intcount0 + 1;
p.immcount <- p.immcount + 1;
if not (p==e) then
(match !stack with [] -> assert false | _::s -> stack := s);
last_alloc := get_alloc ();
raise reraise
let profile3 e f a b c =
let dw = spent_alloc () in
match !stack with [] -> assert false | p::_ ->
(* We add spent alloc since last measure to current caller own/total alloc *)
ajoute_ownalloc p dw;
ajoute_totalloc p dw;
e.owncount <- e.owncount + 1;
if not (p==e) then stack := e::!stack;
let totalloc0 = e.totalloc in
let intcount0 = e.intcount in
let t = get_time () in
try
last_alloc := get_alloc ();
let r = f a b c in
let dw = spent_alloc () in
let dt = get_time () - t in
e.tottime <- e.tottime + dt; e.owntime <- e.owntime + dt;
ajoute_ownalloc e dw;
ajoute_totalloc e dw;
p.owntime <- p.owntime - dt;
ajoute_totalloc p (e.totalloc -. totalloc0);
p.intcount <- p.intcount + e.intcount - intcount0 + 1;
p.immcount <- p.immcount + 1;
if not (p==e) then
(match !stack with [] -> assert false | _::s -> stack := s);
last_alloc := get_alloc ();
r
with reraise ->
let dw = spent_alloc () in
let dt = get_time () - t in
e.tottime <- e.tottime + dt; e.owntime <- e.owntime + dt;
ajoute_ownalloc e dw;
ajoute_totalloc e dw;
p.owntime <- p.owntime - dt;
ajoute_totalloc p (e.totalloc -. totalloc0);
p.intcount <- p.intcount + e.intcount - intcount0 + 1;
p.immcount <- p.immcount + 1;
if not (p==e) then
(match !stack with [] -> assert false | _::s -> stack := s);
last_alloc := get_alloc ();
raise reraise
let profile4 e f a b c d =
let dw = spent_alloc () in
match !stack with [] -> assert false | p::_ ->
(* We add spent alloc since last measure to current caller own/total alloc *)
ajoute_ownalloc p dw;
ajoute_totalloc p dw;
e.owncount <- e.owncount + 1;
if not (p==e) then stack := e::!stack;
let totalloc0 = e.totalloc in
let intcount0 = e.intcount in
let t = get_time () in
try
last_alloc := get_alloc ();
let r = f a b c d in
let dw = spent_alloc () in
let dt = get_time () - t in
e.tottime <- e.tottime + dt; e.owntime <- e.owntime + dt;
ajoute_ownalloc e dw;
ajoute_totalloc e dw;
p.owntime <- p.owntime - dt;
ajoute_totalloc p (e.totalloc -. totalloc0);
p.intcount <- p.intcount + e.intcount - intcount0 + 1;
p.immcount <- p.immcount + 1;
if not (p==e) then
(match !stack with [] -> assert false | _::s -> stack := s);
last_alloc := get_alloc ();
r
with reraise ->
let dw = spent_alloc () in
let dt = get_time () - t in
e.tottime <- e.tottime + dt; e.owntime <- e.owntime + dt;
ajoute_ownalloc e dw;
ajoute_totalloc e dw;
p.owntime <- p.owntime - dt;
ajoute_totalloc p (e.totalloc -. totalloc0);
p.intcount <- p.intcount + e.intcount - intcount0 + 1;
p.immcount <- p.immcount + 1;
if not (p==e) then
(match !stack with [] -> assert false | _::s -> stack := s);
last_alloc := get_alloc ();
raise reraise
let profile5 e f a b c d g =
let dw = spent_alloc () in
match !stack with [] -> assert false | p::_ ->
(* We add spent alloc since last measure to current caller own/total alloc *)
ajoute_ownalloc p dw;
ajoute_totalloc p dw;
e.owncount <- e.owncount + 1;
if not (p==e) then stack := e::!stack;
let totalloc0 = e.totalloc in
let intcount0 = e.intcount in
let t = get_time () in
try
last_alloc := get_alloc ();
let r = f a b c d g in
let dw = spent_alloc () in
let dt = get_time () - t in
e.tottime <- e.tottime + dt; e.owntime <- e.owntime + dt;
ajoute_ownalloc e dw;
ajoute_totalloc e dw;
p.owntime <- p.owntime - dt;
ajoute_totalloc p (e.totalloc -. totalloc0);
p.intcount <- p.intcount + e.intcount - intcount0 + 1;
p.immcount <- p.immcount + 1;
if not (p==e) then
(match !stack with [] -> assert false | _::s -> stack := s);
last_alloc := get_alloc ();
r
with reraise ->
let dw = spent_alloc () in
let dt = get_time () - t in
e.tottime <- e.tottime + dt; e.owntime <- e.owntime + dt;
ajoute_ownalloc e dw;
ajoute_totalloc e dw;
p.owntime <- p.owntime - dt;
ajoute_totalloc p (e.totalloc -. totalloc0);
p.intcount <- p.intcount + e.intcount - intcount0 + 1;
p.immcount <- p.immcount + 1;
if not (p==e) then
(match !stack with [] -> assert false | _::s -> stack := s);
last_alloc := get_alloc ();
raise reraise
let profile6 e f a b c d g h =
let dw = spent_alloc () in
match !stack with [] -> assert false | p::_ ->
(* We add spent alloc since last measure to current caller own/total alloc *)
ajoute_ownalloc p dw;
ajoute_totalloc p dw;
e.owncount <- e.owncount + 1;
if not (p==e) then stack := e::!stack;
let totalloc0 = e.totalloc in
let intcount0 = e.intcount in
let t = get_time () in
try
last_alloc := get_alloc ();
let r = f a b c d g h in
let dw = spent_alloc () in
let dt = get_time () - t in
e.tottime <- e.tottime + dt; e.owntime <- e.owntime + dt;
ajoute_ownalloc e dw;
ajoute_totalloc e dw;
p.owntime <- p.owntime - dt;
ajoute_totalloc p (e.totalloc -. totalloc0);
p.intcount <- p.intcount + e.intcount - intcount0 + 1;
p.immcount <- p.immcount + 1;
if not (p==e) then
(match !stack with [] -> assert false | _::s -> stack := s);
last_alloc := get_alloc ();
r
with reraise ->
let dw = spent_alloc () in
let dt = get_time () - t in
e.tottime <- e.tottime + dt; e.owntime <- e.owntime + dt;
ajoute_ownalloc e dw;
ajoute_totalloc e dw;
p.owntime <- p.owntime - dt;
ajoute_totalloc p (e.totalloc -. totalloc0);
p.intcount <- p.intcount + e.intcount - intcount0 + 1;
p.immcount <- p.immcount + 1;
if not (p==e) then
(match !stack with [] -> assert false | _::s -> stack := s);
last_alloc := get_alloc ();
raise reraise
let profile7 e f a b c d g h i =
let dw = spent_alloc () in
match !stack with [] -> assert false | p::_ ->
(* We add spent alloc since last measure to current caller own/total alloc *)
ajoute_ownalloc p dw;
ajoute_totalloc p dw;
e.owncount <- e.owncount + 1;
if not (p==e) then stack := e::!stack;
let totalloc0 = e.totalloc in
let intcount0 = e.intcount in
let t = get_time () in
try
last_alloc := get_alloc ();
let r = f a b c d g h i in
let dw = spent_alloc () in
let dt = get_time () - t in
e.tottime <- e.tottime + dt; e.owntime <- e.owntime + dt;
ajoute_ownalloc e dw;
ajoute_totalloc e dw;
p.owntime <- p.owntime - dt;
ajoute_totalloc p (e.totalloc -. totalloc0);
p.intcount <- p.intcount + e.intcount - intcount0 + 1;
p.immcount <- p.immcount + 1;
if not (p==e) then
(match !stack with [] -> assert false | _::s -> stack := s);
last_alloc := get_alloc ();
r
with reraise ->
let dw = spent_alloc () in
let dt = get_time () - t in
e.tottime <- e.tottime + dt; e.owntime <- e.owntime + dt;
ajoute_ownalloc e dw;
ajoute_totalloc e dw;
p.owntime <- p.owntime - dt;
ajoute_totalloc p (e.totalloc -. totalloc0);
p.intcount <- p.intcount + e.intcount - intcount0 + 1;
p.immcount <- p.immcount + 1;
if not (p==e) then
(match !stack with [] -> assert false | _::s -> stack := s);
last_alloc := get_alloc ();
raise reraise
let profile8 e f a b c d g h i j =
let dw = spent_alloc () in
match !stack with [] -> assert false | p::_ ->
(* We add spent alloc since last measure to current caller own/total alloc *)
ajoute_ownalloc p dw;
ajoute_totalloc p dw;
e.owncount <- e.owncount + 1;
if not (p==e) then stack := e::!stack;
let totalloc0 = e.totalloc in
let intcount0 = e.intcount in
let t = get_time () in
try
last_alloc := get_alloc ();
let r = f a b c d g h i j in
let dw = spent_alloc () in
let dt = get_time () - t in
e.tottime <- e.tottime + dt; e.owntime <- e.owntime + dt;
ajoute_ownalloc e dw;
ajoute_totalloc e dw;
p.owntime <- p.owntime - dt;
ajoute_totalloc p (e.totalloc -. totalloc0);
p.intcount <- p.intcount + e.intcount - intcount0 + 1;
p.immcount <- p.immcount + 1;
if not (p==e) then
(match !stack with [] -> assert false | _::s -> stack := s);
last_alloc := get_alloc ();
r
with reraise ->
let dw = spent_alloc () in
let dt = get_time () - t in
e.tottime <- e.tottime + dt; e.owntime <- e.owntime + dt;
ajoute_ownalloc e dw;
ajoute_totalloc e dw;
p.owntime <- p.owntime - dt;
ajoute_totalloc p (e.totalloc -. totalloc0);
p.intcount <- p.intcount + e.intcount - intcount0 + 1;
p.immcount <- p.immcount + 1;
if not (p==e) then
(match !stack with [] -> assert false | _::s -> stack := s);
last_alloc := get_alloc ();
raise reraise
let print_logical_stats a =
let (c, s, d) = CObj.obj_stats a in
Printf.printf "Expanded size: %10d (str: %8d) Depth: %6d\n" (s+c) c d
let print_stats a =
let (c1, s, d) = CObj.obj_stats a in
let c2 = CObj.size a in
Printf.printf "Size: %8d (exp: %10d) Depth: %6d\n"
c2 (s + c1) d
(*
let _ = Gc.set { (Gc.get()) with Gc.verbose = 13 }
*)
¤ Dauer der Verarbeitung: 0.24 Sekunden
(vorverarbeitet)
¤
|
Haftungshinweis
Die Informationen auf dieser Webseite wurden
nach bestem Wissen sorgfältig zusammengestellt. Es wird jedoch weder Vollständigkeit, noch Richtigkeit,
noch Qualität der bereit gestellten Informationen zugesichert.
Bemerkung:
Die farbliche Syntaxdarstellung ist noch experimentell.
|
