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
|
-------------------------------------------------------------------------------
-- (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.Characters.Latin_1;
with E_Strings;
with E_Strings.Not_SPARK;
with FatalErrors;
with FileDetails;
with FileHeap;
with GNAT.Directory_Operations;
with OSFiling;
package body OSDirectory is
------------------------------------------------------------------------
-- this procedure reads the named directory using the C calls
-- opendir(), readdir() and closedir()
-- for each entry, it calls OSFiling.IsDirectory and then enters it in the
-- linked list
------------------------------------------------------------------------
procedure Scan (ListIndex : in Heap.Atom) is
--# hide Scan;
DetailsSuccess : Boolean;
FileType : FileDetails.FileTypes;
DirectoryIsResolved : Boolean;
TempName : String (1 .. 1024);
BaseName, DirName, Filename : E_Strings.T;
Dir : GNAT.Directory_Operations.Dir_Type;
Last : Natural;
-- Convert a regular string into an Examiner string. You may
-- be tempted to refactor this using E_Strings.Copy_String, but
-- note that we are given a fixed length string which is padded
-- with NUL so it won't work.
function Create_Examiner_String (Str : in String) return E_Strings.T is
E_Str : E_Strings.T := E_Strings.Empty_String;
Pos : E_Strings.Positions := 1;
begin
while Str (Pos) /= Ada.Characters.Latin_1.NUL loop
E_Strings.Append_Char (E_Str => E_Str,
Ch => Str (Pos));
Pos := Pos + 1;
end loop;
return E_Str;
end Create_Examiner_String;
--------------------------------------------------------------------------
begin -- ScanDirectory
-- retrieve directory details
FileHeap.Details (ListIndex, DetailsSuccess, DirName, FileType, DirectoryIsResolved);
if not DetailsSuccess then
FatalErrors.Process (FatalErrors.Data_Structure_Inconsistency, E_Strings.Empty_String);
end if;
-- block to trap exceptions from Open
begin
-- Read from DirName
GNAT.Directory_Operations.Open (Dir => Dir,
Dir_Name => E_Strings.Not_SPARK.Get_String (E_Str => DirName));
exception
when others =>
-- note: this call will NOT return
FatalErrors.Process (FatalErrors.Expected_Directory_Missing, DirName);
end;
-- Now repeatedly read a file from the directory
loop
-- read the file
TempName := (others => Ada.Characters.Latin_1.NUL);
GNAT.Directory_Operations.Read (Dir, TempName, Last);
if Last = 0 then
exit;
end if;
-- Ignore dot files; hidden Unix ones, and ., ..
if TempName (1) /= '.' then
-- Create a proper name
BaseName := Create_Examiner_String (Str => TempName);
Filename := OSFiling.Down_Directory (Path => DirName,
Sub_Directory => BaseName);
-- Breadth-first search; add any directory to our
-- to-do list
if OSFiling.Is_Directory (Name => Filename) then
FileHeap.Add (ListIndex, Filename, FileDetails.Directory);
else
-- It's a vanilla file; get its full name
Filename := OSFiling.Full_Filename (Path => DirName,
Filename => BaseName);
-- Check if it may be relevant. We need to do this
-- here to guard against JC17-010 on
-- Windows. Otherwise we may look at something like
-- FOO.rep which would result in a duplicate analysis
-- of foo.vcg.
if OSFiling.Is_Relevant_File (Filename) then
-- Remove the extension
OSFiling.Remove_File_Extension (Filename);
FileHeap.Add (ListIndex, Filename, FileDetails.PlainFile);
end if;
end if; -- IsDirectory
end if; -- TempName(1) /= '.'
end loop; -- infinite
GNAT.Directory_Operations.Close (Dir);
end Scan;
end OSDirectory;
|
