[gcc/testsuite]
[official-gcc.git] / gcc / ada / spark_xrefs.ads
blobfd5b76d4a66ea87439ef9e417daa796a5c0dd106
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 ------------------------------------------------------------------------------
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.
32 with Table;
33 with Types; use Types;
35 package SPARK_Xrefs is
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.
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.
47 -- Get_SPARK_Xrefs reads the text lines in ALI format and populates the
48 -- internal tables with corresponding information.
50 -- Put_SPARK_Xrefs reads the internal tables and generates text lines in
51 -- the ALI format.
53 ----------------------------
54 -- SPARK Xrefs ALI Format --
55 ----------------------------
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.
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.
65 -- -------------------
66 -- -- Scope Section --
67 -- -------------------
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.
75 -- FD dependency-number filename (-> unit-filename)?
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).
82 -- The list of FD lines should match the list of D lines defined in the
83 -- ALI file, in the same order.
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).
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.
95 -- The optional unit filename is given only for subunits.
97 -- FS . scope line type col entity (-> spec-file . spec-scope)?
99 -- (The ? mark stands for an optional entry in the syntax)
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).
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.
111 -- type is a single letter identifying the type of the entity, using
112 -- the same code as in cross-references:
114 -- K = package (k = generic package)
115 -- V = function (v = generic function)
116 -- U = procedure (u = generic procedure)
117 -- Y = entry
119 -- col is the column number of the scope entity
121 -- entity is the name of the scope entity, with casing in the canonical
122 -- casing for the source file where it is defined.
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.
127 -- ------------------
128 -- -- Xref Section --
129 -- ------------------
131 -- A second section defines cross-references useful for computing global
132 -- variables read/written in each subprogram/package/protected_type/
133 -- task_type.
135 -- FX dependency-number filename . entity-number entity
137 -- dependency-number and filename identify a file in FD lines
139 -- entity-number and entity identify a scope in FS lines
140 -- for the previously identified file.
142 -- (filename and entity are just a textual representations of
143 -- dependency-number and entity-number)
145 -- F line typ col entity ref*
147 -- line is the line number of the referenced entity
149 -- typ is the type of the referenced entity, using a code similar to
150 -- the one used for cross-references:
152 -- > = IN parameter
153 -- < = OUT parameter
154 -- = = IN OUT parameter
155 -- * = all other cases
157 -- col is the column number of the referenced entity
159 -- entity is the name of the referenced entity as written in the source
160 -- file where it is defined.
162 -- There may be zero or more ref entries on each line
164 -- (file |)? ((. scope :)? line type col)*
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).
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).
176 -- line is the line number of the reference
178 -- col is the column number of the reference
180 -- type is one of the following, using the same code as in
181 -- cross-references:
183 -- m = modification
184 -- r = reference
185 -- c = reference to constant object
186 -- s = subprogram reference in a static call
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.
193 -- Examples: ??? add examples here
195 -- -------------------------------
196 -- -- Generated Globals Section --
197 -- -------------------------------
199 -- The Generated Globals section is located at the end of the ALI file
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.
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.
209 ----------------
210 -- Xref Table --
211 ----------------
213 -- The following table records SPARK cross-references
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.
220 type SPARK_Xref_Record is record
221 Entity_Name : String_Ptr;
222 -- Pointer to entity name in ALI file
224 Entity_Line : Nat;
225 -- Line number for the entity referenced
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
234 Entity_Col : Nat;
235 -- Column number for the entity referenced
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.
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.
247 Line : Nat;
248 -- Line number for the reference
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
257 Col : Nat;
258 -- Column number for the reference
259 end record;
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");
269 -----------------
270 -- Scope Table --
271 -----------------
273 -- This table keeps track of the scopes and the corresponding starting and
274 -- ending indexes (From, To) in the Xref table.
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.
282 type SPARK_Scope_Record is record
283 Scope_Name : String_Ptr;
284 -- Pointer to scope name in ALI file
286 File_Num : Nat;
287 -- Set to the file dependency number for the scope
289 Scope_Num : Pos;
290 -- Set to the scope number for the scope
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.
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.
300 Line : Nat;
301 -- Line number for the scope
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
311 Col : Nat;
312 -- Column number for the scope
314 From_Xref : Xref_Index;
315 -- Starting index in Xref table for this scope
317 To_Xref : Xref_Index;
318 -- Ending index in Xref table for this scope
320 -- The following component is only used in-memory, not printed out in
321 -- ALI file.
323 Scope_Entity : Entity_Id := Empty;
324 -- Entity (subprogram or package) for the scope
325 end record;
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");
335 ----------------
336 -- File Table --
337 ----------------
339 -- This table keeps track of the units and the corresponding starting and
340 -- ending indexes (From, To) in the Scope table.
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.
347 type SPARK_File_Record is record
348 File_Name : String_Ptr;
349 -- Pointer to file name in ALI file
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.
355 File_Num : Nat;
356 -- Dependency number in ALI file
358 From_Scope : Scope_Index;
359 -- Starting index in Scope table for this unit
361 To_Scope : Scope_Index;
362 -- Ending index in Scope table for this unit
363 end record;
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");
373 ---------------
374 -- Constants --
375 ---------------
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.
381 -----------------
382 -- Subprograms --
383 -----------------
385 procedure Initialize_SPARK_Tables;
386 -- Reset tables for a new compilation
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.
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.
396 end SPARK_Xrefs;