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