1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103 | ------------------------------------------------------------------------------
-- Copyright (C) 2020 by Heisenbug Ltd. (gh+spat@heisenbug.eu)
--
-- This work is free. You can redistribute it and/or modify it under the
-- terms of the Do What The Fuck You Want To Public License, Version 2,
-- as published by Sam Hocevar. See the LICENSE file for more details.
------------------------------------------------------------------------------
pragma License (Unrestricted);
------------------------------------------------------------------------------
--
-- SPARK Proof Analysis Tool
--
-- S.P.A.T. - Main program - separate Print_Summary
--
------------------------------------------------------------------------------
with Ada.Text_IO;
with SPAT.Strings;
separate (Run_SPAT)
------------------------------------------------------------------------------
-- Print_Summary
------------------------------------------------------------------------------
procedure Print_Summary (Info : in SPAT.Spark_Info.T;
Sort_By : in SPAT.Spark_Info.Sorting_Criterion;
Cut_Off : in Duration)
is
Files : constant SPAT.Strings.SPARK_File_Names :=
Info.List_All_Files (Sort_By => Sort_By);
Count_Omitted : Natural := 0;
Second_Column : Ada.Text_IO.Count := 0;
Third_Column : Ada.Text_IO.Count;
use type Ada.Text_IO.Count;
begin
for File of Files loop
-- Can't use Files.Max_Length here, because we use the Simple_Name, not
-- the actual string stored.
-- FIXME: This assumes that everything is displayed, the actual output
-- might be less and the tabulation is a bit wide.
Second_Column :=
Ada.Text_IO.Count'Max (Second_Column,
Ada.Directories.Simple_Name
(Name => SPAT.To_String (File))'Length);
end loop;
Second_Column := Second_Column + 2;
Third_Column := Second_Column + 4;
for File of Files loop
if Info.Proof_Time (File => File) < Cut_Off then
-- Below cut off point, do nothing but count the number of items
-- omitted.
Count_Omitted := Count_Omitted + 1;
else
SPAT.Log.Message
(Message =>
Ada.Directories.Simple_Name
(Name => SPAT.To_String (Source => File)),
New_Line => False);
Ada.Text_IO.Set_Col (File => Ada.Text_IO.Standard_Output,
To => Second_Column);
SPAT.Log.Message
(Message =>
"=> (Flow => " &
SPAT.Image (Value => Info.Flow_Time (File => File)) & ",",
New_Line => False);
Ada.Text_IO.Set_Col (File => Ada.Text_IO.Standard_Output,
To => Third_Column);
declare
Max_Success_Proof_Time : constant Duration :=
Info.Max_Success_Proof_Time (File => File);
begin
SPAT.Log.Message
(Message =>
"Proof => " &
(if Max_Success_Proof_Time = -1.0 -- nothing valid found
then "--"
else
SPAT.Image
(Value => Max_Success_Proof_Time,
Steps => Info.Max_Success_Proof_Steps (File => File))) &
"/" &
SPAT.Image (Value => Info.Max_Proof_Time (File => File),
Steps => Info.Max_Proof_Steps (File => File)) &
"/" &
SPAT.Image (Value => Info.Proof_Time (File => File)) & ")");
end;
end if;
end loop;
if Count_Omitted /= 0 and then SPAT.Log.Debug_Enabled then
SPAT.Log.Debug
(Message =>
"Omitted results below cut-off point (" &
SPAT.Image (Cut_Off) & "):" &
Count_Omitted'Image & ".");
end if;
end Print_Summary;
|