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
|
-------------------------------------------------------------------------------
-- (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.
--
--=============================================================================
--------------------------------------------------------------------------------
--Synopsis: --
-- --
--Package combining Heap and FileDetails to give an ordered list of files --
-- --
--This is implemented as an abstract state machine. This is possible as there --
--is only a single occurrence of the FileHeap in the program. It is necessary --
--to prevent unacceptable overheads of creating local copies of the embedded --
--Heap and FileDetails types to circumvent the entire variable rule. It would --
--also be possible to implement Heap and FileDetails as ASMs but not --
--necessarily desirable as this would affect the high level annotations of the--
--program. --
-- --
--------------------------------------------------------------------------------
with E_Strings, FileDetails, Heap;
use type Heap.Atom;
--# inherit E_Strings,
--# FatalErrors,
--# FileDetails,
--# Heap,
--# HeapIndex;
package FileHeap
--# own State;
is
-- StartIndex is a point in the linked list at which to start the
-- search. This is used to start insertion at the parent directory name
-- If the file table is full, a fatal error is produced and Add does not
-- return
procedure Add (StartIndex : in Heap.Atom;
NewName : in E_Strings.T;
NewFileType : in FileDetails.FileTypes);
--# global in out FatalErrors.State;
--# in out State;
--# derives FatalErrors.State,
--# State from *,
--# NewFileType,
--# NewName,
--# StartIndex,
--# State;
--------------------------------------------------------------------------
-- this procedure returns the file details for the specified entry in the
-- linked list. Success if ListIndex points to a heap record which points to
-- a valid set of file details
procedure Details
(ListIndex : in Heap.Atom;
Success : out Boolean;
Name : out E_Strings.T;
FileType : out FileDetails.FileTypes;
DirectoryIsResolved : out Boolean);
--# global in State;
--# derives DirectoryIsResolved,
--# FileType,
--# Name,
--# Success from ListIndex,
--# State;
--------------------------------------------------------------------------
function FirstEntry return Heap.Atom;
--# global in State;
--------------------------------------------------------------------------
procedure Initialize (TopDirectory : in E_Strings.T);
--# global out State;
--# derives State from TopDirectory;
--------------------------------------------------------------------------
procedure MarkDirectoryResolved (ListIndex : in Heap.Atom);
--# global in out State;
--# derives State from *,
--# ListIndex;
--------------------------------------------------------------------------
-- this procedure returns the 'NextOne' ordered element in FH after
-- 'AfterThis'. It is successful if the NextOne is not a 'null' pointer
procedure Next (AfterThis : in Heap.Atom;
Success : out Boolean;
NextOne : out Heap.Atom);
--# global in State;
--# derives NextOne,
--# Success from AfterThis,
--# State;
end FileHeap;
|
