Commit 2a216a5b authored by MARCHE Claude's avatar MARCHE Claude

why3 info --graph: bug fix in computation of cumulative execution time

parent 980e0795
......@@ -395,7 +395,7 @@ let print_hist stats =
(fun p h acc ->
let pf,ch = Filename.open_temp_file "why3session" ".data" in
if acc = 1 then
fprintf main_fmt "plot [1:%d] [0.01:%.2f] "
fprintf main_fmt "plot [0:%d] [0.01:%.2f] "
(stats.nb_proved_sub_goals + stats.nb_proved_root_goals)
max_sum_times
else
......@@ -406,11 +406,12 @@ let print_hist stats =
let fmt = formatter_of_out_channel ch in
(** The time is also accumulated in order to obtain the total cpu time
taken to reach the given number of proved goal *)
fprintf fmt "0.01 0@\n";
let (_ : float * int) =
Mfloat.fold
(fun t c (acct,accc) ->
let accc = c + accc in
let acct = t +. acct in
let acct = (float c) *. t +. acct in
fprintf fmt "%.2f %d@\n" acct accc;
(acct,accc))
h (0.0,0)
......
Markdown is supported
0%
or
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment