src/HOL/Mirabelle/lib/scripts/report.pl
changeset 32508 212530b16e6e
parent 32506 173fd51d06c9
child 32509 9da37876874d
equal deleted inserted replaced
32507:52b4f2f54e46 32508:212530b16e6e
    53 }
    53 }
    54 
    54 
    55 if ($sh_calls > 0) {
    55 if ($sh_calls > 0) {
    56   my $percent = $sh_succeeded / $sh_calls * 100;
    56   my $percent = $sh_succeeded / $sh_calls * 100;
    57   my $time = $sh_time / 1000;
    57   my $time = $sh_time / 1000;
    58   my $avg_time = $sh_time / $sh_succeeded;
    58   my $avg_time = $time / $sh_succeeded;
    59   print FILE "Total number of sledgehammer calls: $sh_calls\n";
    59   print FILE "Total number of sledgehammer calls: $sh_calls\n";
    60   print FILE "Number of successful sledgehammer calls: $sh_succeeded\n";
    60   print FILE "Number of successful sledgehammer calls: $sh_succeeded\n";
    61   printf FILE "Percentage of successful sledgehammer calls: %.0f%%\n", $percent;
    61   printf FILE "Percentage of successful sledgehammer calls: %.0f%%\n", $percent;
    62   print FILE "Total time for successful sledgehammer calls: $time seconds\n";
    62   print FILE "Total time for successful sledgehammer calls: $time seconds\n";
    63   print FILE "Average time for successful sledgehammer calls: $avg_time seconds\n\n";
    63   print FILE "Average time for successful sledgehammer calls: $avg_time seconds\n\n";