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
322
323
324
325
326
327
328
329
330
331
332
333
334
335
336
337
338
339
340
341
342
343
344
345
346
347
348
349
350
351
352
353
354
355
356
357
358
359
360
361
362
363
364
365
366
367
368
369
370
371
372
373
374
375
376
377
|
-------------------------------------------------------------------------------
-- (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 ErrorHandler;
with E_Strings;
with LexTokenLists;
with LexTokenManager;
with SparkLex;
with SPARK_IO;
with STree;
use type LexTokenLists.Lists;
use type LexTokenManager.Str_Comp_Result;
use type SPARK_IO.File_Status;
use type STree.Iterator;
--# inherit CommandLineData,
--# ContextManager,
--# Dictionary,
--# ErrorHandler,
--# ExaminerConstants,
--# E_Strings,
--# FileSystem,
--# IndexManager,
--# LexTokenLists,
--# LexTokenManager,
--# ScreenEcho,
--# SparkLex,
--# SPARK_IO,
--# SP_Symbols,
--# STree,
--# SystemErrors;
package ContextManager.Ops
--# own File_Heap : File_Heaps;
--# Unit_Heap : Unit_Heaps;
--# Unit_Stack : Unit_Stacks;
--# initializes File_Heap,
--# Unit_Heap,
--# Unit_Stack;
is
procedure Open_File (File_Descriptor : in ContextManager.FileDescriptors);
--# global in CommandLineData.Content;
--# in Dictionary.Dict;
--# in LexTokenManager.State;
--# in out ErrorHandler.Error_Context;
--# in out File_Heap;
--# in out SparkLex.Curr_Line;
--# in out SPARK_IO.File_Sys;
--# derives ErrorHandler.Error_Context,
--# File_Heap,
--# SPARK_IO.File_Sys from CommandLineData.Content,
--# Dictionary.Dict,
--# ErrorHandler.Error_Context,
--# File_Descriptor,
--# File_Heap,
--# LexTokenManager.State,
--# SPARK_IO.File_Sys &
--# SparkLex.Curr_Line from *,
--# File_Descriptor,
--# File_Heap,
--# LexTokenManager.State,
--# SPARK_IO.File_Sys;
procedure Close_File (File_Descriptor : in ContextManager.FileDescriptors);
--# global in out File_Heap;
--# in out SPARK_IO.File_Sys;
--# derives File_Heap,
--# SPARK_IO.File_Sys from *,
--# File_Descriptor,
--# File_Heap;
function Current_Unit return ContextManager.UnitDescriptors;
--# global in Unit_Stack;
function Get_Unit_Status (Unit_Descriptor : ContextManager.UnitDescriptors) return ContextManager.UnitStatus;
--# global in Unit_Heap;
procedure Create_Unit_Descriptor
(File_Descriptor : in ContextManager.FileDescriptors;
Unit_Descriptor : out ContextManager.UnitDescriptors);
--# global in out File_Heap;
--# in out Unit_Heap;
--# derives File_Heap,
--# Unit_Heap from *,
--# File_Descriptor,
--# File_Heap &
--# Unit_Descriptor from Unit_Heap;
function Get_File_Descriptor (Unit_Descriptor : ContextManager.UnitDescriptors) return ContextManager.FileDescriptors;
--# global in Unit_Heap;
procedure SetUnitStatus (Descriptor : in ContextManager.UnitDescriptors;
Status : in ContextManager.UnitStatus);
--# global in out Unit_Heap;
--# derives Unit_Heap from *,
--# Descriptor,
--# Status;
function GetFileStatus (Descriptor : ContextManager.FileDescriptors) return ContextManager.FileStatus;
--# global in File_Heap;
procedure SetVCG (Descriptor : in ContextManager.UnitDescriptors;
VCG : in Boolean);
--# global in out Unit_Heap;
--# derives Unit_Heap from *,
--# Descriptor,
--# VCG;
procedure GetVCG (Descriptor : in ContextManager.UnitDescriptors;
VCG : out Boolean);
--# global in Unit_Heap;
--# derives VCG from Descriptor,
--# Unit_Heap;
procedure GetUnitByName
(UnitName : in LexTokenLists.Lists;
UnitTypeSet : in ContextManager.UnitTypeSets;
Descriptor : out ContextManager.UnitDescriptors);
--# global in LexTokenManager.State;
--# in Unit_Heap;
--# derives Descriptor from LexTokenManager.State,
--# UnitName,
--# UnitTypeSet,
--# Unit_Heap;
procedure SetUnitName
(Descriptor : in ContextManager.UnitDescriptors;
UnitName : in LexTokenLists.Lists;
UnitType : in ContextManager.UnitTypes);
--# global in out Unit_Heap;
--# derives Unit_Heap from *,
--# Descriptor,
--# UnitName,
--# UnitType;
procedure GetUnitName
(Descriptor : in ContextManager.UnitDescriptors;
UnitName : out LexTokenLists.Lists;
UnitType : out ContextManager.UnitTypes);
--# global in Unit_Heap;
--# derives UnitName,
--# UnitType from Descriptor,
--# Unit_Heap;
procedure SetParseTree (Descriptor : in ContextManager.UnitDescriptors;
ParseTree : in STree.SyntaxNode);
--# global in STree.Table;
--# in out Unit_Heap;
--# derives Unit_Heap from *,
--# Descriptor,
--# ParseTree,
--# STree.Table;
procedure GetParseTree (Descriptor : in ContextManager.UnitDescriptors;
ParseTree : out STree.SyntaxNode);
--# global in Unit_Heap;
--# derives ParseTree from Descriptor,
--# Unit_Heap;
procedure MarkUnitInCycle (Descriptor : in ContextManager.UnitDescriptors);
--# global in out Unit_Heap;
--# derives Unit_Heap from *,
--# Descriptor;
function UnitInCycle (Descriptor : ContextManager.UnitDescriptors) return Boolean;
--# global in Unit_Heap;
function FirstUnitDescriptor return ContextManager.UnitDescriptors;
--# global in Unit_Heap;
function NextUnitDescriptor (Descriptor : ContextManager.UnitDescriptors) return ContextManager.UnitDescriptors;
--# global in Unit_Heap;
procedure PushUnit (Descriptor : in ContextManager.UnitDescriptors);
--# global in out Unit_Stack;
--# derives Unit_Stack from *,
--# Descriptor;
procedure PopUnit (Descriptor : out ContextManager.UnitDescriptors);
--# global in out Unit_Stack;
--# derives Descriptor,
--# Unit_Stack from Unit_Stack;
procedure CreateFileDescriptor (Descriptor : out ContextManager.FileDescriptors);
--# global in out File_Heap;
--# derives Descriptor,
--# File_Heap from File_Heap;
procedure SetSourceFileName (Descriptor : in ContextManager.FileDescriptors;
SourceFileName : in LexTokenManager.Lex_String);
--# global in out File_Heap;
--# derives File_Heap from *,
--# Descriptor,
--# SourceFileName;
function GetSourceFileName (Descriptor : in ContextManager.FileDescriptors) return LexTokenManager.Lex_String;
--# global in File_Heap;
procedure GetSourceFile (Descriptor : in ContextManager.FileDescriptors;
SourceFile : out SPARK_IO.File_Type);
--# global in File_Heap;
--# derives SourceFile from Descriptor,
--# File_Heap;
function ListingReqt (Descriptor : ContextManager.FileDescriptors) return Boolean;
--# global in File_Heap;
function FirstFileDescriptor return ContextManager.FileDescriptors;
--# global in File_Heap;
function NextFileDescriptor (Descriptor : ContextManager.FileDescriptors) return ContextManager.FileDescriptors;
--# global in File_Heap;
function GetFileByName (FileName : in LexTokenManager.Lex_String) return ContextManager.FileDescriptors;
--# global in File_Heap;
--# in LexTokenManager.State;
procedure SetFileStatus (Descriptor : in ContextManager.FileDescriptors;
Status : in ContextManager.FileStatus);
--# global in out File_Heap;
--# derives File_Heap from *,
--# Descriptor,
--# Status;
procedure SetListingReq (Descriptor : in ContextManager.FileDescriptors;
Req : in Boolean);
--# global in out File_Heap;
--# derives File_Heap from *,
--# Descriptor,
--# Req;
procedure SetLineContext (Descriptor : in ContextManager.FileDescriptors;
FileContext : in SparkLex.Line_Context);
--# global in out File_Heap;
--# derives File_Heap from *,
--# Descriptor,
--# FileContext;
procedure GetLineContext (Descriptor : in ContextManager.FileDescriptors;
FileContext : out SparkLex.Line_Context);
--# global in File_Heap;
--# derives FileContext from Descriptor,
--# File_Heap;
procedure SetErrorContext (Descriptor : in ContextManager.FileDescriptors;
Context : in ErrorHandler.Error_Contexts);
--# global in out File_Heap;
--# derives File_Heap from *,
--# Context,
--# Descriptor;
procedure GetErrorContext (Descriptor : in ContextManager.FileDescriptors;
Context : out ErrorHandler.Error_Contexts);
--# global in File_Heap;
--# derives Context from Descriptor,
--# File_Heap;
procedure SetListingFileName (Descriptor : in ContextManager.FileDescriptors;
Listing_File_Name : in E_Strings.T);
--# global in out File_Heap;
--# derives File_Heap from *,
--# Descriptor,
--# Listing_File_Name;
procedure GetListingFileName (Descriptor : in ContextManager.FileDescriptors;
Listing_File_Name : out E_Strings.T);
--# global in File_Heap;
--# derives Listing_File_Name from Descriptor,
--# File_Heap;
procedure SetErrorsReported (Descriptor : in ContextManager.FileDescriptors);
--# global in out File_Heap;
--# derives File_Heap from *,
--# Descriptor;
function ErrorsReported (Descriptor : ContextManager.FileDescriptors) return Boolean;
--# global in File_Heap;
-- Find the compilation unit descriptor associated with the file
-- descriptor (Descriptor). Each compilation unit has only one
-- file but each file can contain many compilation units. This
-- function must only be used for the SLI generation because, in
-- the case of GNAT source code, each file has only one
-- compilation unit.
procedure Get_Unit (Descriptor : in ContextManager.FileDescriptors;
Unit_Descriptor : out ContextManager.UnitDescriptors);
--# global in CommandLineData.Content;
--# in Dictionary.Dict;
--# in LexTokenManager.State;
--# in STree.Table;
--# in Unit_Heap;
--# in out ErrorHandler.Error_Context;
--# in out SPARK_IO.File_Sys;
--# derives ErrorHandler.Error_Context,
--# SPARK_IO.File_Sys from CommandLineData.Content,
--# Descriptor,
--# Dictionary.Dict,
--# ErrorHandler.Error_Context,
--# LexTokenManager.State,
--# SPARK_IO.File_Sys,
--# STree.Table,
--# Unit_Heap &
--# Unit_Descriptor from Descriptor,
--# Unit_Heap;
-- Get the parent of an Ada separate unit (Unit_Descriptor).
procedure Get_Parent (Unit_Descriptor : in out ContextManager.UnitDescriptors);
--# global in LexTokenManager.State;
--# in Unit_Heap;
--# derives Unit_Descriptor from *,
--# LexTokenManager.State,
--# Unit_Heap;
-- The procedure marks all the compilation units that are in the
-- closure of the compilation unit associated with the file
-- descriptor (Descriptor). Each compilation unit has only one
-- file but each file can contain many compilation units. This
-- function must only be used for the SLI generation because, in
-- the case of GNAT source code, each file has only one
-- compilation unit. This procedure must be called before the
-- function In_Closure.
procedure Dependency_Closure (Descriptor : in ContextManager.FileDescriptors);
--# global in CommandLineData.Content;
--# in Dictionary.Dict;
--# in STree.Table;
--# in out ErrorHandler.Error_Context;
--# in out IndexManager.State;
--# in out LexTokenManager.State;
--# in out SPARK_IO.File_Sys;
--# in out Unit_Heap;
--# derives ErrorHandler.Error_Context,
--# IndexManager.State,
--# LexTokenManager.State,
--# SPARK_IO.File_Sys,
--# Unit_Heap from CommandLineData.Content,
--# Descriptor,
--# Dictionary.Dict,
--# ErrorHandler.Error_Context,
--# IndexManager.State,
--# LexTokenManager.State,
--# SPARK_IO.File_Sys,
--# STree.Table,
--# Unit_Heap;
-- Return TRUE if the compilation unit descriptor (Descriptor) is
-- in the closure of the compilation unit calculated by
-- Dependency_Closure. The procedure Dependency_Closure must be
-- called before this function.
function In_Closure (Descriptor : in ContextManager.UnitDescriptors) return Boolean;
--# global in Unit_Heap;
-- Set the line number of the "D ..." line (see D section of the
-- ALI format).
procedure Set_Line_Number (Descriptor : in ContextManager.UnitDescriptors;
Line_Number : in Positive);
--# global in out Unit_Heap;
--# derives Unit_Heap from *,
--# Descriptor,
--# Line_Number;
-- Get the line number of the "D ..." line (see D section of the
-- ALI format).
function Get_Line_Number (Descriptor : in ContextManager.UnitDescriptors) return Natural;
--# global in Unit_Heap;
end ContextManager.Ops;
|
