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
120
121
122
123
124
125
126
127
128
129
130
131
132
133
134
135
136
137
138
139
140
141
142
143
144
145
146
147
148
149
150
151
152
153
154
155
156
157
158
159
160
161
162
163
164
165
166
167
168
169
170
171
172
173
174
175
176
177
178
179
180
181
182
183
184
185
186
187
188
189
190
191
192
193
194
195
196
197
198
199
200
201
202
203
204
205
206
207
208
209
210
211
212
213
214
215
216
217
218
219
220
221
222
|
-------------------------------------------------------------------------------
-- (C) Altran Praxis Limited
-------------------------------------------------------------------------------
--
-- The SPARK toolset is free software; you can redistribute it and/or modify it
-- under terms of the GNU General Public License as published by the Free
-- Software Foundation; either version 3, or (at your option) any later
-- version. The SPARK toolset is distributed in the hope that it will be
-- useful, but WITHOUT ANY WARRANTY; without even the implied warranty of
-- MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the GNU General
-- Public License for more details. You should have received a copy of the GNU
-- General Public License distributed with the SPARK toolset; see file
-- COPYING3. If not, go to http://www.gnu.org/licenses for a complete copy of
-- the license.
--
--=============================================================================
with Ada.Command_Line;
with GNAT.Command_Line;
package body Command_Line is
procedure Int_From_Commandline
(E_Str : in E_Strings.T;
Limit_Low : in Integer;
Limit_High : in Integer;
Output : out Integer;
Ok : out Boolean;
Error : out E_Strings.T)
--# pre Limit_Low <= Limit_High;
--# post Output >= Limit_Low and Output <= Limit_High;
is
Tmp_Str : E_Strings.T;
Tmp_Nat : Natural;
begin
-- Chop off the '=' at the start, if present
if E_Strings.Get_Length (E_Str) >= 2 and then E_Strings.Get_Element (E_Str, 1) = '=' then
Tmp_Str := E_Strings.Section (E_Str => E_Str,
Start_Pos => 2,
Length => E_Strings.Get_Length (E_Str) - 1);
else
Tmp_Str := E_Str;
end if;
E_Strings.Get_Int_From_String (Source => Tmp_Str,
Item => Output,
Start_Pt => 1,
Stop => Tmp_Nat);
if Tmp_Nat = E_Strings.Get_Length (Tmp_Str) and Output >= Limit_Low and Output <= Limit_High then
Ok := True;
Error := E_Strings.Empty_String;
else
Output := Limit_Low;
Ok := False;
Error := E_Strings.Copy_String ("Parameter must be a valid number. Got '");
E_Strings.Append_Examiner_String (Error, Tmp_Str);
E_Strings.Append_String (Error, "' instead.");
end if;
end Int_From_Commandline;
procedure Solver_From_Commandline
(E_Str : in E_Strings.T;
Output : out Solver_T;
Ok : out Boolean;
Error : out E_Strings.T)
is
Tmp_Str : E_Strings.T;
begin
-- Chop off the '=' at the start, if present
if E_Strings.Get_Length (E_Str) >= 2 and then E_Strings.Get_Element (E_Str, 1) = '=' then
Tmp_Str := E_Strings.Section (E_Str => E_Str,
Start_Pos => 2,
Length => E_Strings.Get_Length (E_Str) - 1);
else
Tmp_Str := E_Str;
end if;
Ok := True;
Error := E_Strings.Empty_String;
if E_Strings.Eq1_String (Tmp_Str, "alt-ergo") then
Output := Alt_Ergo;
elsif E_Strings.Eq1_String (Tmp_Str, "cvc3") then
Output := CVC3;
elsif E_Strings.Eq1_String (Tmp_Str, "cvc4_smtlib1") then
Output := CVC4_SMTLIB1;
elsif E_Strings.Eq1_String (Tmp_Str, "cvc4") then
Output := CVC4;
elsif E_Strings.Eq1_String (Tmp_Str, "yices") then
Output := Yices;
elsif E_Strings.Eq1_String (Tmp_Str, "z3") then
Output := Z3;
else
Output := Alt_Ergo;
Ok := False;
Error := E_Strings.Copy_String ("Invalid/unsupported solver.");
end if;
end Solver_From_Commandline;
procedure Initialize (Data : out Command_Line_Data_T;
Ok : out Boolean;
Error : out E_Strings.T) is
--# hide Initialize;
Tmp_Int : Integer;
begin
Data := Default_Options;
Ok := True;
Error := E_Strings.Empty_String;
begin
loop
case GNAT.Command_Line.Getopt ("h help m: plain solver: steps: t: v nouserrules keep") is
when ASCII.NUL =>
exit;
when 'h' =>
-- Both the -h and -help options.
Data.Show_Help := True;
when 'k' =>
Data.Keep_Temp := True;
when 'm' =>
Int_From_Commandline
(E_Str => E_Strings.Copy_String (GNAT.Command_Line.Parameter),
Limit_Low => Memory_Limit_T'First,
Limit_High => Memory_Limit_T'Last,
Output => Tmp_Int,
Ok => Ok,
Error => Error);
if Ok then
Data.Memory_Limit := Memory_Limit_T'(Tmp_Int);
end if;
when 'n' =>
Data.User_Rules := False;
when 'p' =>
Data.Plain := True;
when 's' =>
if GNAT.Command_Line.Full_Switch = "steps" then
Int_From_Commandline
(E_Str => E_Strings.Copy_String (GNAT.Command_Line.Parameter),
Limit_Low => Natural'First,
Limit_High => Natural'Last,
Output => Tmp_Int,
Ok => Ok,
Error => Error);
if Ok then
Data.Proof_Steps := Natural'(Tmp_Int);
end if;
elsif GNAT.Command_Line.Full_Switch = "solver" then
Solver_From_Commandline
(E_Str => E_Strings.Copy_String (GNAT.Command_Line.Parameter),
Output => Data.Solver,
Ok => Ok,
Error => Error);
else
null;
end if;
when 't' =>
Int_From_Commandline
(E_Str => E_Strings.Copy_String (GNAT.Command_Line.Parameter),
Limit_Low => Natural'First,
Limit_High => Natural'Last,
Output => Tmp_Int,
Ok => Ok,
Error => Error);
if Ok then
Data.Time_Out := Natural'(Tmp_Int);
end if;
when 'v' =>
Data.Ignore_SIV := True;
when others =>
Ok := False;
Error := E_Strings.Copy_String ("Could not parse commandline.");
exit;
end case;
end loop;
loop
declare
S : constant String := GNAT.Command_Line.Get_Argument (Do_Expansion => True);
begin
exit when S'Length = 0;
if E_Strings.Is_Empty (Data.Unit_Name) then
Data.Unit_Name := E_Strings.Copy_String (S);
else
Ok := False;
Error := E_Strings.Copy_String ("You can only specify a single unit.");
end if;
end;
end loop;
exception
when GNAT.Command_Line.Invalid_Switch =>
Ok := False;
Error := E_Strings.Copy_String ("Invalid commandline switch " & GNAT.Command_Line.Full_Switch);
when GNAT.Command_Line.Invalid_Parameter =>
Ok := False;
Error := E_Strings.Copy_String ("No parameter for " & GNAT.Command_Line.Full_Switch);
end;
-- Finally, check that a unit is given. If not, we just show
-- the help text.
if E_Strings.Is_Empty (Data.Unit_Name) then
Data.Show_Help := True;
end if;
end Initialize;
procedure Set_Exit_Status_Error is
--# hide Set_Exit_Status_Error;
begin
Ada.Command_Line.Set_Exit_Status (1);
end Set_Exit_Status_Error;
end Command_Line;
|
