|
111
|
1 ------------------------------------------------------------------------------
|
|
|
2 -- --
|
|
|
3 -- GNAT COMPILER COMPONENTS --
|
|
|
4 -- --
|
|
|
5 -- S P A R K _ X R E F S --
|
|
|
6 -- --
|
|
|
7 -- S p e c --
|
|
|
8 -- --
|
|
|
9 -- Copyright (C) 2011-2017, Free Software Foundation, Inc. --
|
|
|
10 -- --
|
|
|
11 -- GNAT is free software; you can redistribute it and/or modify it under --
|
|
|
12 -- terms of the GNU General Public License as published by the Free Soft- --
|
|
|
13 -- ware Foundation; either version 3, or (at your option) any later ver- --
|
|
|
14 -- sion. GNAT is distributed in the hope that it will be useful, but WITH- --
|
|
|
15 -- OUT ANY WARRANTY; without even the implied warranty of MERCHANTABILITY --
|
|
|
16 -- or FITNESS FOR A PARTICULAR PURPOSE. See the GNU General Public License --
|
|
|
17 -- for more details. You should have received a copy of the GNU General --
|
|
|
18 -- Public License distributed with GNAT; see file COPYING3. If not, go to --
|
|
|
19 -- http://www.gnu.org/licenses for a complete copy of the license. --
|
|
|
20 -- --
|
|
|
21 -- GNAT was originally developed by the GNAT team at New York University. --
|
|
|
22 -- Extensive contributions were provided by Ada Core Technologies Inc. --
|
|
|
23 -- --
|
|
|
24 ------------------------------------------------------------------------------
|
|
|
25
|
|
|
26 -- This package defines tables used to store information needed for the SPARK
|
|
|
27 -- mode. It is used by procedures in Lib.Xref.SPARK_Specific to build the
|
|
|
28 -- SPARK-specific cross-reference information before writing it to the ALI
|
|
|
29 -- file, and by Get_SPARK_Xrefs/Put_SPARK_Xrefs to read/write the textual
|
|
|
30 -- representation that is stored in the ALI file.
|
|
|
31
|
|
|
32 with Table;
|
|
|
33 with Types; use Types;
|
|
|
34
|
|
|
35 package SPARK_Xrefs is
|
|
|
36
|
|
|
37 -- SPARK cross-reference information can exist in one of two forms. In
|
|
|
38 -- the ALI file, it is represented using a text format that is described
|
|
|
39 -- in this specification. Internally it is stored using three tables:
|
|
|
40 -- SPARK_Xref_Table, SPARK_Scope_Table and SPARK_File_Table, which are
|
|
|
41 -- also defined in this unit.
|
|
|
42
|
|
|
43 -- Lib.Xref.SPARK_Specific is part of the compiler. It extracts SPARK
|
|
|
44 -- cross-reference information from the complete set of cross-references
|
|
|
45 -- generated during compilation.
|
|
|
46
|
|
|
47 -- Get_SPARK_Xrefs reads the text lines in ALI format and populates the
|
|
|
48 -- internal tables with corresponding information.
|
|
|
49
|
|
|
50 -- Put_SPARK_Xrefs reads the internal tables and generates text lines in
|
|
|
51 -- the ALI format.
|
|
|
52
|
|
|
53 ----------------------------
|
|
|
54 -- SPARK Xrefs ALI Format --
|
|
|
55 ----------------------------
|
|
|
56
|
|
|
57 -- SPARK cross-reference information is generated on a unit-by-unit basis
|
|
|
58 -- in the ALI file, using lines that start with the identifying character F
|
|
|
59 -- ("Formal"). These lines are generated if GNATprove_Mode is True.
|
|
|
60
|
|
|
61 -- The SPARK cross-reference information comes after the shared
|
|
|
62 -- cross-reference information, so it can be ignored by tools like
|
|
|
63 -- gnatbind, gnatmake, etc.
|
|
|
64
|
|
|
65 -- -------------------
|
|
|
66 -- -- Scope Section --
|
|
|
67 -- -------------------
|
|
|
68
|
|
|
69 -- A first section defines the scopes in which entities are defined and
|
|
|
70 -- referenced. A scope is a package/subprogram/protected_type/task_type
|
|
|
71 -- declaration/body. Note that a package declaration and body define two
|
|
|
72 -- different scopes. Similarly, a subprogram, protected type and task type
|
|
|
73 -- declaration and body, when both present, define two different scopes.
|
|
|
74
|
|
|
75 -- FD dependency-number filename (-> unit-filename)?
|
|
|
76
|
|
|
77 -- This header precedes scope information for the unit identified by
|
|
|
78 -- dependency number and file name. The dependency number is the index
|
|
|
79 -- into the generated D lines and is ones-origin (e.g. 2 = reference to
|
|
|
80 -- second generated D line).
|
|
|
81
|
|
|
82 -- The list of FD lines should match the list of D lines defined in the
|
|
|
83 -- ALI file, in the same order.
|
|
|
84
|
|
|
85 -- Note that the filename here will reflect the original name if a
|
|
|
86 -- Source_Reference pragma was encountered (since all line number
|
|
|
87 -- references will be with respect to the original file).
|
|
|
88
|
|
|
89 -- Note: the filename is redundant in that it could be deduced from the
|
|
|
90 -- corresponding D line, but it is convenient at least for human
|
|
|
91 -- reading of the SPARK cross-reference information, and means that
|
|
|
92 -- the SPARK cross-reference information can stand on its own without
|
|
|
93 -- needing other parts of the ALI file.
|
|
|
94
|
|
|
95 -- The optional unit filename is given only for subunits.
|
|
|
96
|
|
|
97 -- FS . scope line type col entity (-> spec-file . spec-scope)?
|
|
|
98
|
|
|
99 -- (The ? mark stands for an optional entry in the syntax)
|
|
|
100
|
|
|
101 -- scope is the ones-origin scope number for the current file (e.g. 2 =
|
|
|
102 -- reference to the second FS line in this FD block).
|
|
|
103
|
|
|
104 -- line is the line number of the scope entity. The name of the entity
|
|
|
105 -- starts in column col. Columns are numbered from one, and if
|
|
|
106 -- horizontal tab characters are present, the column number is computed
|
|
|
107 -- assuming standard 1,9,17,.. tab stops. For example, if the entity is
|
|
|
108 -- the first token on the line, and is preceded by space-HT-space, then
|
|
|
109 -- the column would be column 10.
|
|
|
110
|
|
|
111 -- type is a single letter identifying the type of the entity, using
|
|
|
112 -- the same code as in cross-references:
|
|
|
113
|
|
|
114 -- K = package (k = generic package)
|
|
|
115 -- V = function (v = generic function)
|
|
|
116 -- U = procedure (u = generic procedure)
|
|
|
117 -- Y = entry
|
|
|
118
|
|
|
119 -- col is the column number of the scope entity
|
|
|
120
|
|
|
121 -- entity is the name of the scope entity, with casing in the canonical
|
|
|
122 -- casing for the source file where it is defined.
|
|
|
123
|
|
|
124 -- spec-file and spec-scope are respectively the file and scope for the
|
|
|
125 -- spec corresponding to the current body scope, when they differ.
|
|
|
126
|
|
|
127 -- ------------------
|
|
|
128 -- -- Xref Section --
|
|
|
129 -- ------------------
|
|
|
130
|
|
|
131 -- A second section defines cross-references useful for computing global
|
|
|
132 -- variables read/written in each subprogram/package/protected_type/
|
|
|
133 -- task_type.
|
|
|
134
|
|
|
135 -- FX dependency-number filename . entity-number entity
|
|
|
136
|
|
|
137 -- dependency-number and filename identify a file in FD lines
|
|
|
138
|
|
|
139 -- entity-number and entity identify a scope in FS lines
|
|
|
140 -- for the previously identified file.
|
|
|
141
|
|
|
142 -- (filename and entity are just a textual representations of
|
|
|
143 -- dependency-number and entity-number)
|
|
|
144
|
|
|
145 -- F line typ col entity ref*
|
|
|
146
|
|
|
147 -- line is the line number of the referenced entity
|
|
|
148
|
|
|
149 -- typ is the type of the referenced entity, using a code similar to
|
|
|
150 -- the one used for cross-references:
|
|
|
151
|
|
|
152 -- > = IN parameter
|
|
|
153 -- < = OUT parameter
|
|
|
154 -- = = IN OUT parameter
|
|
|
155 -- * = all other cases
|
|
|
156
|
|
|
157 -- col is the column number of the referenced entity
|
|
|
158
|
|
|
159 -- entity is the name of the referenced entity as written in the source
|
|
|
160 -- file where it is defined.
|
|
|
161
|
|
|
162 -- There may be zero or more ref entries on each line
|
|
|
163
|
|
|
164 -- (file |)? ((. scope :)? line type col)*
|
|
|
165
|
|
|
166 -- file is the dependency number of the file with the reference. It and
|
|
|
167 -- the following vertical bar are omitted if the file is the same as
|
|
|
168 -- the previous ref, and the refs for the current file are first (and
|
|
|
169 -- do not need a bar).
|
|
|
170
|
|
|
171 -- scope is the scope number of the scope with the reference. It and
|
|
|
172 -- the following colon are omitted if the scope is the same as the
|
|
|
173 -- previous ref, and the refs for the current scope are first (and do
|
|
|
174 -- not need a colon).
|
|
|
175
|
|
|
176 -- line is the line number of the reference
|
|
|
177
|
|
|
178 -- col is the column number of the reference
|
|
|
179
|
|
|
180 -- type is one of the following, using the same code as in
|
|
|
181 -- cross-references:
|
|
|
182
|
|
|
183 -- m = modification
|
|
|
184 -- r = reference
|
|
|
185 -- c = reference to constant object
|
|
|
186 -- s = subprogram reference in a static call
|
|
|
187
|
|
|
188 -- Special entries for reads and writes to memory reference a special
|
|
|
189 -- variable called "__HEAP". These special entries are present in every
|
|
|
190 -- scope where reads and writes to memory are present. Line and column for
|
|
|
191 -- this special variable are always 0.
|
|
|
192
|
|
|
193 -- Examples: ??? add examples here
|
|
|
194
|
|
|
195 -- -------------------------------
|
|
|
196 -- -- Generated Globals Section --
|
|
|
197 -- -------------------------------
|
|
|
198
|
|
|
199 -- The Generated Globals section is located at the end of the ALI file
|
|
|
200
|
|
|
201 -- All lines with information related to the Generated Globals begin with
|
|
|
202 -- string "GG". This string should therefore not be used in the beginning
|
|
|
203 -- of any line not related to Generated Globals.
|
|
|
204
|
|
|
205 -- The processing (reading and writing) of this section happens in package
|
|
|
206 -- Flow_Generated_Globals (from the SPARK 2014 sources), for further
|
|
|
207 -- information please refer there.
|
|
|
208
|
|
|
209 ----------------
|
|
|
210 -- Xref Table --
|
|
|
211 ----------------
|
|
|
212
|
|
|
213 -- The following table records SPARK cross-references
|
|
|
214
|
|
|
215 type Xref_Index is new Nat;
|
|
|
216 -- Used to index values in this table. Values start at 1 and are assigned
|
|
|
217 -- sequentially as entries are constructed; value 0 is used temporarily
|
|
|
218 -- until a proper value is determined.
|
|
|
219
|
|
|
220 type SPARK_Xref_Record is record
|
|
|
221 Entity_Name : String_Ptr;
|
|
|
222 -- Pointer to entity name in ALI file
|
|
|
223
|
|
|
224 Entity_Line : Nat;
|
|
|
225 -- Line number for the entity referenced
|
|
|
226
|
|
|
227 Etype : Character;
|
|
|
228 -- Indicates type of entity, using code used in ALI file:
|
|
|
229 -- > = IN parameter
|
|
|
230 -- < = OUT parameter
|
|
|
231 -- = = IN OUT parameter
|
|
|
232 -- * = all other cases
|
|
|
233
|
|
|
234 Entity_Col : Nat;
|
|
|
235 -- Column number for the entity referenced
|
|
|
236
|
|
|
237 File_Num : Nat;
|
|
|
238 -- File dependency number for the cross-reference. Note that if no file
|
|
|
239 -- entry is present explicitly, this is just a copy of the reference for
|
|
|
240 -- the current cross-reference section.
|
|
|
241
|
|
|
242 Scope_Num : Nat;
|
|
|
243 -- Scope number for the cross-reference. Note that if no scope entry is
|
|
|
244 -- present explicitly, this is just a copy of the reference for the
|
|
|
245 -- current cross-reference section.
|
|
|
246
|
|
|
247 Line : Nat;
|
|
|
248 -- Line number for the reference
|
|
|
249
|
|
|
250 Rtype : Character;
|
|
|
251 -- Indicates type of the reference, using code used in ALI file:
|
|
|
252 -- r = reference
|
|
|
253 -- c = reference to constant object
|
|
|
254 -- m = modification
|
|
|
255 -- s = call
|
|
|
256
|
|
|
257 Col : Nat;
|
|
|
258 -- Column number for the reference
|
|
|
259 end record;
|
|
|
260
|
|
|
261 package SPARK_Xref_Table is new Table.Table (
|
|
|
262 Table_Component_Type => SPARK_Xref_Record,
|
|
|
263 Table_Index_Type => Xref_Index,
|
|
|
264 Table_Low_Bound => 1,
|
|
|
265 Table_Initial => 2000,
|
|
|
266 Table_Increment => 300,
|
|
|
267 Table_Name => "Xref_Table");
|
|
|
268
|
|
|
269 -----------------
|
|
|
270 -- Scope Table --
|
|
|
271 -----------------
|
|
|
272
|
|
|
273 -- This table keeps track of the scopes and the corresponding starting and
|
|
|
274 -- ending indexes (From, To) in the Xref table.
|
|
|
275
|
|
|
276 type Scope_Index is new Nat;
|
|
|
277 -- Used to index values in this table. Values start at 1 and are assigned
|
|
|
278 -- sequentially as entries are constructed; value 0 indicates that no
|
|
|
279 -- entries have been constructed and is also used until a proper value is
|
|
|
280 -- determined.
|
|
|
281
|
|
|
282 type SPARK_Scope_Record is record
|
|
|
283 Scope_Name : String_Ptr;
|
|
|
284 -- Pointer to scope name in ALI file
|
|
|
285
|
|
|
286 File_Num : Nat;
|
|
|
287 -- Set to the file dependency number for the scope
|
|
|
288
|
|
|
289 Scope_Num : Pos;
|
|
|
290 -- Set to the scope number for the scope
|
|
|
291
|
|
|
292 Spec_File_Num : Nat;
|
|
|
293 -- Set to the file dependency number for the scope corresponding to the
|
|
|
294 -- spec of the current scope entity, if different, or else 0.
|
|
|
295
|
|
|
296 Spec_Scope_Num : Nat;
|
|
|
297 -- Set to the scope number for the scope corresponding to the spec of
|
|
|
298 -- the current scope entity, if different, or else 0.
|
|
|
299
|
|
|
300 Line : Nat;
|
|
|
301 -- Line number for the scope
|
|
|
302
|
|
|
303 Stype : Character;
|
|
|
304 -- Indicates type of scope, using code used in ALI file:
|
|
|
305 -- K = package
|
|
|
306 -- T = task
|
|
|
307 -- U = procedure
|
|
|
308 -- V = function
|
|
|
309 -- Y = entry
|
|
|
310
|
|
|
311 Col : Nat;
|
|
|
312 -- Column number for the scope
|
|
|
313
|
|
|
314 From_Xref : Xref_Index;
|
|
|
315 -- Starting index in Xref table for this scope
|
|
|
316
|
|
|
317 To_Xref : Xref_Index;
|
|
|
318 -- Ending index in Xref table for this scope
|
|
|
319
|
|
|
320 -- The following component is only used in-memory, not printed out in
|
|
|
321 -- ALI file.
|
|
|
322
|
|
|
323 Scope_Entity : Entity_Id := Empty;
|
|
|
324 -- Entity (subprogram or package) for the scope
|
|
|
325 end record;
|
|
|
326
|
|
|
327 package SPARK_Scope_Table is new Table.Table (
|
|
|
328 Table_Component_Type => SPARK_Scope_Record,
|
|
|
329 Table_Index_Type => Scope_Index,
|
|
|
330 Table_Low_Bound => 1,
|
|
|
331 Table_Initial => 200,
|
|
|
332 Table_Increment => 300,
|
|
|
333 Table_Name => "Scope_Table");
|
|
|
334
|
|
|
335 ----------------
|
|
|
336 -- File Table --
|
|
|
337 ----------------
|
|
|
338
|
|
|
339 -- This table keeps track of the units and the corresponding starting and
|
|
|
340 -- ending indexes (From, To) in the Scope table.
|
|
|
341
|
|
|
342 type File_Index is new Nat;
|
|
|
343 -- Used to index values in this table. Values start at 1 and are assigned
|
|
|
344 -- sequentially as entries are constructed; value 0 indicates that no
|
|
|
345 -- entries have been constructed.
|
|
|
346
|
|
|
347 type SPARK_File_Record is record
|
|
|
348 File_Name : String_Ptr;
|
|
|
349 -- Pointer to file name in ALI file
|
|
|
350
|
|
|
351 Unit_File_Name : String_Ptr;
|
|
|
352 -- Pointer to file name for unit in ALI file, when File_Name refers to a
|
|
|
353 -- subunit; otherwise null.
|
|
|
354
|
|
|
355 File_Num : Nat;
|
|
|
356 -- Dependency number in ALI file
|
|
|
357
|
|
|
358 From_Scope : Scope_Index;
|
|
|
359 -- Starting index in Scope table for this unit
|
|
|
360
|
|
|
361 To_Scope : Scope_Index;
|
|
|
362 -- Ending index in Scope table for this unit
|
|
|
363 end record;
|
|
|
364
|
|
|
365 package SPARK_File_Table is new Table.Table (
|
|
|
366 Table_Component_Type => SPARK_File_Record,
|
|
|
367 Table_Index_Type => File_Index,
|
|
|
368 Table_Low_Bound => 1,
|
|
|
369 Table_Initial => 20,
|
|
|
370 Table_Increment => 200,
|
|
|
371 Table_Name => "File_Table");
|
|
|
372
|
|
|
373 ---------------
|
|
|
374 -- Constants --
|
|
|
375 ---------------
|
|
|
376
|
|
|
377 Name_Of_Heap_Variable : constant String := "__HEAP";
|
|
|
378 -- Name of special variable used in effects to denote reads and writes
|
|
|
379 -- through explicit dereference.
|
|
|
380
|
|
|
381 -----------------
|
|
|
382 -- Subprograms --
|
|
|
383 -----------------
|
|
|
384
|
|
|
385 procedure Initialize_SPARK_Tables;
|
|
|
386 -- Reset tables for a new compilation
|
|
|
387
|
|
|
388 procedure dspark;
|
|
|
389 -- Debug routine to dump internal SPARK cross-reference tables. This is a
|
|
|
390 -- raw format dump showing exactly what the tables contain.
|
|
|
391
|
|
|
392 procedure pspark;
|
|
|
393 -- Debugging procedure to output contents of SPARK cross-reference binary
|
|
|
394 -- tables in the format in which they appear in an ALI file.
|
|
|
395
|
|
|
396 end SPARK_Xrefs;
|
