]>
Commit | Line | Data |
---|---|---|
56e94186 AC |
1 | ------------------------------------------------------------------------------ |
2 | -- -- | |
3 | -- GNAT COMPILER COMPONENTS -- | |
4 | -- -- | |
06b599fd | 5 | -- L I B . X R E F . S P A R K _ S P E C I F I C -- |
56e94186 AC |
6 | -- -- |
7 | -- B o d y -- | |
8 | -- -- | |
ed323421 | 9 | -- Copyright (C) 2011-2017, Free Software Foundation, Inc. -- |
56e94186 AC |
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 | ||
63b5225b YM |
26 | with Einfo; use Einfo; |
27 | with Nmake; use Nmake; | |
9db78a42 | 28 | with SPARK_Xrefs; use SPARK_Xrefs; |
996c8821 | 29 | |
56e94186 AC |
30 | with GNAT.HTable; |
31 | ||
32 | separate (Lib.Xref) | |
06b599fd | 33 | package body SPARK_Specific is |
56e94186 AC |
34 | |
35 | --------------------- | |
36 | -- Local Constants -- | |
37 | --------------------- | |
38 | ||
06b599fd | 39 | -- Table of SPARK_Entities, True for each entity kind used in SPARK |
e917aec2 | 40 | |
06b599fd | 41 | SPARK_Entities : constant array (Entity_Kind) of Boolean := |
cdc96e3e | 42 | (E_Constant => True, |
7b52257c | 43 | E_Entry => True, |
cdc96e3e AC |
44 | E_Function => True, |
45 | E_In_Out_Parameter => True, | |
46 | E_In_Parameter => True, | |
47 | E_Loop_Parameter => True, | |
48 | E_Operator => True, | |
49 | E_Out_Parameter => True, | |
50 | E_Procedure => True, | |
51 | E_Variable => True, | |
52 | others => False); | |
56e94186 | 53 | |
06b599fd | 54 | -- True for each reference type used in SPARK |
5b0113d6 | 55 | |
06b599fd | 56 | SPARK_References : constant array (Character) of Boolean := |
80007176 AC |
57 | ('m' => True, |
58 | 'r' => True, | |
59 | 's' => True, | |
56e94186 AC |
60 | others => False); |
61 | ||
9466892f AC |
62 | type Entity_Hashed_Range is range 0 .. 255; |
63 | -- Size of hash table headers | |
64 | ||
226a7fa4 AC |
65 | --------------------- |
66 | -- Local Variables -- | |
67 | --------------------- | |
68 | ||
69 | package Drefs is new Table.Table ( | |
70 | Table_Component_Type => Xref_Entry, | |
71 | Table_Index_Type => Xref_Entry_Number, | |
72 | Table_Low_Bound => 1, | |
ce5c2061 YM |
73 | Table_Initial => Alloc.Drefs_Initial, |
74 | Table_Increment => Alloc.Drefs_Increment, | |
226a7fa4 AC |
75 | Table_Name => "Drefs"); |
76 | -- Table of cross-references for reads and writes through explicit | |
77 | -- dereferences, that are output as reads/writes to the special variable | |
c01817d2 | 78 | -- "Heap". These references are added to the regular references when |
06b599fd | 79 | -- computing SPARK cross-references. |
226a7fa4 | 80 | |
56e94186 AC |
81 | ----------------------- |
82 | -- Local Subprograms -- | |
83 | ----------------------- | |
84 | ||
7ffbef99 | 85 | procedure Add_SPARK_File (Uspec, Ubody : Unit_Number_Type; Dspec : Nat); |
06b599fd | 86 | -- Add file and corresponding scopes for unit to the tables |
7ffbef99 AC |
87 | -- SPARK_File_Table and SPARK_Scope_Table. When two units are present |
88 | -- for the same compilation unit, as it happens for library-level | |
89 | -- instantiations of generics, then Ubody is the number of the body | |
90 | -- unit; otherwise it is No_Unit. | |
56e94186 | 91 | |
06b599fd YM |
92 | procedure Add_SPARK_Xrefs; |
93 | -- Filter table Xrefs to add all references used in SPARK to the table | |
94 | -- SPARK_Xref_Table. | |
56e94186 | 95 | |
9466892f AC |
96 | function Entity_Hash (E : Entity_Id) return Entity_Hashed_Range; |
97 | -- Hash function for hash table | |
98 | ||
06b599fd YM |
99 | -------------------- |
100 | -- Add_SPARK_File -- | |
101 | -------------------- | |
56e94186 | 102 | |
7ffbef99 | 103 | procedure Add_SPARK_File (Uspec, Ubody : Unit_Number_Type; Dspec : Nat) is |
4b985e20 | 104 | File : constant Source_File_Index := Source_Index (Uspec); |
7ffbef99 | 105 | From : constant Scope_Index := SPARK_Scope_Table.Last + 1; |
56e94186 | 106 | |
7ffbef99 | 107 | Scope_Id : Pos := 1; |
56e94186 | 108 | |
7ffbef99 AC |
109 | procedure Add_SPARK_Scope (N : Node_Id); |
110 | -- Add scope N to the table SPARK_Scope_Table | |
56e94186 | 111 | |
7ffbef99 AC |
112 | procedure Detect_And_Add_SPARK_Scope (N : Node_Id); |
113 | -- Call Add_SPARK_Scope on scopes | |
a5150cb1 | 114 | |
7ffbef99 AC |
115 | --------------------- |
116 | -- Add_SPARK_Scope -- | |
117 | --------------------- | |
56e94186 | 118 | |
7ffbef99 | 119 | procedure Add_SPARK_Scope (N : Node_Id) is |
013e9958 | 120 | E : constant Entity_Id := Defining_Entity (N); |
56e94186 | 121 | |
b5ea9143 | 122 | begin |
7ffbef99 | 123 | -- Ignore scopes without a proper location |
1f163ef7 | 124 | |
7ffbef99 AC |
125 | if Sloc (N) = No_Location then |
126 | return; | |
127 | end if; | |
56e94186 | 128 | |
7ffbef99 | 129 | case Ekind (E) is |
d8f43ee6 HK |
130 | when E_Entry |
131 | | E_Entry_Family | |
7cc7f3aa | 132 | | E_Function |
d8f43ee6 HK |
133 | | E_Generic_Function |
134 | | E_Generic_Package | |
135 | | E_Generic_Procedure | |
136 | | E_Package | |
013e9958 | 137 | | E_Package_Body |
7cc7f3aa | 138 | | E_Procedure |
013e9958 | 139 | | E_Protected_Body |
d8f43ee6 | 140 | | E_Protected_Type |
013e9958 | 141 | | E_Task_Body |
d8f43ee6 | 142 | | E_Task_Type |
d8f43ee6 | 143 | | E_Subprogram_Body |
d8f43ee6 | 144 | => |
013e9958 | 145 | null; |
80007176 AC |
146 | |
147 | when E_Void => | |
148 | ||
149 | -- Compilation of prj-attr.adb with -gnatn creates a node with | |
150 | -- entity E_Void for the package defined at a-charac.ads16:13. | |
151 | -- ??? TBD | |
56e94186 | 152 | |
80007176 AC |
153 | return; |
154 | ||
155 | when others => | |
156 | raise Program_Error; | |
7ffbef99 AC |
157 | end case; |
158 | ||
159 | -- File_Num and Scope_Num are filled later. From_Xref and To_Xref | |
160 | -- are filled even later, but are initialized to represent an empty | |
161 | -- range. | |
162 | ||
163 | SPARK_Scope_Table.Append | |
76b37a56 PMR |
164 | ((Entity => E, |
165 | Scope_Num => Scope_Id, | |
166 | From_Xref => 1, | |
167 | To_Xref => 0)); | |
7ffbef99 AC |
168 | |
169 | Scope_Id := Scope_Id + 1; | |
170 | end Add_SPARK_Scope; | |
171 | ||
172 | -------------------------------- | |
173 | -- Detect_And_Add_SPARK_Scope -- | |
174 | -------------------------------- | |
175 | ||
176 | procedure Detect_And_Add_SPARK_Scope (N : Node_Id) is | |
177 | begin | |
80007176 AC |
178 | -- Entries |
179 | ||
180 | if Nkind_In (N, N_Entry_Body, N_Entry_Declaration) | |
181 | ||
182 | -- Packages | |
183 | ||
184 | or else Nkind_In (N, N_Package_Body, | |
80007176 AC |
185 | N_Package_Declaration) |
186 | -- Protected units | |
187 | ||
188 | or else Nkind_In (N, N_Protected_Body, | |
80007176 AC |
189 | N_Protected_Type_Declaration) |
190 | ||
191 | -- Subprograms | |
192 | ||
193 | or else Nkind_In (N, N_Subprogram_Body, | |
80007176 AC |
194 | N_Subprogram_Declaration) |
195 | ||
196 | -- Task units | |
197 | ||
198 | or else Nkind_In (N, N_Task_Body, | |
80007176 | 199 | N_Task_Type_Declaration) |
7ffbef99 AC |
200 | then |
201 | Add_SPARK_Scope (N); | |
202 | end if; | |
203 | end Detect_And_Add_SPARK_Scope; | |
204 | ||
205 | procedure Traverse_Scopes is new | |
206 | Traverse_Compilation_Unit (Detect_And_Add_SPARK_Scope); | |
207 | ||
208 | -- Start of processing for Add_SPARK_File | |
209 | ||
210 | begin | |
211 | -- Source file could be inexistant as a result of an error, if option | |
212 | -- gnatQ is used. | |
213 | ||
cd644ae2 | 214 | if File <= No_Source_File then |
7ffbef99 AC |
215 | return; |
216 | end if; | |
217 | ||
218 | -- Subunits are traversed as part of the top-level unit to which they | |
219 | -- belong. | |
220 | ||
221 | if Nkind (Unit (Cunit (Uspec))) = N_Subunit then | |
222 | return; | |
223 | end if; | |
224 | ||
784ef0fb | 225 | Traverse_Scopes (CU => Cunit (Uspec)); |
7ffbef99 AC |
226 | |
227 | -- When two units are present for the same compilation unit, as it | |
228 | -- happens for library-level instantiations of generics, then add all | |
229 | -- scopes to the same SPARK file. | |
230 | ||
231 | if Ubody /= No_Unit then | |
784ef0fb | 232 | Traverse_Scopes (CU => Cunit (Ubody)); |
7ffbef99 AC |
233 | end if; |
234 | ||
7ffbef99 | 235 | SPARK_File_Table.Append ( |
00b3de22 PT |
236 | (File_Num => Dspec, |
237 | From_Scope => From, | |
238 | To_Scope => SPARK_Scope_Table.Last)); | |
7ffbef99 | 239 | end Add_SPARK_File; |
56e94186 | 240 | |
06b599fd YM |
241 | --------------------- |
242 | -- Add_SPARK_Xrefs -- | |
243 | --------------------- | |
56e94186 | 244 | |
06b599fd | 245 | procedure Add_SPARK_Xrefs is |
cdc96e3e AC |
246 | function Entity_Of_Scope (S : Scope_Index) return Entity_Id; |
247 | -- Return the entity which maps to the input scope index | |
248 | ||
5067f3a0 PMR |
249 | function Get_Scope_Num (E : Entity_Id) return Nat; |
250 | -- Return the scope number associated with the entity E | |
80007176 | 251 | |
24fd21c3 AC |
252 | function Is_Future_Scope_Entity |
253 | (E : Entity_Id; | |
254 | S : Scope_Index) return Boolean; | |
255 | -- Check whether entity E is in SPARK_Scope_Table at index S or higher | |
256 | ||
06b599fd | 257 | function Is_SPARK_Reference |
cdc96e3e AC |
258 | (E : Entity_Id; |
259 | Typ : Character) return Boolean; | |
06b599fd YM |
260 | -- Return whether entity reference E meets SPARK requirements. Typ is |
261 | -- the reference type. | |
cdc96e3e | 262 | |
06b599fd | 263 | function Is_SPARK_Scope (E : Entity_Id) return Boolean; |
cdc96e3e | 264 | -- Return whether the entity or reference scope meets requirements for |
8e2d104b | 265 | -- being a SPARK scope. |
cdc96e3e | 266 | |
cdc96e3e AC |
267 | function Lt (Op1 : Natural; Op2 : Natural) return Boolean; |
268 | -- Comparison function for Sort call | |
269 | ||
270 | procedure Move (From : Natural; To : Natural); | |
271 | -- Move procedure for Sort call | |
272 | ||
5067f3a0 PMR |
273 | procedure Set_Scope_Num (E : Entity_Id; Num : Nat); |
274 | -- Associate entity E with the scope number Num | |
80007176 | 275 | |
cdc96e3e AC |
276 | procedure Update_Scope_Range |
277 | (S : Scope_Index; | |
278 | From : Xref_Index; | |
279 | To : Xref_Index); | |
280 | -- Update the scope which maps to S with the new range From .. To | |
281 | ||
282 | package Sorting is new GNAT.Heap_Sort_G (Move, Lt); | |
56e94186 | 283 | |
e0adfeb4 AC |
284 | No_Scope : constant Nat := 0; |
285 | -- Initial scope counter | |
286 | ||
e0adfeb4 AC |
287 | package Scopes is new GNAT.HTable.Simple_HTable |
288 | (Header_Num => Entity_Hashed_Range, | |
5067f3a0 PMR |
289 | Element => Nat, |
290 | No_Element => No_Scope, | |
e0adfeb4 AC |
291 | Key => Entity_Id, |
292 | Hash => Entity_Hash, | |
293 | Equal => "="); | |
eff69022 | 294 | -- Package used to build a correspondence between entities and scope |
06b599fd | 295 | -- numbers used in SPARK cross references. |
5b0113d6 | 296 | |
56e94186 AC |
297 | Nrefs : Nat := Xrefs.Last; |
298 | -- Number of references in table. This value may get reset (reduced) | |
299 | -- when we eliminate duplicate reference entries as well as references | |
300 | -- not suitable for local cross-references. | |
301 | ||
226a7fa4 | 302 | Nrefs_Add : constant Nat := Drefs.Last; |
ce5c2061 YM |
303 | -- Number of additional references which correspond to dereferences in |
304 | -- the source code. | |
226a7fa4 AC |
305 | |
306 | Rnums : array (0 .. Nrefs + Nrefs_Add) of Nat; | |
56e94186 AC |
307 | -- This array contains numbers of references in the Xrefs table. This |
308 | -- list is sorted in output order. The extra 0'th entry is convenient | |
4f94fa11 | 309 | -- for the call to sort. When we sort the table, we move the indices in |
56e94186 AC |
310 | -- Rnums around, but we do not move the original table entries. |
311 | ||
cdc96e3e AC |
312 | --------------------- |
313 | -- Entity_Of_Scope -- | |
314 | --------------------- | |
56e94186 | 315 | |
cdc96e3e AC |
316 | function Entity_Of_Scope (S : Scope_Index) return Entity_Id is |
317 | begin | |
45a6947d | 318 | return SPARK_Scope_Table.Table (S).Entity; |
cdc96e3e | 319 | end Entity_Of_Scope; |
56e94186 | 320 | |
e0adfeb4 AC |
321 | ------------------- |
322 | -- Get_Scope_Num -- | |
323 | ------------------- | |
324 | ||
5067f3a0 | 325 | function Get_Scope_Num (E : Entity_Id) return Nat renames Scopes.Get; |
e0adfeb4 | 326 | |
cdc96e3e AC |
327 | ---------------------------- |
328 | -- Is_Future_Scope_Entity -- | |
329 | ---------------------------- | |
330 | ||
331 | function Is_Future_Scope_Entity | |
332 | (E : Entity_Id; | |
333 | S : Scope_Index) return Boolean | |
334 | is | |
335 | function Is_Past_Scope_Entity return Boolean; | |
06b599fd | 336 | -- Check whether entity E is in SPARK_Scope_Table at index strictly |
cdc96e3e AC |
337 | -- lower than S. |
338 | ||
339 | -------------------------- | |
340 | -- Is_Past_Scope_Entity -- | |
341 | -------------------------- | |
342 | ||
343 | function Is_Past_Scope_Entity return Boolean is | |
344 | begin | |
06b599fd | 345 | for Index in SPARK_Scope_Table.First .. S - 1 loop |
45a6947d | 346 | if SPARK_Scope_Table.Table (Index).Entity = E then |
363f2c58 | 347 | return True; |
cdc96e3e AC |
348 | end if; |
349 | end loop; | |
350 | ||
351 | return False; | |
352 | end Is_Past_Scope_Entity; | |
353 | ||
354 | -- Start of processing for Is_Future_Scope_Entity | |
355 | ||
356 | begin | |
06b599fd | 357 | for Index in S .. SPARK_Scope_Table.Last loop |
45a6947d | 358 | if SPARK_Scope_Table.Table (Index).Entity = E then |
cdc96e3e AC |
359 | return True; |
360 | end if; | |
361 | end loop; | |
362 | ||
363 | -- If this assertion fails, this means that the scope which we are | |
364 | -- looking for has been treated already, which reveals a problem in | |
365 | -- the order of cross-references. | |
366 | ||
367 | pragma Assert (not Is_Past_Scope_Entity); | |
368 | ||
369 | return False; | |
370 | end Is_Future_Scope_Entity; | |
371 | ||
24fd21c3 AC |
372 | ------------------------ |
373 | -- Is_SPARK_Reference -- | |
374 | ------------------------ | |
375 | ||
376 | function Is_SPARK_Reference | |
377 | (E : Entity_Id; | |
378 | Typ : Character) return Boolean | |
379 | is | |
380 | begin | |
381 | -- The only references of interest on callable entities are calls. On | |
363f2c58 AC |
382 | -- uncallable entities, the only references of interest are reads and |
383 | -- writes. | |
24fd21c3 AC |
384 | |
385 | if Ekind (E) in Overloadable_Kind then | |
386 | return Typ = 's'; | |
387 | ||
24fd21c3 AC |
388 | -- In all other cases, result is true for reference/modify cases, |
389 | -- and false for all other cases. | |
390 | ||
391 | else | |
392 | return Typ = 'r' or else Typ = 'm'; | |
393 | end if; | |
394 | end Is_SPARK_Reference; | |
395 | ||
396 | -------------------- | |
397 | -- Is_SPARK_Scope -- | |
398 | -------------------- | |
399 | ||
400 | function Is_SPARK_Scope (E : Entity_Id) return Boolean is | |
333e4f86 | 401 | Can_Be_Renamed : constant Boolean := |
13126368 YM |
402 | Present (E) |
403 | and then (Is_Subprogram_Or_Entry (E) | |
404 | or else Ekind (E) = E_Package); | |
24fd21c3 AC |
405 | begin |
406 | return Present (E) | |
407 | and then not Is_Generic_Unit (E) | |
6f77df72 | 408 | and then (not Can_Be_Renamed or else No (Renamed_Entity (E))) |
24fd21c3 AC |
409 | and then Get_Scope_Num (E) /= No_Scope; |
410 | end Is_SPARK_Scope; | |
411 | ||
56e94186 AC |
412 | -------- |
413 | -- Lt -- | |
414 | -------- | |
415 | ||
80007176 | 416 | function Lt (Op1 : Natural; Op2 : Natural) return Boolean is |
56e94186 AC |
417 | T1 : constant Xref_Entry := Xrefs.Table (Rnums (Nat (Op1))); |
418 | T2 : constant Xref_Entry := Xrefs.Table (Rnums (Nat (Op2))); | |
419 | ||
420 | begin | |
e917aec2 | 421 | -- First test: if entity is in different unit, sort by unit. Note: |
56e94186 | 422 | -- that we use Ent_Scope_File rather than Eun, as Eun may refer to |
e917aec2 RD |
423 | -- the file where the generic scope is defined, which may differ from |
424 | -- the file where the enclosing scope is defined. It is the latter | |
425 | -- which matters for a correct order here. | |
56e94186 AC |
426 | |
427 | if T1.Ent_Scope_File /= T2.Ent_Scope_File then | |
428 | return Dependency_Num (T1.Ent_Scope_File) < | |
5b0113d6 | 429 | Dependency_Num (T2.Ent_Scope_File); |
56e94186 AC |
430 | |
431 | -- Second test: within same unit, sort by location of the scope of | |
432 | -- the entity definition. | |
433 | ||
f7bb41af | 434 | elsif Get_Scope_Num (T1.Key.Ent_Scope) /= |
2c17ca0a | 435 | Get_Scope_Num (T2.Key.Ent_Scope) |
56e94186 | 436 | then |
f7bb41af | 437 | return Get_Scope_Num (T1.Key.Ent_Scope) < |
5b0113d6 | 438 | Get_Scope_Num (T2.Key.Ent_Scope); |
56e94186 AC |
439 | |
440 | -- Third test: within same unit and scope, sort by location of | |
441 | -- entity definition. | |
442 | ||
443 | elsif T1.Def /= T2.Def then | |
444 | return T1.Def < T2.Def; | |
445 | ||
e228f7ee AC |
446 | else |
447 | -- Both entities must be equal at this point | |
4b985e20 | 448 | |
e228f7ee | 449 | pragma Assert (T1.Key.Ent = T2.Key.Ent); |
a5150cb1 AC |
450 | pragma Assert (T1.Key.Ent_Scope = T2.Key.Ent_Scope); |
451 | pragma Assert (T1.Ent_Scope_File = T2.Ent_Scope_File); | |
4b985e20 | 452 | |
e228f7ee AC |
453 | -- Fourth test: if reference is in same unit as entity definition, |
454 | -- sort first. | |
56e94186 | 455 | |
e228f7ee AC |
456 | if T1.Key.Lun /= T2.Key.Lun |
457 | and then T1.Ent_Scope_File = T1.Key.Lun | |
458 | then | |
459 | return True; | |
f7bb41af | 460 | |
e228f7ee AC |
461 | elsif T1.Key.Lun /= T2.Key.Lun |
462 | and then T2.Ent_Scope_File = T2.Key.Lun | |
463 | then | |
464 | return False; | |
56e94186 | 465 | |
e228f7ee AC |
466 | -- Fifth test: if reference is in same unit and same scope as |
467 | -- entity definition, sort first. | |
56e94186 | 468 | |
e228f7ee AC |
469 | elsif T1.Ent_Scope_File = T1.Key.Lun |
470 | and then T1.Key.Ref_Scope /= T2.Key.Ref_Scope | |
471 | and then T1.Key.Ent_Scope = T1.Key.Ref_Scope | |
472 | then | |
473 | return True; | |
cdc96e3e | 474 | |
e228f7ee AC |
475 | elsif T2.Ent_Scope_File = T2.Key.Lun |
476 | and then T1.Key.Ref_Scope /= T2.Key.Ref_Scope | |
477 | and then T2.Key.Ent_Scope = T2.Key.Ref_Scope | |
478 | then | |
479 | return False; | |
56e94186 | 480 | |
e228f7ee | 481 | -- Sixth test: for same entity, sort by reference location unit |
56e94186 | 482 | |
e228f7ee AC |
483 | elsif T1.Key.Lun /= T2.Key.Lun then |
484 | return Dependency_Num (T1.Key.Lun) < | |
485 | Dependency_Num (T2.Key.Lun); | |
56e94186 | 486 | |
e228f7ee | 487 | -- Seventh test: for same entity, sort by reference location scope |
56e94186 | 488 | |
e228f7ee AC |
489 | elsif Get_Scope_Num (T1.Key.Ref_Scope) /= |
490 | Get_Scope_Num (T2.Key.Ref_Scope) | |
491 | then | |
492 | return Get_Scope_Num (T1.Key.Ref_Scope) < | |
493 | Get_Scope_Num (T2.Key.Ref_Scope); | |
56e94186 | 494 | |
e228f7ee | 495 | -- Eighth test: order of location within referencing unit |
56e94186 | 496 | |
e228f7ee AC |
497 | elsif T1.Key.Loc /= T2.Key.Loc then |
498 | return T1.Key.Loc < T2.Key.Loc; | |
56e94186 | 499 | |
e228f7ee AC |
500 | -- Finally, for two locations at the same address prefer the one |
501 | -- that does NOT have the type 'r', so that a modification or | |
502 | -- extension takes preference, when there are more than one | |
503 | -- reference at the same location. As a result, in the case of | |
504 | -- entities that are in-out actuals, the read reference follows | |
505 | -- the modify reference. | |
56e94186 | 506 | |
e228f7ee AC |
507 | else |
508 | return T2.Key.Typ = 'r'; | |
509 | end if; | |
56e94186 AC |
510 | end if; |
511 | end Lt; | |
512 | ||
513 | ---------- | |
514 | -- Move -- | |
515 | ---------- | |
516 | ||
517 | procedure Move (From : Natural; To : Natural) is | |
518 | begin | |
519 | Rnums (Nat (To)) := Rnums (Nat (From)); | |
520 | end Move; | |
521 | ||
e0adfeb4 AC |
522 | ------------------- |
523 | -- Set_Scope_Num -- | |
524 | ------------------- | |
525 | ||
5067f3a0 | 526 | procedure Set_Scope_Num (E : Entity_Id; Num : Nat) renames Scopes.Set; |
e0adfeb4 | 527 | |
cdc96e3e AC |
528 | ------------------------ |
529 | -- Update_Scope_Range -- | |
530 | ------------------------ | |
531 | ||
532 | procedure Update_Scope_Range | |
533 | (S : Scope_Index; | |
534 | From : Xref_Index; | |
535 | To : Xref_Index) | |
536 | is | |
537 | begin | |
06b599fd YM |
538 | SPARK_Scope_Table.Table (S).From_Xref := From; |
539 | SPARK_Scope_Table.Table (S).To_Xref := To; | |
cdc96e3e AC |
540 | end Update_Scope_Range; |
541 | ||
542 | -- Local variables | |
543 | ||
cdc96e3e | 544 | From_Index : Xref_Index; |
4f94fa11 | 545 | Prev_Loc : Source_Ptr; |
cdc96e3e AC |
546 | Prev_Typ : Character; |
547 | Ref_Count : Nat; | |
cdc96e3e | 548 | Scope_Id : Scope_Index; |
226a7fa4 | 549 | |
06b599fd | 550 | -- Start of processing for Add_SPARK_Xrefs |
56e94186 | 551 | |
996c8821 | 552 | begin |
06b599fd | 553 | for Index in SPARK_Scope_Table.First .. SPARK_Scope_Table.Last loop |
cdc96e3e | 554 | declare |
06b599fd | 555 | S : SPARK_Scope_Record renames SPARK_Scope_Table.Table (Index); |
cdc96e3e | 556 | begin |
45a6947d | 557 | Set_Scope_Num (S.Entity, S.Scope_Num); |
cdc96e3e | 558 | end; |
56e94186 AC |
559 | end loop; |
560 | ||
54740d7d AC |
561 | declare |
562 | Drefs_Table : Drefs.Table_Type | |
374c09e8 | 563 | renames Drefs.Table (Drefs.First .. Drefs.Last); |
54740d7d AC |
564 | begin |
565 | Xrefs.Append_All (Xrefs.Table_Type (Drefs_Table)); | |
566 | Nrefs := Nrefs + Drefs_Table'Length; | |
567 | end; | |
226a7fa4 | 568 | |
4b985e20 AC |
569 | -- Capture the definition Sloc values. As in the case of normal cross |
570 | -- references, we have to wait until now to get the correct value. | |
571 | ||
572 | for Index in 1 .. Nrefs loop | |
573 | Xrefs.Table (Index).Def := Sloc (Xrefs.Table (Index).Key.Ent); | |
574 | end loop; | |
575 | ||
06b599fd | 576 | -- Eliminate entries not appropriate for SPARK. Done prior to sorting |
e917aec2 RD |
577 | -- cross-references, as it discards useless references which do not have |
578 | -- a proper format for the comparison function (like no location). | |
56e94186 | 579 | |
cdc96e3e AC |
580 | Ref_Count := Nrefs; |
581 | Nrefs := 0; | |
d2b4b3da | 582 | |
cdc96e3e AC |
583 | for Index in 1 .. Ref_Count loop |
584 | declare | |
4f94fa11 | 585 | Ref : Xref_Key renames Xrefs.Table (Index).Key; |
56e94186 | 586 | |
1f9939b5 | 587 | begin |
06b599fd YM |
588 | if SPARK_Entities (Ekind (Ref.Ent)) |
589 | and then SPARK_References (Ref.Typ) | |
590 | and then Is_SPARK_Scope (Ref.Ent_Scope) | |
591 | and then Is_SPARK_Scope (Ref.Ref_Scope) | |
06b599fd | 592 | and then Is_SPARK_Reference (Ref.Ent, Ref.Typ) |
cdc96e3e | 593 | |
5b0113d6 | 594 | -- Discard references from unknown scopes, e.g. generic scopes |
cdc96e3e AC |
595 | |
596 | and then Get_Scope_Num (Ref.Ent_Scope) /= No_Scope | |
597 | and then Get_Scope_Num (Ref.Ref_Scope) /= No_Scope | |
3815f967 AC |
598 | |
599 | -- Discard references to loop parameters introduced within | |
600 | -- expression functions, as they give two references: one from | |
601 | -- the analysis of the expression function itself and one from | |
602 | -- the analysis of the expanded body. We don't lose any globals | |
603 | -- by discarding them, because such loop parameters can only be | |
604 | -- accessed locally from within the expression function body. | |
605 | ||
606 | and then not | |
607 | (Ekind (Ref.Ent) = E_Loop_Parameter | |
608 | and then Scope_Within | |
609 | (Ref.Ent, Unique_Entity (Ref.Ref_Scope)) | |
610 | and then Is_Expression_Function (Ref.Ref_Scope)) | |
56e94186 AC |
611 | then |
612 | Nrefs := Nrefs + 1; | |
4f94fa11 | 613 | Rnums (Nrefs) := Index; |
56e94186 | 614 | end if; |
cdc96e3e AC |
615 | end; |
616 | end loop; | |
56e94186 AC |
617 | |
618 | -- Sort the references | |
619 | ||
620 | Sorting.Sort (Integer (Nrefs)); | |
621 | ||
cdc96e3e | 622 | -- Eliminate duplicate entries |
56e94186 | 623 | |
cdc96e3e AC |
624 | -- We need this test for Ref_Count because if we force ALI file |
625 | -- generation in case of errors detected, it may be the case that | |
626 | -- Nrefs is 0, so we should not reset it here. | |
56e94186 | 627 | |
cdc96e3e AC |
628 | if Nrefs >= 2 then |
629 | Ref_Count := Nrefs; | |
630 | Nrefs := 1; | |
56e94186 | 631 | |
cdc96e3e | 632 | for Index in 2 .. Ref_Count loop |
80007176 | 633 | if Xrefs.Table (Rnums (Index)) /= Xrefs.Table (Rnums (Nrefs)) then |
cdc96e3e AC |
634 | Nrefs := Nrefs + 1; |
635 | Rnums (Nrefs) := Rnums (Index); | |
636 | end if; | |
637 | end loop; | |
638 | end if; | |
56e94186 | 639 | |
cdc96e3e AC |
640 | -- Eliminate the reference if it is at the same location as the previous |
641 | -- one, unless it is a read-reference indicating that the entity is an | |
642 | -- in-out actual in a call. | |
56e94186 | 643 | |
cdc96e3e AC |
644 | Ref_Count := Nrefs; |
645 | Nrefs := 0; | |
4f94fa11 | 646 | Prev_Loc := No_Location; |
cdc96e3e | 647 | Prev_Typ := 'm'; |
56e94186 | 648 | |
cdc96e3e AC |
649 | for Index in 1 .. Ref_Count loop |
650 | declare | |
651 | Ref : Xref_Key renames Xrefs.Table (Rnums (Index)).Key; | |
56e94186 | 652 | |
cdc96e3e | 653 | begin |
4f94fa11 | 654 | if Ref.Loc /= Prev_Loc |
5b0113d6 | 655 | or else (Prev_Typ = 'm' and then Ref.Typ = 'r') |
56e94186 | 656 | then |
4f94fa11 | 657 | Prev_Loc := Ref.Loc; |
cdc96e3e | 658 | Prev_Typ := Ref.Typ; |
56e94186 | 659 | Nrefs := Nrefs + 1; |
cdc96e3e | 660 | Rnums (Nrefs) := Rnums (Index); |
56e94186 | 661 | end if; |
cdc96e3e AC |
662 | end; |
663 | end loop; | |
56e94186 | 664 | |
cdc96e3e | 665 | -- The two steps have eliminated all references, nothing to do |
56e94186 | 666 | |
06b599fd | 667 | if SPARK_Scope_Table.Last = 0 then |
483361a6 | 668 | return; |
56e94186 AC |
669 | end if; |
670 | ||
cdc96e3e AC |
671 | Scope_Id := 1; |
672 | From_Index := 1; | |
673 | ||
56e94186 AC |
674 | -- Loop to output references |
675 | ||
676 | for Refno in 1 .. Nrefs loop | |
cdc96e3e AC |
677 | declare |
678 | Ref_Entry : Xref_Entry renames Xrefs.Table (Rnums (Refno)); | |
679 | Ref : Xref_Key renames Ref_Entry.Key; | |
56e94186 AC |
680 | |
681 | begin | |
e917aec2 | 682 | -- If this assertion fails, the scope which we are looking for is |
06b599fd | 683 | -- not in SPARK scope table, which reveals either a problem in the |
e917aec2 RD |
684 | -- construction of the scope table, or an erroneous scope for the |
685 | -- current cross-reference. | |
56e94186 | 686 | |
5b0113d6 | 687 | pragma Assert (Is_Future_Scope_Entity (Ref.Ent_Scope, Scope_Id)); |
56e94186 | 688 | |
483361a6 AC |
689 | -- Update the range of cross references to which the current scope |
690 | -- refers to. This may be the empty range only for the first scope | |
691 | -- considered. | |
692 | ||
cdc96e3e AC |
693 | if Ref.Ent_Scope /= Entity_Of_Scope (Scope_Id) then |
694 | Update_Scope_Range | |
695 | (S => Scope_Id, | |
696 | From => From_Index, | |
06b599fd | 697 | To => SPARK_Xref_Table.Last); |
cdc96e3e | 698 | |
06b599fd | 699 | From_Index := SPARK_Xref_Table.Last + 1; |
56e94186 AC |
700 | end if; |
701 | ||
cdc96e3e AC |
702 | while Ref.Ent_Scope /= Entity_Of_Scope (Scope_Id) loop |
703 | Scope_Id := Scope_Id + 1; | |
06b599fd | 704 | pragma Assert (Scope_Id <= SPARK_Scope_Table.Last); |
56e94186 AC |
705 | end loop; |
706 | ||
06b599fd | 707 | SPARK_Xref_Table.Append ( |
3e5400f4 | 708 | (Entity => Unique_Entity (Ref.Ent), |
2cf8eabd | 709 | Ref_Scope => Ref.Ref_Scope, |
9ac3cbb3 | 710 | Rtype => Ref.Typ)); |
cdc96e3e | 711 | end; |
56e94186 AC |
712 | end loop; |
713 | ||
483361a6 AC |
714 | -- Update the range of cross references to which the scope refers to |
715 | ||
cdc96e3e AC |
716 | Update_Scope_Range |
717 | (S => Scope_Id, | |
718 | From => From_Index, | |
06b599fd YM |
719 | To => SPARK_Xref_Table.Last); |
720 | end Add_SPARK_Xrefs; | |
56e94186 | 721 | |
06b599fd YM |
722 | ------------------------- |
723 | -- Collect_SPARK_Xrefs -- | |
724 | ------------------------- | |
56e94186 | 725 | |
06b599fd YM |
726 | procedure Collect_SPARK_Xrefs |
727 | (Sdep_Table : Unit_Ref_Table; | |
728 | Num_Sdep : Nat) | |
729 | is | |
80007176 AC |
730 | Sdep : Pos; |
731 | Sdep_Next : Pos; | |
7ffbef99 AC |
732 | -- Index of the current and next source dependency |
733 | ||
734 | Sdep_File : Pos; | |
735 | -- Index of the file to which the scopes need to be assigned; for | |
736 | -- library-level instances of generic units this points to the unit | |
737 | -- of the body, because this is where references are assigned to. | |
738 | ||
80007176 AC |
739 | Ubody : Unit_Number_Type; |
740 | Uspec : Unit_Number_Type; | |
7ffbef99 AC |
741 | -- Unit numbers for the dependency spec and possibly its body (only in |
742 | -- the case of library-level instance of a generic package). | |
4b985e20 | 743 | |
56e94186 AC |
744 | begin |
745 | -- Cross-references should have been computed first | |
746 | ||
747 | pragma Assert (Xrefs.Last /= 0); | |
748 | ||
06b599fd | 749 | Initialize_SPARK_Tables; |
56e94186 | 750 | |
06b599fd | 751 | -- Generate file and scope SPARK cross-reference information |
56e94186 | 752 | |
7ffbef99 AC |
753 | Sdep := 1; |
754 | while Sdep <= Num_Sdep loop | |
4b985e20 | 755 | |
497a660d AC |
756 | -- Skip dependencies with no entity node, e.g. configuration files |
757 | -- with pragmas (.adc) or target description (.atp), since they | |
758 | -- present no interest for SPARK cross references. | |
759 | ||
760 | if No (Cunit_Entity (Sdep_Table (Sdep))) then | |
761 | Sdep_Next := Sdep + 1; | |
762 | ||
7ffbef99 AC |
763 | -- For library-level instantiation of a generic, two consecutive |
764 | -- units refer to the same compilation unit node and entity (one to | |
765 | -- body, one to spec). In that case, treat them as a single unit for | |
766 | -- the sake of SPARK cross references by passing to Add_SPARK_File. | |
4b985e20 | 767 | |
497a660d AC |
768 | else |
769 | if Sdep < Num_Sdep | |
770 | and then Cunit_Entity (Sdep_Table (Sdep)) = | |
771 | Cunit_Entity (Sdep_Table (Sdep + 1)) | |
772 | then | |
773 | declare | |
774 | Cunit1 : Node_Id renames Cunit (Sdep_Table (Sdep)); | |
775 | Cunit2 : Node_Id renames Cunit (Sdep_Table (Sdep + 1)); | |
80007176 | 776 | |
497a660d AC |
777 | begin |
778 | -- Both Cunits point to compilation unit nodes | |
80007176 | 779 | |
497a660d AC |
780 | pragma Assert |
781 | (Nkind (Cunit1) = N_Compilation_Unit | |
782 | and then Nkind (Cunit2) = N_Compilation_Unit); | |
b48a45e3 | 783 | |
497a660d AC |
784 | -- Do not depend on the sorting order, which is based on |
785 | -- Unit_Name, and for library-level instances of nested | |
786 | -- generic packages they are equal. | |
b48a45e3 | 787 | |
497a660d | 788 | -- If declaration comes before the body |
80007176 | 789 | |
497a660d AC |
790 | if Nkind (Unit (Cunit1)) = N_Package_Declaration |
791 | and then Nkind (Unit (Cunit2)) = N_Package_Body | |
792 | then | |
793 | Uspec := Sdep_Table (Sdep); | |
794 | Ubody := Sdep_Table (Sdep + 1); | |
7ffbef99 | 795 | |
497a660d | 796 | Sdep_File := Sdep + 1; |
b48a45e3 | 797 | |
497a660d | 798 | -- If body comes before declaration |
b48a45e3 | 799 | |
497a660d AC |
800 | elsif Nkind (Unit (Cunit1)) = N_Package_Body |
801 | and then Nkind (Unit (Cunit2)) = N_Package_Declaration | |
802 | then | |
803 | Uspec := Sdep_Table (Sdep + 1); | |
804 | Ubody := Sdep_Table (Sdep); | |
7ffbef99 | 805 | |
497a660d | 806 | Sdep_File := Sdep; |
7ffbef99 | 807 | |
497a660d | 808 | -- Otherwise it is an error |
b48a45e3 | 809 | |
497a660d AC |
810 | else |
811 | raise Program_Error; | |
812 | end if; | |
80007176 | 813 | |
497a660d AC |
814 | Sdep_Next := Sdep + 2; |
815 | end; | |
80007176 | 816 | |
497a660d | 817 | -- ??? otherwise? |
7ffbef99 | 818 | |
497a660d AC |
819 | else |
820 | Uspec := Sdep_Table (Sdep); | |
821 | Ubody := No_Unit; | |
4b985e20 | 822 | |
497a660d AC |
823 | Sdep_File := Sdep; |
824 | Sdep_Next := Sdep + 1; | |
825 | end if; | |
ccfe725b | 826 | |
ccfe725b | 827 | Add_SPARK_File |
7ffbef99 AC |
828 | (Uspec => Uspec, |
829 | Ubody => Ubody, | |
830 | Dspec => Sdep_File); | |
ccfe725b JK |
831 | end if; |
832 | ||
7ffbef99 | 833 | Sdep := Sdep_Next; |
56e94186 AC |
834 | end loop; |
835 | ||
06b599fd | 836 | -- Generate SPARK cross-reference information |
56e94186 | 837 | |
06b599fd YM |
838 | Add_SPARK_Xrefs; |
839 | end Collect_SPARK_Xrefs; | |
56e94186 | 840 | |
226a7fa4 AC |
841 | ------------------------------------- |
842 | -- Enclosing_Subprogram_Or_Package -- | |
843 | ------------------------------------- | |
844 | ||
63b5225b YM |
845 | function Enclosing_Subprogram_Or_Library_Package |
846 | (N : Node_Id) return Entity_Id | |
847 | is | |
4871a41d | 848 | Context : Entity_Id; |
226a7fa4 AC |
849 | |
850 | begin | |
851 | -- If N is the defining identifier for a subprogram, then return the | |
852 | -- enclosing subprogram or package, not this subprogram. | |
853 | ||
854 | if Nkind_In (N, N_Defining_Identifier, N_Defining_Operator_Symbol) | |
4871a41d | 855 | and then (Ekind (N) in Entry_Kind |
2c94bbe3 AC |
856 | or else Ekind (N) = E_Subprogram_Body |
857 | or else Ekind (N) in Generic_Subprogram_Kind | |
858 | or else Ekind (N) in Subprogram_Kind) | |
226a7fa4 | 859 | then |
4871a41d | 860 | Context := Parent (Unit_Declaration_Node (N)); |
f6f40114 | 861 | |
4871a41d | 862 | -- If this was a library-level subprogram then replace Context with |
f6f40114 | 863 | -- its Unit, which points to N_Subprogram_* node. |
cdabbb52 | 864 | |
4871a41d AC |
865 | if Nkind (Context) = N_Compilation_Unit then |
866 | Context := Unit (Context); | |
f6f40114 | 867 | end if; |
226a7fa4 | 868 | else |
4871a41d | 869 | Context := N; |
226a7fa4 AC |
870 | end if; |
871 | ||
4871a41d AC |
872 | while Present (Context) loop |
873 | case Nkind (Context) is | |
d8f43ee6 HK |
874 | when N_Package_Body |
875 | | N_Package_Specification | |
876 | => | |
63b5225b YM |
877 | -- Only return a library-level package |
878 | ||
4871a41d AC |
879 | if Is_Library_Level_Entity (Defining_Entity (Context)) then |
880 | Context := Defining_Entity (Context); | |
63b5225b YM |
881 | exit; |
882 | else | |
4871a41d | 883 | Context := Parent (Context); |
63b5225b | 884 | end if; |
226a7fa4 | 885 | |
226a7fa4 | 886 | when N_Pragma => |
9e92ad49 | 887 | |
15918371 | 888 | -- The enclosing subprogram for a precondition, postcondition, |
ab986406 AC |
889 | -- or contract case should be the declaration preceding the |
890 | -- pragma (skipping any other pragmas between this pragma and | |
891 | -- this declaration. | |
892 | ||
4871a41d AC |
893 | while Nkind (Context) = N_Pragma |
894 | and then Is_List_Member (Context) | |
895 | and then Present (Prev (Context)) | |
ab986406 | 896 | loop |
4871a41d | 897 | Context := Prev (Context); |
ab986406 AC |
898 | end loop; |
899 | ||
4871a41d AC |
900 | if Nkind (Context) = N_Pragma then |
901 | Context := Parent (Context); | |
226a7fa4 AC |
902 | end if; |
903 | ||
d8f43ee6 HK |
904 | when N_Entry_Body |
905 | | N_Entry_Declaration | |
906 | | N_Protected_Type_Declaration | |
907 | | N_Subprogram_Body | |
908 | | N_Subprogram_Declaration | |
909 | | N_Subprogram_Specification | |
910 | | N_Task_Body | |
911 | | N_Task_Type_Declaration | |
912 | => | |
4871a41d | 913 | Context := Defining_Entity (Context); |
eff69022 AC |
914 | exit; |
915 | ||
226a7fa4 | 916 | when others => |
4871a41d | 917 | Context := Parent (Context); |
226a7fa4 AC |
918 | end case; |
919 | end loop; | |
920 | ||
4871a41d AC |
921 | if Nkind (Context) = N_Defining_Program_Unit_Name then |
922 | Context := Defining_Identifier (Context); | |
226a7fa4 AC |
923 | end if; |
924 | ||
5b0113d6 | 925 | -- Do not return a scope without a proper location |
226a7fa4 | 926 | |
4871a41d AC |
927 | if Present (Context) |
928 | and then Sloc (Context) = No_Location | |
226a7fa4 AC |
929 | then |
930 | return Empty; | |
931 | end if; | |
932 | ||
4871a41d | 933 | return Context; |
63b5225b | 934 | end Enclosing_Subprogram_Or_Library_Package; |
226a7fa4 | 935 | |
9466892f AC |
936 | ----------------- |
937 | -- Entity_Hash -- | |
938 | ----------------- | |
939 | ||
940 | function Entity_Hash (E : Entity_Id) return Entity_Hashed_Range is | |
941 | begin | |
9fde638d RD |
942 | return |
943 | Entity_Hashed_Range (E mod (Entity_Id (Entity_Hashed_Range'Last) + 1)); | |
9466892f AC |
944 | end Entity_Hash; |
945 | ||
226a7fa4 AC |
946 | -------------------------- |
947 | -- Generate_Dereference -- | |
948 | -------------------------- | |
949 | ||
950 | procedure Generate_Dereference | |
951 | (N : Node_Id; | |
952 | Typ : Character := 'r') | |
953 | is | |
cdc96e3e AC |
954 | procedure Create_Heap; |
955 | -- Create and decorate the special entity which denotes the heap | |
956 | ||
957 | ----------------- | |
958 | -- Create_Heap -- | |
959 | ----------------- | |
960 | ||
961 | procedure Create_Heap is | |
962 | begin | |
963 | Name_Len := Name_Of_Heap_Variable'Length; | |
964 | Name_Buffer (1 .. Name_Len) := Name_Of_Heap_Variable; | |
965 | ||
966 | Heap := Make_Defining_Identifier (Standard_Location, Name_Enter); | |
967 | ||
968 | Set_Ekind (Heap, E_Variable); | |
969 | Set_Is_Internal (Heap, True); | |
970 | Set_Has_Fully_Qualified_Name (Heap); | |
971 | end Create_Heap; | |
972 | ||
973 | -- Local variables | |
974 | ||
b48a45e3 | 975 | Loc : constant Source_Ptr := Sloc (N); |
226a7fa4 | 976 | |
cdc96e3e AC |
977 | -- Start of processing for Generate_Dereference |
978 | ||
226a7fa4 | 979 | begin |
23e7bf6a | 980 | if Loc > No_Location then |
226a7fa4 | 981 | Drefs.Increment_Last; |
cdc96e3e AC |
982 | |
983 | declare | |
b48a45e3 | 984 | Deref_Entry : Xref_Entry renames Drefs.Table (Drefs.Last); |
cdc96e3e AC |
985 | Deref : Xref_Key renames Deref_Entry.Key; |
986 | ||
987 | begin | |
988 | if No (Heap) then | |
989 | Create_Heap; | |
990 | end if; | |
226a7fa4 | 991 | |
cdc96e3e | 992 | Deref.Ent := Heap; |
23e7bf6a | 993 | Deref.Loc := Loc; |
cdc96e3e | 994 | Deref.Typ := Typ; |
226a7fa4 | 995 | |
a5150cb1 AC |
996 | -- It is as if the special "Heap" was defined in the main unit, |
997 | -- in the scope of the entity for the main unit. This single | |
998 | -- definition point is required to ensure that sorting cross | |
999 | -- references works for "Heap" references as well. | |
226a7fa4 | 1000 | |
a5150cb1 AC |
1001 | Deref.Eun := Main_Unit; |
1002 | Deref.Lun := Get_Top_Level_Code_Unit (Loc); | |
226a7fa4 | 1003 | |
b48a45e3 | 1004 | Deref.Ref_Scope := Enclosing_Subprogram_Or_Library_Package (N); |
a5150cb1 | 1005 | Deref.Ent_Scope := Cunit_Entity (Main_Unit); |
226a7fa4 | 1006 | |
cdc96e3e | 1007 | Deref_Entry.Def := No_Location; |
226a7fa4 | 1008 | |
a5150cb1 | 1009 | Deref_Entry.Ent_Scope_File := Main_Unit; |
cdc96e3e | 1010 | end; |
226a7fa4 AC |
1011 | end if; |
1012 | end Generate_Dereference; | |
1013 | ||
2c1b72d7 AC |
1014 | ------------------------------- |
1015 | -- Traverse_Compilation_Unit -- | |
1016 | ------------------------------- | |
1017 | ||
784ef0fb | 1018 | procedure Traverse_Compilation_Unit (CU : Node_Id) is |
7ffbef99 | 1019 | procedure Traverse_Block (N : Node_Id); |
7ffbef99 | 1020 | procedure Traverse_Declaration_Or_Statement (N : Node_Id); |
80007176 | 1021 | procedure Traverse_Declarations_And_HSS (N : Node_Id); |
7ffbef99 AC |
1022 | procedure Traverse_Declarations_Or_Statements (L : List_Id); |
1023 | procedure Traverse_Handled_Statement_Sequence (N : Node_Id); | |
1024 | procedure Traverse_Package_Body (N : Node_Id); | |
1025 | procedure Traverse_Visible_And_Private_Parts (N : Node_Id); | |
1026 | procedure Traverse_Protected_Body (N : Node_Id); | |
1027 | procedure Traverse_Subprogram_Body (N : Node_Id); | |
1028 | procedure Traverse_Task_Body (N : Node_Id); | |
23e7bf6a | 1029 | |
7ffbef99 | 1030 | -- Traverse corresponding construct, calling Process on all declarations |
2c1b72d7 | 1031 | |
7ffbef99 AC |
1032 | -------------------- |
1033 | -- Traverse_Block -- | |
1034 | -------------------- | |
2c1b72d7 | 1035 | |
7ffbef99 AC |
1036 | procedure Traverse_Block (N : Node_Id) renames |
1037 | Traverse_Declarations_And_HSS; | |
2c1b72d7 | 1038 | |
7ffbef99 AC |
1039 | --------------------------------------- |
1040 | -- Traverse_Declaration_Or_Statement -- | |
1041 | --------------------------------------- | |
56e94186 | 1042 | |
80007176 | 1043 | procedure Traverse_Declaration_Or_Statement (N : Node_Id) is |
42e2600a AC |
1044 | function Traverse_Stub (N : Node_Id) return Boolean; |
1045 | -- Returns True iff stub N should be traversed | |
1046 | ||
1047 | function Traverse_Stub (N : Node_Id) return Boolean is | |
1048 | begin | |
1049 | pragma Assert (Nkind_In (N, N_Package_Body_Stub, | |
1050 | N_Protected_Body_Stub, | |
1051 | N_Subprogram_Body_Stub, | |
1052 | N_Task_Body_Stub)); | |
1053 | ||
784ef0fb | 1054 | return Present (Library_Unit (N)); |
42e2600a AC |
1055 | end Traverse_Stub; |
1056 | ||
1057 | -- Start of processing for Traverse_Declaration_Or_Statement | |
1058 | ||
7ffbef99 AC |
1059 | begin |
1060 | case Nkind (N) is | |
80007176 AC |
1061 | when N_Package_Declaration => |
1062 | Traverse_Visible_And_Private_Parts (Specification (N)); | |
56e94186 | 1063 | |
80007176 | 1064 | when N_Package_Body => |
42e2600a | 1065 | Traverse_Package_Body (N); |
56e94186 | 1066 | |
80007176 | 1067 | when N_Package_Body_Stub => |
42e2600a AC |
1068 | if Traverse_Stub (N) then |
1069 | Traverse_Package_Body (Get_Body_From_Stub (N)); | |
80007176 | 1070 | end if; |
56e94186 | 1071 | |
80007176 | 1072 | when N_Subprogram_Body => |
42e2600a | 1073 | Traverse_Subprogram_Body (N); |
56e94186 | 1074 | |
80007176 AC |
1075 | when N_Entry_Body => |
1076 | Traverse_Subprogram_Body (N); | |
7ffbef99 | 1077 | |
80007176 | 1078 | when N_Subprogram_Body_Stub => |
42e2600a AC |
1079 | if Traverse_Stub (N) then |
1080 | Traverse_Subprogram_Body (Get_Body_From_Stub (N)); | |
80007176 | 1081 | end if; |
60370fb1 | 1082 | |
80007176 AC |
1083 | when N_Protected_Body => |
1084 | Traverse_Protected_Body (N); | |
704228bd | 1085 | |
80007176 | 1086 | when N_Protected_Body_Stub => |
42e2600a | 1087 | if Traverse_Stub (N) then |
7ffbef99 AC |
1088 | Traverse_Protected_Body (Get_Body_From_Stub (N)); |
1089 | end if; | |
704228bd | 1090 | |
42e2600a | 1091 | when N_Protected_Type_Declaration => |
80007176 | 1092 | Traverse_Visible_And_Private_Parts (Protected_Definition (N)); |
363f2c58 | 1093 | |
ed323421 AC |
1094 | when N_Task_Type_Declaration => |
1095 | ||
1096 | -- Task type definition is optional (unlike protected type | |
1097 | -- definition, which is mandatory). | |
1098 | ||
1099 | declare | |
1100 | Task_Def : constant Node_Id := Task_Definition (N); | |
1101 | begin | |
1102 | if Present (Task_Def) then | |
1103 | Traverse_Visible_And_Private_Parts (Task_Def); | |
1104 | end if; | |
1105 | end; | |
704228bd | 1106 | |
80007176 AC |
1107 | when N_Task_Body => |
1108 | Traverse_Task_Body (N); | |
704228bd | 1109 | |
80007176 | 1110 | when N_Task_Body_Stub => |
42e2600a | 1111 | if Traverse_Stub (N) then |
7ffbef99 AC |
1112 | Traverse_Task_Body (Get_Body_From_Stub (N)); |
1113 | end if; | |
704228bd | 1114 | |
80007176 AC |
1115 | when N_Block_Statement => |
1116 | Traverse_Block (N); | |
704228bd | 1117 | |
80007176 | 1118 | when N_If_Statement => |
704228bd | 1119 | |
80007176 | 1120 | -- Traverse the statements in the THEN part |
56e94186 | 1121 | |
80007176 | 1122 | Traverse_Declarations_Or_Statements (Then_Statements (N)); |
56e94186 | 1123 | |
80007176 | 1124 | -- Loop through ELSIF parts if present |
56e94186 | 1125 | |
80007176 AC |
1126 | if Present (Elsif_Parts (N)) then |
1127 | declare | |
1128 | Elif : Node_Id := First (Elsif_Parts (N)); | |
56e94186 | 1129 | |
80007176 AC |
1130 | begin |
1131 | while Present (Elif) loop | |
1132 | Traverse_Declarations_Or_Statements | |
1133 | (Then_Statements (Elif)); | |
1134 | Next (Elif); | |
1135 | end loop; | |
1136 | end; | |
1137 | end if; | |
56e94186 | 1138 | |
80007176 | 1139 | -- Finally traverse the ELSE statements if present |
56e94186 | 1140 | |
80007176 | 1141 | Traverse_Declarations_Or_Statements (Else_Statements (N)); |
56e94186 | 1142 | |
80007176 | 1143 | when N_Case_Statement => |
56e94186 | 1144 | |
80007176 | 1145 | -- Process case branches |
56e94186 | 1146 | |
80007176 | 1147 | declare |
42e2600a | 1148 | Alt : Node_Id := First (Alternatives (N)); |
80007176 | 1149 | begin |
42e2600a | 1150 | loop |
80007176 AC |
1151 | Traverse_Declarations_Or_Statements (Statements (Alt)); |
1152 | Next (Alt); | |
42e2600a | 1153 | exit when No (Alt); |
80007176 AC |
1154 | end loop; |
1155 | end; | |
56e94186 | 1156 | |
80007176 AC |
1157 | when N_Extended_Return_Statement => |
1158 | Traverse_Handled_Statement_Sequence | |
1159 | (Handled_Statement_Sequence (N)); | |
56e94186 | 1160 | |
80007176 AC |
1161 | when N_Loop_Statement => |
1162 | Traverse_Declarations_Or_Statements (Statements (N)); | |
56e94186 | 1163 | |
80007176 | 1164 | -- Generic declarations are ignored |
56e94186 | 1165 | |
80007176 AC |
1166 | when others => |
1167 | null; | |
7ffbef99 AC |
1168 | end case; |
1169 | end Traverse_Declaration_Or_Statement; | |
56e94186 | 1170 | |
7ffbef99 AC |
1171 | ----------------------------------- |
1172 | -- Traverse_Declarations_And_HSS -- | |
1173 | ----------------------------------- | |
56e94186 | 1174 | |
80007176 | 1175 | procedure Traverse_Declarations_And_HSS (N : Node_Id) is |
7ffbef99 AC |
1176 | begin |
1177 | Traverse_Declarations_Or_Statements (Declarations (N)); | |
1178 | Traverse_Handled_Statement_Sequence (Handled_Statement_Sequence (N)); | |
1179 | end Traverse_Declarations_And_HSS; | |
56e94186 | 1180 | |
7ffbef99 AC |
1181 | ----------------------------------------- |
1182 | -- Traverse_Declarations_Or_Statements -- | |
1183 | ----------------------------------------- | |
56e94186 | 1184 | |
80007176 | 1185 | procedure Traverse_Declarations_Or_Statements (L : List_Id) is |
7ffbef99 | 1186 | N : Node_Id; |
56e94186 | 1187 | |
7ffbef99 AC |
1188 | begin |
1189 | -- Loop through statements or declarations | |
1190 | ||
1191 | N := First (L); | |
1192 | while Present (N) loop | |
80007176 | 1193 | |
7ffbef99 AC |
1194 | -- Call Process on all declarations |
1195 | ||
1196 | if Nkind (N) in N_Declaration | |
80007176 AC |
1197 | or else Nkind (N) in N_Later_Decl_Item |
1198 | or else Nkind (N) = N_Entry_Body | |
7ffbef99 | 1199 | then |
5067f3a0 PMR |
1200 | if Nkind (N) in N_Body_Stub then |
1201 | Process (Get_Body_From_Stub (N)); | |
1202 | else | |
1203 | Process (N); | |
1204 | end if; | |
7ffbef99 AC |
1205 | end if; |
1206 | ||
1207 | Traverse_Declaration_Or_Statement (N); | |
1208 | ||
1209 | Next (N); | |
1210 | end loop; | |
1211 | end Traverse_Declarations_Or_Statements; | |
1212 | ||
1213 | ----------------------------------------- | |
1214 | -- Traverse_Handled_Statement_Sequence -- | |
1215 | ----------------------------------------- | |
1216 | ||
80007176 | 1217 | procedure Traverse_Handled_Statement_Sequence (N : Node_Id) is |
7ffbef99 AC |
1218 | Handler : Node_Id; |
1219 | ||
1220 | begin | |
1221 | if Present (N) then | |
1222 | Traverse_Declarations_Or_Statements (Statements (N)); | |
1223 | ||
1224 | if Present (Exception_Handlers (N)) then | |
1225 | Handler := First (Exception_Handlers (N)); | |
1226 | while Present (Handler) loop | |
1227 | Traverse_Declarations_Or_Statements (Statements (Handler)); | |
1228 | Next (Handler); | |
1229 | end loop; | |
1230 | end if; | |
ca7e6c26 | 1231 | end if; |
7ffbef99 | 1232 | end Traverse_Handled_Statement_Sequence; |
ce5c2061 | 1233 | |
7ffbef99 AC |
1234 | --------------------------- |
1235 | -- Traverse_Package_Body -- | |
1236 | --------------------------- | |
56e94186 | 1237 | |
42e2600a AC |
1238 | procedure Traverse_Package_Body (N : Node_Id) is |
1239 | Spec_E : constant Entity_Id := Unique_Defining_Entity (N); | |
c63a2ad6 | 1240 | |
42e2600a AC |
1241 | begin |
1242 | case Ekind (Spec_E) is | |
1243 | when E_Package => | |
1244 | Traverse_Declarations_And_HSS (N); | |
c63a2ad6 | 1245 | |
42e2600a AC |
1246 | when E_Generic_Package => |
1247 | null; | |
c63a2ad6 | 1248 | |
42e2600a AC |
1249 | when others => |
1250 | raise Program_Error; | |
1251 | end case; | |
1252 | end Traverse_Package_Body; | |
56e94186 | 1253 | |
7ffbef99 AC |
1254 | ----------------------------- |
1255 | -- Traverse_Protected_Body -- | |
1256 | ----------------------------- | |
56e94186 | 1257 | |
7ffbef99 AC |
1258 | procedure Traverse_Protected_Body (N : Node_Id) is |
1259 | begin | |
1260 | Traverse_Declarations_Or_Statements (Declarations (N)); | |
1261 | end Traverse_Protected_Body; | |
1262 | ||
1263 | ------------------------------ | |
1264 | -- Traverse_Subprogram_Body -- | |
1265 | ------------------------------ | |
1266 | ||
42e2600a AC |
1267 | procedure Traverse_Subprogram_Body (N : Node_Id) is |
1268 | Spec_E : constant Entity_Id := Unique_Defining_Entity (N); | |
c63a2ad6 | 1269 | |
42e2600a AC |
1270 | begin |
1271 | case Ekind (Spec_E) is | |
c63a2ad6 AC |
1272 | when Entry_Kind |
1273 | | E_Function | |
1274 | | E_Procedure | |
1275 | => | |
42e2600a | 1276 | Traverse_Declarations_And_HSS (N); |
c63a2ad6 | 1277 | |
42e2600a AC |
1278 | when Generic_Subprogram_Kind => |
1279 | null; | |
c63a2ad6 | 1280 | |
42e2600a AC |
1281 | when others => |
1282 | raise Program_Error; | |
1283 | end case; | |
1284 | end Traverse_Subprogram_Body; | |
7ffbef99 AC |
1285 | |
1286 | ------------------------ | |
1287 | -- Traverse_Task_Body -- | |
1288 | ------------------------ | |
1289 | ||
1290 | procedure Traverse_Task_Body (N : Node_Id) renames | |
1291 | Traverse_Declarations_And_HSS; | |
1292 | ||
80007176 AC |
1293 | ---------------------------------------- |
1294 | -- Traverse_Visible_And_Private_Parts -- | |
1295 | ---------------------------------------- | |
1296 | ||
7ffbef99 AC |
1297 | procedure Traverse_Visible_And_Private_Parts (N : Node_Id) is |
1298 | begin | |
1299 | Traverse_Declarations_Or_Statements (Visible_Declarations (N)); | |
1300 | Traverse_Declarations_Or_Statements (Private_Declarations (N)); | |
1301 | end Traverse_Visible_And_Private_Parts; | |
1302 | ||
80007176 AC |
1303 | -- Local variables |
1304 | ||
1305 | Lu : Node_Id; | |
1306 | ||
7ffbef99 | 1307 | -- Start of processing for Traverse_Compilation_Unit |
56e94186 AC |
1308 | |
1309 | begin | |
7ffbef99 AC |
1310 | -- Get Unit (checking case of subunit) |
1311 | ||
1312 | Lu := Unit (CU); | |
1313 | ||
1314 | if Nkind (Lu) = N_Subunit then | |
1315 | Lu := Proper_Body (Lu); | |
56e94186 | 1316 | end if; |
56e94186 | 1317 | |
7ffbef99 | 1318 | -- Do not add scopes for generic units |
56e94186 | 1319 | |
7ffbef99 AC |
1320 | if Nkind (Lu) = N_Package_Body |
1321 | and then Ekind (Corresponding_Spec (Lu)) in Generic_Unit_Kind | |
1322 | then | |
1323 | return; | |
1324 | end if; | |
265ca04a | 1325 | |
7ffbef99 | 1326 | -- Call Process on all declarations |
56e94186 | 1327 | |
7ffbef99 AC |
1328 | if Nkind (Lu) in N_Declaration |
1329 | or else Nkind (Lu) in N_Later_Decl_Item | |
1330 | then | |
1331 | Process (Lu); | |
1332 | end if; | |
1333 | ||
1334 | -- Traverse the unit | |
1335 | ||
1336 | Traverse_Declaration_Or_Statement (Lu); | |
1337 | end Traverse_Compilation_Unit; | |
56e94186 | 1338 | |
06b599fd | 1339 | end SPARK_Specific; |