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
|
-------------------------------------------------------------------------------
-- (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 SPARK.Ada.Command_Line;
with SPARK.Ada.Command_Line.Unbounded_String;
with SPARK.Ada.Strings.Unbounded;
with SPARK.Ada.Text_IO.Unbounded_String;
package body Command_Line is
-- This procedure can be used to parse a command-line argument,
-- S. Arguments starts with a dash '-' and can contain an optional
-- value. For example:
--
-- "-foo" -> Has_Value = False
-- Option = "foo"
-- Value = ""
--
-- "-foo=bar" -> Has_Value = True
-- Option = "foo"
-- Value = "bar"
--
-- Valid is set to false if the S does not start with a dash '-'
-- or the value given is blank.
procedure Parse_Option
(S : in SPARK.Ada.Strings.Unbounded.Unbounded_String;
Valid : out Boolean;
Has_Value : out Boolean;
Option : out SPARK.Ada.Strings.Unbounded.Unbounded_String;
Value : out SPARK.Ada.Strings.Unbounded.Unbounded_String)
--# derives Has_Value,
--# Option,
--# Valid,
--# Value from S;
is
In_Name : Boolean := True;
In_Sep : Boolean := True;
C : Character;
begin
Valid := SPARK.Ada.Strings.Unbounded.Get_Length (S) >= 2;
Has_Value := False;
Option := SPARK.Ada.Strings.Unbounded.Get_Null_Unbounded_String;
Value := SPARK.Ada.Strings.Unbounded.Get_Null_Unbounded_String;
-- Parse option.
for N in Natural range 1 .. SPARK.Ada.Strings.Unbounded.Get_Length (S) loop
--# assert N <= SPARK.Ada.Strings.Unbounded.Get_Length (S)
--# and SPARK.Ada.Strings.Unbounded.Get_Length (S) <= Natural'Last
--# and SPARK.Ada.Strings.Unbounded.Get_Length (Option) < N
--# and SPARK.Ada.Strings.Unbounded.Get_Length (Value) < N;
C := SPARK.Ada.Strings.Unbounded.Get_Element (Source => S,
Index => N);
if N = 1 then
-- Options must start with a dash.
Valid := (C = '-');
elsif N > 1 and In_Name then
if C = '=' then
In_Name := False;
Has_Value := True;
else
SPARK.Ada.Strings.Unbounded.Append_Char (Option, C);
end if;
elsif N > 1 and In_Sep then
In_Sep := False;
elsif N > 1 then
SPARK.Ada.Strings.Unbounded.Append_Char (Value, C);
end if;
end loop;
-- If we have an option with a value, it can't be empty.
if Has_Value and SPARK.Ada.Strings.Unbounded.Get_Length (Value) = 0 then
Valid := False;
end if;
end Parse_Option;
procedure Initialize (Data : out Data_T;
Status : out Status_T) is
Opt_Name : SPARK.Ada.Strings.Unbounded.Unbounded_String;
Opt_Value : SPARK.Ada.Strings.Unbounded.Unbounded_String;
Opt_Has_Value : Boolean;
Opt_Is_Valid : Boolean;
Number_Of_Arguments : Natural;
begin
Number_Of_Arguments := SPARK.Ada.Command_Line.Argument_Count;
if SPARK.Ada.Command_Line.Argument_Count = 0 then
-- Delete all the files by default.
Data := Data_T'(Files_To_Delete => File_Type_Map'(others => True));
Status := Ok;
else
-- Delete only the files requested.
Data := Data_T'(Files_To_Delete => File_Type_Map'(others => False));
Status := Ok;
-- Check arguments. Each argument flags up one set of files
-- to delete.
for N in Positive range 1 .. Number_Of_Arguments loop
--# accept F, 10, Opt_Value, "So far no arguments have a value...";
Parse_Option
(S => SPARK.Ada.Command_Line.Unbounded_String.Argument (N),
Valid => Opt_Is_Valid,
Has_Value => Opt_Has_Value,
Option => Opt_Name,
Value => Opt_Value);
--# end accept;
--# assert Number_Of_Arguments = Number_Of_Arguments%
--# and Number_Of_Arguments = SPARK.Ada.Command_Line.Argument_Count (SPARK.Ada.Command_Line.State)
--# and Status = Ok;
if Opt_Is_Valid then
if SPARK.Ada.Strings.Unbounded.Equal_Unbounded_String_String (Opt_Name, "examiner") then
Opt_Is_Valid := not Opt_Has_Value;
Opt_Is_Valid := Opt_Is_Valid and not Data.Files_To_Delete (Files.Examiner_Files);
Data.Files_To_Delete (Files.Examiner_Files) := True;
elsif SPARK.Ada.Strings.Unbounded.Equal_Unbounded_String_String (Opt_Name, "simplifier") then
Opt_Is_Valid := not Opt_Has_Value;
Opt_Is_Valid := Opt_Is_Valid and
not Data.Files_To_Delete (Files.Simplifier_Files);
Data.Files_To_Delete (Files.Simplifier_Files) := True;
elsif SPARK.Ada.Strings.Unbounded.Equal_Unbounded_String_String (Opt_Name, "victor") then
Opt_Is_Valid := not Opt_Has_Value;
Opt_Is_Valid := Opt_Is_Valid and not Data.Files_To_Delete (Files.Victor_Files);
Data.Files_To_Delete (Files.Victor_Files) := True;
elsif SPARK.Ada.Strings.Unbounded.Equal_Unbounded_String_String (Opt_Name, "pogs") then
Opt_Is_Valid := not Opt_Has_Value;
Opt_Is_Valid := Opt_Is_Valid and not Data.Files_To_Delete (Files.POGS_Files);
Data.Files_To_Delete (Files.POGS_Files) := True;
elsif SPARK.Ada.Strings.Unbounded.Equal_Unbounded_String_String (Opt_Name, "help") then
Opt_Is_Valid := not Opt_Has_Value;
Status := Help;
else
-- Unknown option.
Opt_Is_Valid := False;
end if;
end if;
-- If the option was not valid for any reason, we flag up
-- an error.
if not Opt_Is_Valid then
SPARK.Ada.Text_IO.Put_Error ("Invalid option: `");
SPARK.Ada.Text_IO.Unbounded_String.Put_Error (SPARK.Ada.Command_Line.Unbounded_String.Argument (N));
SPARK.Ada.Text_IO.Put_Line_Error ("'");
Status := Error;
end if;
-- There is no point in carrying on if we're not Ok.
exit when not (Status = Ok);
end loop;
end if;
--# accept F, 33, Opt_Value, "So far, none of our arguments have a value, so...";
end Initialize;
end Command_Line;
|
