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
223
224
225
226
227
228
229
230
231
232
233
234
235
236
237
238
239
240
241
242
243
244
245
246
247
248
249
250
251
252
253
254
255
256
257
258
259
260
261
262
263
264
265
266
267
268
269
270
271
272
273
274
275
276
277
278
279
280
281
282
283
284
285
286
287
288
289
290
291
292
293
294
295
296
297
298
299
300
301
302
303
304
305
306
307
308
309
310
311
312
313
314
315
316
317
318
319
320
321
|
-------------------------------------------------------------------------------
-- (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 E_Strings.Not_SPARK;
with FatalErrors;
with GNAT.Directory_Operations;
with GNAT.IO_Aux;
with GNAT.OS_Lib;
package body OSFiling is
------------------------------------------------------------------------------
--
-- Given a path, this function changes directory to that path and returns a
-- string containing the full path. Useful when you have a path such as "."
-- or ".." and you want to get a meaningful directory name.
--
-- Note: has the side-effect of changing the current directory to be the
-- specified directory so if that isn't what you want then save the current
-- directory before calling this function, then cd back to it afterwards.
--
-- Note also that the returned directory name will have a trailing slash
-- that you may have to deal with.
--
-- If the specified path doesn't exist then a fatal error is reported.
--
------------------------------------------------------------------------------
function CD_And_Get_Name (Path : E_Strings.T) return GNAT.Directory_Operations.Dir_Name_Str is
begin
GNAT.Directory_Operations.Change_Dir (E_Strings.Not_SPARK.Get_String (E_Str => Path));
return GNAT.Directory_Operations.Get_Current_Dir;
exception
when others =>
-- Note: this call will NOT return so the return statement following
-- it will never be executed, but is expected by the compiler.
FatalErrors.Process (FatalErrors.Expected_Directory_Missing, Path);
return "";
end CD_And_Get_Name;
----------------------------------------------------------------------------
function Base_Dir_Name (Path : E_Strings.T) return E_Strings.T is
-- save for later
Current_Dir : constant GNAT.Directory_Operations.Path_Name := GNAT.Directory_Operations.Get_Current_Dir;
Full_Path_With_Slash : constant String := CD_And_Get_Name (Path);
Full_Path_No_Slash : constant String :=
Full_Path_With_Slash (1 .. Full_Path_With_Slash'Length - 1);
Base_Name : constant String :=
GNAT.Directory_Operations.Base_Name (Full_Path_No_Slash, "");
begin
GNAT.Directory_Operations.Change_Dir (Current_Dir); -- return to saved dir
return E_Strings.Copy_String (Str => Base_Name);
exception
when others =>
-- Note: this call will NOT return so the return statement following
-- it will never be executed, but is expected by the compiler.
FatalErrors.Process (FatalErrors.Expected_Directory_Missing, Path);
return E_Strings.Empty_String;
end Base_Dir_Name;
----------------------------------------------------------------------------
function Base_Filename (Path : E_Strings.T) return E_Strings.T is
C : constant String := GNAT.Directory_Operations.Base_Name (E_Strings.Not_SPARK.Get_String (E_Str => Path), "");
begin
return E_Strings.Copy_String (Str => C);
end Base_Filename;
----------------------------------------------------------------------------
function Default_Report_Extn return E_Strings.T is
begin
return E_Strings.Copy_String (Str => ".sum");
end Default_Report_Extn;
------------------------------------------------------------------------------
-- this function combines the inputs to produce the path to the
-- subdirectory
function Down_Directory (Path : E_Strings.T;
Sub_Directory : E_Strings.T) return E_Strings.T is
Result : E_Strings.T;
begin
Result := Path;
if E_Strings.Get_Element (E_Str => Path,
Pos => E_Strings.Get_Length (E_Str => Path)) /=
GNAT.Directory_Operations.Dir_Separator then
E_Strings.Append_Char (E_Str => Result,
Ch => GNAT.Directory_Operations.Dir_Separator);
end if;
E_Strings.Append_Examiner_String (E_Str1 => Result,
E_Str2 => Sub_Directory);
return Result;
end Down_Directory;
------------------------------------------------------------------------------
-- this function combines the inputs to produce a full file name
function Full_Filename (Path : E_Strings.T;
Filename : E_Strings.T) return E_Strings.T is
begin
return Down_Directory (Path => Path,
Sub_Directory => Filename);
end Full_Filename;
------------------------------------------------------------------------------
function Get_Working_Directory return E_Strings.T is
--# hide GetWorkingDirectory;
-- save for later
Current_Dir : constant GNAT.Directory_Operations.Path_Name := GNAT.Directory_Operations.Get_Current_Dir;
Cwd : E_Strings.T;
begin
Cwd := E_Strings.Copy_String (Str => Current_Dir);
-- Get_Current_Dir can return a trailing '/' on NT..
if E_Strings.Get_Length (E_Str => Cwd) /= 0
and then E_Strings.Get_Element (E_Str => Cwd,
Pos => E_Strings.Get_Length (E_Str => Cwd)) =
GNAT.Directory_Operations.Dir_Separator then
Cwd := E_Strings.Section (E_Str => Cwd,
Start_Pos => 1,
Length => E_Strings.Get_Length (E_Str => Cwd) - 1);
end if;
return Cwd;
end Get_Working_Directory;
------------------------------------------------------------------------------
function Is_Directory (Name : E_Strings.T) return Boolean is
String_Name : constant String := E_Strings.Not_SPARK.Get_String (E_Str => Name);
begin
return GNAT.OS_Lib.Is_Directory (String_Name);
end Is_Directory;
-----------------------------------------------------------------------------
function Is_File (Name : E_Strings.T) return Boolean is
String_Name : constant String := E_Strings.Not_SPARK.Get_String (E_Str => Name);
begin
return GNAT.IO_Aux.File_Exists (String_Name);
end Is_File;
------------------------------------------------------------------------------
function Order (First_Name, Second_Name : E_Strings.T) return E_Strings.Order_Types is
begin
return E_Strings.Lex_Order (First_Name => First_Name,
Second_Name => Second_Name);
end Order;
------------------------------------------------------------------------------
procedure Remove_File_Extension (Filename : in out E_Strings.T) is
Dot_Pos : E_Strings.Positions;
begin
Dot_Pos := E_Strings.Get_Length (E_Str => Filename);
while Dot_Pos > 1 and then E_Strings.Get_Element (E_Str => Filename,
Pos => Dot_Pos) /= '.' loop
Dot_Pos := Dot_Pos - 1;
end loop;
if E_Strings.Get_Element (E_Str => Filename,
Pos => Dot_Pos) = '.' then
Filename := E_Strings.Section (E_Str => Filename,
Start_Pos => 1,
Length => Dot_Pos - 1);
end if;
end Remove_File_Extension;
----------------------------------------------------------------------------
function Simplified_VC_File_Extension return E_Strings.T is
begin
return E_Strings.Copy_String (Str => ".siv");
end Simplified_VC_File_Extension;
------------------------------------------------------------------------------
function Victored_VC_File_Extension return E_Strings.T is
begin
return E_Strings.Copy_String (Str => ".vct");
end Victored_VC_File_Extension;
------------------------------------------------------------------------------
function Victor_Log_File_Extension return E_Strings.T is
begin
return E_Strings.Copy_String (Str => ".vlg");
end Victor_Log_File_Extension;
------------------------------------------------------------------------------
function Riposte_Summary_File_Extension return E_Strings.T is
begin
return E_Strings.Copy_String (Str => ".rsm");
end Riposte_Summary_File_Extension;
------------------------------------------------------------------------------
-- this function removes the last directory name from the supplied string
function Dir_Name (Path : E_Strings.T) return E_Strings.T is
C : constant String := GNAT.Directory_Operations.Dir_Name (E_Strings.Not_SPARK.Get_String (E_Str => Path));
begin
return E_Strings.Copy_String (Str => C);
end Dir_Name;
----------------------------------------------------------------------------
function VC_File_Extension return E_Strings.T is
begin
return E_Strings.Copy_String (Str => ".vcg");
end VC_File_Extension;
----------------------------------------------------------------------------
function Proof_Log_File_Extension return E_Strings.T is
begin
return E_Strings.Copy_String (Str => ".plg");
end Proof_Log_File_Extension;
----------------------------------------------------------------------------
function Review_File_Extension return E_Strings.T is
begin
return E_Strings.Copy_String (Str => ".prv");
end Review_File_Extension;
----------------------------------------------------------------------------
function Simplifier_Log_File_Extension return E_Strings.T is
begin
return E_Strings.Copy_String (Str => ".slg");
end Simplifier_Log_File_Extension;
----------------------------------------------------------------------------
function DPC_File_Extension return E_Strings.T is
begin
return E_Strings.Copy_String (Str => ".dpc");
end DPC_File_Extension;
----------------------------------------------------------------------------
function Summary_DP_File_Extension return E_Strings.T is
begin
return E_Strings.Copy_String (Str => ".sdp");
end Summary_DP_File_Extension;
----------------------------------------------------------------------------
function Directory_Separator return Character is
begin
return GNAT.Directory_Operations.Dir_Separator;
end Directory_Separator;
----------------------------------------------------------------------------
function Is_Relevant_File (Name : in E_Strings.T) return Boolean is
Extension : E_Strings.T;
-- Stolen from SPARKClean.
-- This function attempts to work out a file's extension. It
-- should do something like this:
-- "foobar.vcg" -> "vcg"
-- ".vcg" -> "vcg"
-- "foobar" -> ""
-- "fail." -> ""
-- "foo.bar.baz" -> "baz"
function Get_Extension (File_Name : in E_Strings.T) return E_Strings.T is
Ext : E_Strings.T;
Ext_Starts_At : Natural;
begin
-- Search for the last '.' in the filename.
Ext_Starts_At := 0;
for N in reverse Natural range 1 .. E_Strings.Get_Length (File_Name) loop
if E_Strings.Get_Element (File_Name, N) = '.' then
Ext_Starts_At := N;
exit;
end if;
end loop;
-- Copy and return the extension, if it exists.
Ext := E_Strings.Empty_String;
if Ext_Starts_At >= 1 and Ext_Starts_At < E_Strings.Get_Length (File_Name) then
for N in Positive range Ext_Starts_At + 1 .. E_Strings.Get_Length (File_Name) loop
E_Strings.Append_Char (Ext, E_Strings.Get_Element (File_Name, N));
end loop;
end if;
return Ext;
end Get_Extension;
begin
Extension := Get_Extension (Name);
return E_Strings.Eq1_String (Extension, "vcg")
or else E_Strings.Eq1_String (Extension, "siv")
or else E_Strings.Eq1_String (Extension, "slg")
or else E_Strings.Eq1_String (Extension, "dpc")
or else E_Strings.Eq1_String (Extension, "sdp")
or else E_Strings.Eq1_String (Extension, "plg")
or else E_Strings.Eq1_String (Extension, "prv")
or else E_Strings.Eq1_String (Extension, "vct")
or else E_Strings.Eq1_String (Extension, "vlg");
end Is_Relevant_File;
end OSFiling;
|
