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
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119 | ------------------------------------------------------------------------------
-- 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_Suggestion
--
------------------------------------------------------------------------------
with Ada.Strings.Fixed;
with SPAT.Log;
with SPAT.Spark_Info.Heuristics;
with SPAT.Strings;
separate (Run_SPAT)
------------------------------------------------------------------------------
-- Print_Suggestion
------------------------------------------------------------------------------
procedure Print_Suggestion
(Info : in SPAT.Spark_Info.T;
File_Map : in SPAT.GPR_Support.SPARK_Source_Maps.Map)
is
Indent : constant String := " ";
Results : SPAT.Spark_Info.Heuristics.File_Vectors.Vector;
use type SPAT.Spark_Info.Heuristics.Prover_Vectors.Cursor;
begin
SPAT.Log.Warning
(Message => "You requested a suggested prover configuration.");
SPAT.Log.Warning (Message => "This feature is highly experimental.");
SPAT.Log.Warning (Message => "Please consult the documentation.");
Results := SPAT.Spark_Info.Heuristics.Find_Optimum (Info => Info,
File_Map => File_Map);
SPAT.Log.Message (Message => "");
SPAT.Log.Message (Message => "package Prove is");
For_Each_File :
for File of Results loop
Find_Minima :
declare
Min_Steps : SPAT.Prover_Steps := 0;
Min_Timeout : Duration := 0.0;
begin
if not File.Provers.Is_Empty then
SPAT.Log.Message
(Message =>
Indent & "for Proof_Switches (""" &
SPAT.To_String (Source => File.Name) & """) use (""",
New_Line => False);
SPAT.Log.Message (Message => "--prover=",
New_Line => False);
For_Each_Prover :
for Prover in File.Provers.Iterate loop
Min_Steps :=
SPAT.Prover_Steps'Max
(File.Provers (Prover).Workload.Max_Success.Steps,
Min_Steps);
Min_Timeout :=
Duration'Max (File.Provers (Prover).Workload.Max_Success.Time,
Min_Timeout);
SPAT.Log.Message
(Message => SPAT.To_String (File.Provers (Prover).Name),
New_Line => False);
if Prover /= File.Provers.Last then
SPAT.Log.Message (Message => ",",
New_Line => False);
end if;
end loop For_Each_Prover;
SPAT.Log.Message (Message => """, ",
New_Line => False);
SPAT.Log.Message
(Message =>
"""--steps=" &
Ada.Strings.Fixed.Trim (Source => Min_Steps'Image,
Side => Ada.Strings.Both) &
"""",
New_Line => False);
SPAT.Log.Message (Message => ", ",
New_Line => False);
SPAT.Log.Message
(Message =>
"""--timeout=" &
Ada.Strings.Fixed.Trim
(Source => Integer'Image (Integer (Min_Timeout + 0.5)),
Side => Ada.Strings.Both) &
"""",
New_Line => False);
SPAT.Log.Message (Message => ");");
else
SPAT.Log.Message
(Message =>
Indent & "-- """ & SPAT.To_String (Source => File.Name) &
""" -- no data found.");
end if;
end Find_Minima;
end loop For_Each_File;
SPAT.Log.Message (Message => "end Prove;");
SPAT.Log.Message (Message => "");
end Print_Suggestion;
|