Mercurial > hg > CbC > CbC_gcc
comparison gcc/ada/spark_xrefs.ads @ 131:84e7813d76e9
gcc-8.2
author | mir3636 |
---|---|
date | Thu, 25 Oct 2018 07:37:49 +0900 |
parents | 04ced10e8804 |
children | 1830386684a0 |
comparison
equal
deleted
inserted
replaced
111:04ced10e8804 | 131:84e7813d76e9 |
---|---|
4 -- -- | 4 -- -- |
5 -- S P A R K _ X R E F S -- | 5 -- S P A R K _ X R E F S -- |
6 -- -- | 6 -- -- |
7 -- S p e c -- | 7 -- S p e c -- |
8 -- -- | 8 -- -- |
9 -- Copyright (C) 2011-2017, Free Software Foundation, Inc. -- | 9 -- Copyright (C) 2011-2018, Free Software Foundation, Inc. -- |
10 -- -- | 10 -- -- |
11 -- GNAT is free software; you can redistribute it and/or modify it under -- | 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- -- | 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- -- | 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- -- | 14 -- sion. GNAT is distributed in the hope that it will be useful, but WITH- -- |
21 -- GNAT was originally developed by the GNAT team at New York University. -- | 21 -- GNAT was originally developed by the GNAT team at New York University. -- |
22 -- Extensive contributions were provided by Ada Core Technologies Inc. -- | 22 -- Extensive contributions were provided by Ada Core Technologies Inc. -- |
23 -- -- | 23 -- -- |
24 ------------------------------------------------------------------------------ | 24 ------------------------------------------------------------------------------ |
25 | 25 |
26 -- This package defines tables used to store information needed for the SPARK | 26 -- This package defines data structures used to expose frontend |
27 -- mode. It is used by procedures in Lib.Xref.SPARK_Specific to build the | 27 -- cross-references to the SPARK backend. |
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 | 28 |
32 with Table; | 29 with Types; use Types; |
33 with Types; use Types; | |
34 | 30 |
35 package SPARK_Xrefs is | 31 package SPARK_Xrefs is |
36 | 32 |
37 -- SPARK cross-reference information can exist in one of two forms. In | 33 type SPARK_Xref_Record is record |
38 -- the ALI file, it is represented using a text format that is described | 34 Entity : Entity_Id; |
39 -- in this specification. Internally it is stored using three tables: | 35 -- Referenced entity |
40 -- SPARK_Xref_Table, SPARK_Scope_Table and SPARK_File_Table, which are | |
41 -- also defined in this unit. | |
42 | 36 |
43 -- Lib.Xref.SPARK_Specific is part of the compiler. It extracts SPARK | 37 Ref_Scope : Entity_Id; |
44 -- cross-reference information from the complete set of cross-references | 38 -- Scope where the reference occurs |
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 | 39 |
250 Rtype : Character; | 40 Rtype : Character; |
251 -- Indicates type of the reference, using code used in ALI file: | 41 -- Indicates type of the reference, using code used in ALI file: |
252 -- r = reference | 42 -- r = reference |
253 -- c = reference to constant object | |
254 -- m = modification | 43 -- m = modification |
255 -- s = call | 44 -- s = call |
256 | |
257 Col : Nat; | |
258 -- Column number for the reference | |
259 end record; | 45 end record; |
260 | 46 -- This type holds a subset of the frontend xref entry that is needed by |
261 package SPARK_Xref_Table is new Table.Table ( | 47 -- the SPARK backend. |
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 | 48 |
373 --------------- | 49 --------------- |
374 -- Constants -- | 50 -- Constants -- |
375 --------------- | 51 --------------- |
376 | 52 |
377 Name_Of_Heap_Variable : constant String := "__HEAP"; | 53 Name_Of_Heap_Variable : constant String := "__HEAP"; |
378 -- Name of special variable used in effects to denote reads and writes | 54 -- Name of special variable used in effects to denote reads and writes |
379 -- through explicit dereference. | 55 -- through explicit dereference. |
380 | 56 |
57 Heap : Entity_Id := Empty; | |
58 -- A special entity which denotes the heap object; it should be considered | |
59 -- constant, but needs to be variable, because it can only be initialized | |
60 -- after the node tables are created. | |
61 | |
381 ----------------- | 62 ----------------- |
382 -- Subprograms -- | 63 -- Subprograms -- |
383 ----------------- | 64 ----------------- |
384 | |
385 procedure Initialize_SPARK_Tables; | |
386 -- Reset tables for a new compilation | |
387 | 65 |
388 procedure dspark; | 66 procedure dspark; |
389 -- Debug routine to dump internal SPARK cross-reference tables. This is a | 67 -- Debug routine to dump internal SPARK cross-reference tables. This is a |
390 -- raw format dump showing exactly what the tables contain. | 68 -- raw format dump showing exactly what the tables contain. |
391 | 69 |
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; | 70 end SPARK_Xrefs; |