1 ------------------------------------------------------------------------------
3 -- GNAT COMPILER COMPONENTS --
5 -- L I B . X R E F . S P A R K _ S P E C I F I C --
9 -- Copyright (C) 2011-2017, Free Software Foundation, Inc. --
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. --
21 -- GNAT was originally developed by the GNAT team at New York University. --
22 -- Extensive contributions were provided by Ada Core Technologies Inc. --
24 ------------------------------------------------------------------------------
26 with Einfo; use Einfo;
27 with Nmake; use Nmake;
28 with SPARK_Xrefs; use SPARK_Xrefs;
33 package body SPARK_Specific is
39 -- Table of SPARK_Entities, True for each entity kind used in SPARK
41 SPARK_Entities : constant array (Entity_Kind) of Boolean :=
45 E_In_Out_Parameter => True,
46 E_In_Parameter => True,
47 E_Loop_Parameter => True,
49 E_Out_Parameter => True,
54 -- True for each reference type used in SPARK
56 SPARK_References : constant array (Character) of Boolean :=
62 type Entity_Hashed_Range is range 0 .. 255;
63 -- Size of hash table headers
69 package Drefs is new Table.Table (
70 Table_Component_Type => Xref_Entry,
71 Table_Index_Type => Xref_Entry_Number,
73 Table_Initial => Alloc.Drefs_Initial,
74 Table_Increment => Alloc.Drefs_Increment,
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
78 -- "Heap". These references are added to the regular references when
79 -- computing SPARK cross-references.
81 -----------------------
82 -- Local Subprograms --
83 -----------------------
85 procedure Add_SPARK_File (Uspec, Ubody : Unit_Number_Type; Dspec : Nat);
86 -- Add file and corresponding scopes for unit to the tables
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.
92 procedure Add_SPARK_Xrefs;
93 -- Filter table Xrefs to add all references used in SPARK to the table
96 function Entity_Hash (E : Entity_Id) return Entity_Hashed_Range;
97 -- Hash function for hash table
103 procedure Add_SPARK_File (Uspec, Ubody : Unit_Number_Type; Dspec : Nat) is
104 File : constant Source_File_Index := Source_Index (Uspec);
105 From : constant Scope_Index := SPARK_Scope_Table.Last + 1;
109 procedure Add_SPARK_Scope (N : Node_Id);
110 -- Add scope N to the table SPARK_Scope_Table
112 procedure Detect_And_Add_SPARK_Scope (N : Node_Id);
113 -- Call Add_SPARK_Scope on scopes
115 ---------------------
116 -- Add_SPARK_Scope --
117 ---------------------
119 procedure Add_SPARK_Scope (N : Node_Id) is
120 E : constant Entity_Id := Defining_Entity (N);
123 -- Ignore scopes without a proper location
125 if Sloc (N) = No_Location then
135 | E_Generic_Procedure
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.
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
163 SPARK_Scope_Table.Append
166 Scope_Num => Scope_Id,
172 Scope_Id := Scope_Id + 1;
175 --------------------------------
176 -- Detect_And_Add_SPARK_Scope --
177 --------------------------------
179 procedure Detect_And_Add_SPARK_Scope (N : Node_Id) is
183 if Nkind_In (N, N_Entry_Body, N_Entry_Declaration)
187 or else Nkind_In (N, N_Package_Body,
188 N_Package_Declaration)
191 or else Nkind_In (N, N_Protected_Body,
192 N_Protected_Type_Declaration)
196 or else Nkind_In (N, N_Subprogram_Body,
197 N_Subprogram_Declaration)
201 or else Nkind_In (N, N_Task_Body,
202 N_Task_Type_Declaration)
206 end Detect_And_Add_SPARK_Scope;
208 procedure Traverse_Scopes is new
209 Traverse_Compilation_Unit (Detect_And_Add_SPARK_Scope);
211 -- Start of processing for Add_SPARK_File
214 -- Source file could be inexistant as a result of an error, if option
217 if File <= No_Source_File then
221 -- Subunits are traversed as part of the top-level unit to which they
224 if Nkind (Unit (Cunit (Uspec))) = N_Subunit then
228 Traverse_Scopes (CU => Cunit (Uspec));
230 -- When two units are present for the same compilation unit, as it
231 -- happens for library-level instantiations of generics, then add all
232 -- scopes to the same SPARK file.
234 if Ubody /= No_Unit then
235 Traverse_Scopes (CU => Cunit (Ubody));
238 SPARK_File_Table.Append (
241 To_Scope => SPARK_Scope_Table.Last));
244 ---------------------
245 -- Add_SPARK_Xrefs --
246 ---------------------
248 procedure Add_SPARK_Xrefs is
249 function Entity_Of_Scope (S : Scope_Index) return Entity_Id;
250 -- Return the entity which maps to the input scope index
252 function Get_Scope_Num (E : Entity_Id) return Nat;
253 -- Return the scope number associated with the entity E
255 function Is_Constant_Object_Without_Variable_Input
256 (E : Entity_Id) return Boolean;
257 -- Return True if E is known to have no variable input, as defined in
260 function Is_Future_Scope_Entity
262 S : Scope_Index) return Boolean;
263 -- Check whether entity E is in SPARK_Scope_Table at index S or higher
265 function Is_SPARK_Reference
267 Typ : Character) return Boolean;
268 -- Return whether entity reference E meets SPARK requirements. Typ is
269 -- the reference type.
271 function Is_SPARK_Scope (E : Entity_Id) return Boolean;
272 -- Return whether the entity or reference scope meets requirements for
273 -- being a SPARK scope.
275 function Lt (Op1 : Natural; Op2 : Natural) return Boolean;
276 -- Comparison function for Sort call
278 procedure Move (From : Natural; To : Natural);
279 -- Move procedure for Sort call
281 procedure Set_Scope_Num (E : Entity_Id; Num : Nat);
282 -- Associate entity E with the scope number Num
284 procedure Update_Scope_Range
288 -- Update the scope which maps to S with the new range From .. To
290 package Sorting is new GNAT.Heap_Sort_G (Move, Lt);
292 No_Scope : constant Nat := 0;
293 -- Initial scope counter
295 package Scopes is new GNAT.HTable.Simple_HTable
296 (Header_Num => Entity_Hashed_Range,
298 No_Element => No_Scope,
302 -- Package used to build a correspondence between entities and scope
303 -- numbers used in SPARK cross references.
305 Nrefs : Nat := Xrefs.Last;
306 -- Number of references in table. This value may get reset (reduced)
307 -- when we eliminate duplicate reference entries as well as references
308 -- not suitable for local cross-references.
310 Nrefs_Add : constant Nat := Drefs.Last;
311 -- Number of additional references which correspond to dereferences in
314 Rnums : array (0 .. Nrefs + Nrefs_Add) of Nat;
315 -- This array contains numbers of references in the Xrefs table. This
316 -- list is sorted in output order. The extra 0'th entry is convenient
317 -- for the call to sort. When we sort the table, we move the indices in
318 -- Rnums around, but we do not move the original table entries.
320 ---------------------
321 -- Entity_Of_Scope --
322 ---------------------
324 function Entity_Of_Scope (S : Scope_Index) return Entity_Id is
326 return SPARK_Scope_Table.Table (S).Entity;
333 function Get_Scope_Num (E : Entity_Id) return Nat renames Scopes.Get;
335 -----------------------------------------------
336 -- Is_Constant_Object_Without_Variable_Input --
337 -----------------------------------------------
339 function Is_Constant_Object_Without_Variable_Input
340 (E : Entity_Id) return Boolean
345 -- A constant is known to have no variable input if its
346 -- initializing expression is static (a value which is
347 -- compile-time-known is not guaranteed to have no variable input
348 -- as defined in the SPARK RM). Otherwise, the constant may or not
349 -- have variable input.
355 if Present (Full_View (E)) then
356 Decl := Parent (Full_View (E));
361 if Is_Imported (E) then
364 pragma Assert (Present (Expression (Decl)));
365 return Is_Static_Expression (Expression (Decl));
377 end Is_Constant_Object_Without_Variable_Input;
379 ----------------------------
380 -- Is_Future_Scope_Entity --
381 ----------------------------
383 function Is_Future_Scope_Entity
385 S : Scope_Index) return Boolean
387 function Is_Past_Scope_Entity return Boolean;
388 -- Check whether entity E is in SPARK_Scope_Table at index strictly
391 --------------------------
392 -- Is_Past_Scope_Entity --
393 --------------------------
395 function Is_Past_Scope_Entity return Boolean is
397 for Index in SPARK_Scope_Table.First .. S - 1 loop
398 if SPARK_Scope_Table.Table (Index).Entity = E then
404 end Is_Past_Scope_Entity;
406 -- Start of processing for Is_Future_Scope_Entity
409 for Index in S .. SPARK_Scope_Table.Last loop
410 if SPARK_Scope_Table.Table (Index).Entity = E then
415 -- If this assertion fails, this means that the scope which we are
416 -- looking for has been treated already, which reveals a problem in
417 -- the order of cross-references.
419 pragma Assert (not Is_Past_Scope_Entity);
422 end Is_Future_Scope_Entity;
424 ------------------------
425 -- Is_SPARK_Reference --
426 ------------------------
428 function Is_SPARK_Reference
430 Typ : Character) return Boolean
433 -- The only references of interest on callable entities are calls. On
434 -- uncallable entities, the only references of interest are reads and
437 if Ekind (E) in Overloadable_Kind then
440 -- In all other cases, result is true for reference/modify cases,
441 -- and false for all other cases.
444 return Typ = 'r' or else Typ = 'm';
446 end Is_SPARK_Reference;
452 function Is_SPARK_Scope (E : Entity_Id) return Boolean is
453 Can_Be_Renamed : constant Boolean :=
455 and then (Is_Subprogram_Or_Entry (E)
456 or else Ekind (E) = E_Package);
459 and then not Is_Generic_Unit (E)
460 and then (not Can_Be_Renamed or else No (Renamed_Entity (E)))
461 and then Get_Scope_Num (E) /= No_Scope;
468 function Lt (Op1 : Natural; Op2 : Natural) return Boolean is
469 T1 : constant Xref_Entry := Xrefs.Table (Rnums (Nat (Op1)));
470 T2 : constant Xref_Entry := Xrefs.Table (Rnums (Nat (Op2)));
473 -- First test: if entity is in different unit, sort by unit. Note:
474 -- that we use Ent_Scope_File rather than Eun, as Eun may refer to
475 -- the file where the generic scope is defined, which may differ from
476 -- the file where the enclosing scope is defined. It is the latter
477 -- which matters for a correct order here.
479 if T1.Ent_Scope_File /= T2.Ent_Scope_File then
480 return Dependency_Num (T1.Ent_Scope_File) <
481 Dependency_Num (T2.Ent_Scope_File);
483 -- Second test: within same unit, sort by location of the scope of
484 -- the entity definition.
486 elsif Get_Scope_Num (T1.Key.Ent_Scope) /=
487 Get_Scope_Num (T2.Key.Ent_Scope)
489 return Get_Scope_Num (T1.Key.Ent_Scope) <
490 Get_Scope_Num (T2.Key.Ent_Scope);
492 -- Third test: within same unit and scope, sort by location of
493 -- entity definition.
495 elsif T1.Def /= T2.Def then
496 return T1.Def < T2.Def;
499 -- Both entities must be equal at this point
501 pragma Assert (T1.Key.Ent = T2.Key.Ent);
502 pragma Assert (T1.Key.Ent_Scope = T2.Key.Ent_Scope);
503 pragma Assert (T1.Ent_Scope_File = T2.Ent_Scope_File);
505 -- Fourth test: if reference is in same unit as entity definition,
508 if T1.Key.Lun /= T2.Key.Lun
509 and then T1.Ent_Scope_File = T1.Key.Lun
513 elsif T1.Key.Lun /= T2.Key.Lun
514 and then T2.Ent_Scope_File = T2.Key.Lun
518 -- Fifth test: if reference is in same unit and same scope as
519 -- entity definition, sort first.
521 elsif T1.Ent_Scope_File = T1.Key.Lun
522 and then T1.Key.Ref_Scope /= T2.Key.Ref_Scope
523 and then T1.Key.Ent_Scope = T1.Key.Ref_Scope
527 elsif T2.Ent_Scope_File = T2.Key.Lun
528 and then T1.Key.Ref_Scope /= T2.Key.Ref_Scope
529 and then T2.Key.Ent_Scope = T2.Key.Ref_Scope
533 -- Sixth test: for same entity, sort by reference location unit
535 elsif T1.Key.Lun /= T2.Key.Lun then
536 return Dependency_Num (T1.Key.Lun) <
537 Dependency_Num (T2.Key.Lun);
539 -- Seventh test: for same entity, sort by reference location scope
541 elsif Get_Scope_Num (T1.Key.Ref_Scope) /=
542 Get_Scope_Num (T2.Key.Ref_Scope)
544 return Get_Scope_Num (T1.Key.Ref_Scope) <
545 Get_Scope_Num (T2.Key.Ref_Scope);
547 -- Eighth test: order of location within referencing unit
549 elsif T1.Key.Loc /= T2.Key.Loc then
550 return T1.Key.Loc < T2.Key.Loc;
552 -- Finally, for two locations at the same address prefer the one
553 -- that does NOT have the type 'r', so that a modification or
554 -- extension takes preference, when there are more than one
555 -- reference at the same location. As a result, in the case of
556 -- entities that are in-out actuals, the read reference follows
557 -- the modify reference.
560 return T2.Key.Typ = 'r';
569 procedure Move (From : Natural; To : Natural) is
571 Rnums (Nat (To)) := Rnums (Nat (From));
578 procedure Set_Scope_Num (E : Entity_Id; Num : Nat) renames Scopes.Set;
580 ------------------------
581 -- Update_Scope_Range --
582 ------------------------
584 procedure Update_Scope_Range
590 SPARK_Scope_Table.Table (S).From_Xref := From;
591 SPARK_Scope_Table.Table (S).To_Xref := To;
592 end Update_Scope_Range;
596 From_Index : Xref_Index;
597 Prev_Loc : Source_Ptr;
598 Prev_Typ : Character;
600 Scope_Id : Scope_Index;
602 -- Start of processing for Add_SPARK_Xrefs
605 for Index in SPARK_Scope_Table.First .. SPARK_Scope_Table.Last loop
607 S : SPARK_Scope_Record renames SPARK_Scope_Table.Table (Index);
609 Set_Scope_Num (S.Entity, S.Scope_Num);
614 Drefs_Table : Drefs.Table_Type
615 renames Drefs.Table (Drefs.First .. Drefs.Last);
617 Xrefs.Append_All (Xrefs.Table_Type (Drefs_Table));
618 Nrefs := Nrefs + Drefs_Table'Length;
621 -- Capture the definition Sloc values. As in the case of normal cross
622 -- references, we have to wait until now to get the correct value.
624 for Index in 1 .. Nrefs loop
625 Xrefs.Table (Index).Def := Sloc (Xrefs.Table (Index).Key.Ent);
628 -- Eliminate entries not appropriate for SPARK. Done prior to sorting
629 -- cross-references, as it discards useless references which do not have
630 -- a proper format for the comparison function (like no location).
635 for Index in 1 .. Ref_Count loop
637 Ref : Xref_Key renames Xrefs.Table (Index).Key;
640 if SPARK_Entities (Ekind (Ref.Ent))
641 and then SPARK_References (Ref.Typ)
642 and then Is_SPARK_Scope (Ref.Ent_Scope)
643 and then Is_SPARK_Scope (Ref.Ref_Scope)
644 and then Is_SPARK_Reference (Ref.Ent, Ref.Typ)
646 -- Discard references from unknown scopes, e.g. generic scopes
648 and then Get_Scope_Num (Ref.Ent_Scope) /= No_Scope
649 and then Get_Scope_Num (Ref.Ref_Scope) /= No_Scope
651 -- Discard references to loop parameters introduced within
652 -- expression functions, as they give two references: one from
653 -- the analysis of the expression function itself and one from
654 -- the analysis of the expanded body. We don't lose any globals
655 -- by discarding them, because such loop parameters can only be
656 -- accessed locally from within the expression function body.
659 (Ekind (Ref.Ent) = E_Loop_Parameter
660 and then Scope_Within
661 (Ref.Ent, Unique_Entity (Ref.Ref_Scope))
662 and then Is_Expression_Function (Ref.Ref_Scope))
665 Rnums (Nrefs) := Index;
670 -- Sort the references
672 Sorting.Sort (Integer (Nrefs));
674 -- Eliminate duplicate entries
676 -- We need this test for Ref_Count because if we force ALI file
677 -- generation in case of errors detected, it may be the case that
678 -- Nrefs is 0, so we should not reset it here.
684 for Index in 2 .. Ref_Count loop
685 if Xrefs.Table (Rnums (Index)) /= Xrefs.Table (Rnums (Nrefs)) then
687 Rnums (Nrefs) := Rnums (Index);
692 -- Eliminate the reference if it is at the same location as the previous
693 -- one, unless it is a read-reference indicating that the entity is an
694 -- in-out actual in a call.
698 Prev_Loc := No_Location;
701 for Index in 1 .. Ref_Count loop
703 Ref : Xref_Key renames Xrefs.Table (Rnums (Index)).Key;
706 if Ref.Loc /= Prev_Loc
707 or else (Prev_Typ = 'm' and then Ref.Typ = 'r')
712 Rnums (Nrefs) := Rnums (Index);
717 -- The two steps have eliminated all references, nothing to do
719 if SPARK_Scope_Table.Last = 0 then
726 -- Loop to output references
728 for Refno in 1 .. Nrefs loop
730 Ref_Entry : Xref_Entry renames Xrefs.Table (Rnums (Refno));
731 Ref : Xref_Key renames Ref_Entry.Key;
735 -- If this assertion fails, the scope which we are looking for is
736 -- not in SPARK scope table, which reveals either a problem in the
737 -- construction of the scope table, or an erroneous scope for the
738 -- current cross-reference.
740 pragma Assert (Is_Future_Scope_Entity (Ref.Ent_Scope, Scope_Id));
742 -- Update the range of cross references to which the current scope
743 -- refers to. This may be the empty range only for the first scope
746 if Ref.Ent_Scope /= Entity_Of_Scope (Scope_Id) then
750 To => SPARK_Xref_Table.Last);
752 From_Index := SPARK_Xref_Table.Last + 1;
755 while Ref.Ent_Scope /= Entity_Of_Scope (Scope_Id) loop
756 Scope_Id := Scope_Id + 1;
757 pragma Assert (Scope_Id <= SPARK_Scope_Table.Last);
760 -- References to constant objects without variable inputs (see
761 -- SPARK RM 3.3.1) are considered specially in SPARK section,
762 -- because these will be translated as constants in the
763 -- intermediate language for formal verification, and should
764 -- therefore never appear in frame conditions. Other constants may
765 -- later be treated the same, up to GNATprove to decide based on
766 -- its flow analysis.
768 if Is_Constant_Object_Without_Variable_Input (Ref.Ent) then
774 SPARK_Xref_Table.Append (
775 (Entity => Unique_Entity (Ref.Ent),
776 Ref_Scope => Ref.Ref_Scope,
781 -- Update the range of cross references to which the scope refers to
786 To => SPARK_Xref_Table.Last);
789 -------------------------
790 -- Collect_SPARK_Xrefs --
791 -------------------------
793 procedure Collect_SPARK_Xrefs
794 (Sdep_Table : Unit_Ref_Table;
799 -- Index of the current and next source dependency
802 -- Index of the file to which the scopes need to be assigned; for
803 -- library-level instances of generic units this points to the unit
804 -- of the body, because this is where references are assigned to.
806 Ubody : Unit_Number_Type;
807 Uspec : Unit_Number_Type;
808 -- Unit numbers for the dependency spec and possibly its body (only in
809 -- the case of library-level instance of a generic package).
812 -- Cross-references should have been computed first
814 pragma Assert (Xrefs.Last /= 0);
816 Initialize_SPARK_Tables;
818 -- Generate file and scope SPARK cross-reference information
821 while Sdep <= Num_Sdep loop
823 -- Skip dependencies with no entity node, e.g. configuration files
824 -- with pragmas (.adc) or target description (.atp), since they
825 -- present no interest for SPARK cross references.
827 if No (Cunit_Entity (Sdep_Table (Sdep))) then
828 Sdep_Next := Sdep + 1;
830 -- For library-level instantiation of a generic, two consecutive
831 -- units refer to the same compilation unit node and entity (one to
832 -- body, one to spec). In that case, treat them as a single unit for
833 -- the sake of SPARK cross references by passing to Add_SPARK_File.
837 and then Cunit_Entity (Sdep_Table (Sdep)) =
838 Cunit_Entity (Sdep_Table (Sdep + 1))
841 Cunit1 : Node_Id renames Cunit (Sdep_Table (Sdep));
842 Cunit2 : Node_Id renames Cunit (Sdep_Table (Sdep + 1));
845 -- Both Cunits point to compilation unit nodes
848 (Nkind (Cunit1) = N_Compilation_Unit
849 and then Nkind (Cunit2) = N_Compilation_Unit);
851 -- Do not depend on the sorting order, which is based on
852 -- Unit_Name, and for library-level instances of nested
853 -- generic packages they are equal.
855 -- If declaration comes before the body
857 if Nkind (Unit (Cunit1)) = N_Package_Declaration
858 and then Nkind (Unit (Cunit2)) = N_Package_Body
860 Uspec := Sdep_Table (Sdep);
861 Ubody := Sdep_Table (Sdep + 1);
863 Sdep_File := Sdep + 1;
865 -- If body comes before declaration
867 elsif Nkind (Unit (Cunit1)) = N_Package_Body
868 and then Nkind (Unit (Cunit2)) = N_Package_Declaration
870 Uspec := Sdep_Table (Sdep + 1);
871 Ubody := Sdep_Table (Sdep);
875 -- Otherwise it is an error
881 Sdep_Next := Sdep + 2;
887 Uspec := Sdep_Table (Sdep);
891 Sdep_Next := Sdep + 1;
903 -- Fill in the spec information when relevant
906 package Entity_Hash_Table is new
907 GNAT.HTable.Simple_HTable
908 (Header_Num => Entity_Hashed_Range,
909 Element => Scope_Index,
916 -- Fill in the hash-table
918 for S in SPARK_Scope_Table.First .. SPARK_Scope_Table.Last loop
920 Srec : SPARK_Scope_Record renames SPARK_Scope_Table.Table (S);
922 Entity_Hash_Table.Set (Srec.Entity, S);
926 -- Use the hash-table to locate spec entities
928 for S in SPARK_Scope_Table.First .. SPARK_Scope_Table.Last loop
930 Srec : SPARK_Scope_Record renames SPARK_Scope_Table.Table (S);
932 Spec_Entity : constant Entity_Id :=
933 Unique_Entity (Srec.Entity);
934 Spec_Scope : constant Scope_Index :=
935 Entity_Hash_Table.Get (Spec_Entity);
938 -- Generic spec may be missing in which case Spec_Scope is zero
940 if Spec_Entity /= Srec.Entity
941 and then Spec_Scope /= 0
943 Srec.Spec_File_Num :=
944 SPARK_Scope_Table.Table (Spec_Scope).File_Num;
945 Srec.Spec_Scope_Num :=
946 SPARK_Scope_Table.Table (Spec_Scope).Scope_Num;
952 -- Generate SPARK cross-reference information
955 end Collect_SPARK_Xrefs;
957 -------------------------------------
958 -- Enclosing_Subprogram_Or_Package --
959 -------------------------------------
961 function Enclosing_Subprogram_Or_Library_Package
962 (N : Node_Id) return Entity_Id
967 -- If N is the defining identifier for a subprogram, then return the
968 -- enclosing subprogram or package, not this subprogram.
970 if Nkind_In (N, N_Defining_Identifier, N_Defining_Operator_Symbol)
971 and then (Ekind (N) in Entry_Kind
972 or else Ekind (N) = E_Subprogram_Body
973 or else Ekind (N) in Generic_Subprogram_Kind
974 or else Ekind (N) in Subprogram_Kind)
976 Context := Parent (Unit_Declaration_Node (N));
978 -- If this was a library-level subprogram then replace Context with
979 -- its Unit, which points to N_Subprogram_* node.
981 if Nkind (Context) = N_Compilation_Unit then
982 Context := Unit (Context);
988 while Present (Context) loop
989 case Nkind (Context) is
991 | N_Package_Specification
993 -- Only return a library-level package
995 if Is_Library_Level_Entity (Defining_Entity (Context)) then
996 Context := Defining_Entity (Context);
999 Context := Parent (Context);
1004 -- The enclosing subprogram for a precondition, postcondition,
1005 -- or contract case should be the declaration preceding the
1006 -- pragma (skipping any other pragmas between this pragma and
1007 -- this declaration.
1009 while Nkind (Context) = N_Pragma
1010 and then Is_List_Member (Context)
1011 and then Present (Prev (Context))
1013 Context := Prev (Context);
1016 if Nkind (Context) = N_Pragma then
1017 Context := Parent (Context);
1021 | N_Entry_Declaration
1022 | N_Protected_Type_Declaration
1024 | N_Subprogram_Declaration
1025 | N_Subprogram_Specification
1027 | N_Task_Type_Declaration
1029 Context := Defining_Entity (Context);
1033 Context := Parent (Context);
1037 if Nkind (Context) = N_Defining_Program_Unit_Name then
1038 Context := Defining_Identifier (Context);
1041 -- Do not return a scope without a proper location
1043 if Present (Context)
1044 and then Sloc (Context) = No_Location
1050 end Enclosing_Subprogram_Or_Library_Package;
1056 function Entity_Hash (E : Entity_Id) return Entity_Hashed_Range is
1059 Entity_Hashed_Range (E mod (Entity_Id (Entity_Hashed_Range'Last) + 1));
1062 --------------------------
1063 -- Generate_Dereference --
1064 --------------------------
1066 procedure Generate_Dereference
1068 Typ : Character := 'r')
1070 procedure Create_Heap;
1071 -- Create and decorate the special entity which denotes the heap
1077 procedure Create_Heap is
1079 Name_Len := Name_Of_Heap_Variable'Length;
1080 Name_Buffer (1 .. Name_Len) := Name_Of_Heap_Variable;
1082 Heap := Make_Defining_Identifier (Standard_Location, Name_Enter);
1084 Set_Ekind (Heap, E_Variable);
1085 Set_Is_Internal (Heap, True);
1086 Set_Has_Fully_Qualified_Name (Heap);
1091 Loc : constant Source_Ptr := Sloc (N);
1093 -- Start of processing for Generate_Dereference
1096 if Loc > No_Location then
1097 Drefs.Increment_Last;
1100 Deref_Entry : Xref_Entry renames Drefs.Table (Drefs.Last);
1101 Deref : Xref_Key renames Deref_Entry.Key;
1112 -- It is as if the special "Heap" was defined in the main unit,
1113 -- in the scope of the entity for the main unit. This single
1114 -- definition point is required to ensure that sorting cross
1115 -- references works for "Heap" references as well.
1117 Deref.Eun := Main_Unit;
1118 Deref.Lun := Get_Top_Level_Code_Unit (Loc);
1120 Deref.Ref_Scope := Enclosing_Subprogram_Or_Library_Package (N);
1121 Deref.Ent_Scope := Cunit_Entity (Main_Unit);
1123 Deref_Entry.Def := No_Location;
1125 Deref_Entry.Ent_Scope_File := Main_Unit;
1128 end Generate_Dereference;
1130 -------------------------------
1131 -- Traverse_Compilation_Unit --
1132 -------------------------------
1134 procedure Traverse_Compilation_Unit (CU : Node_Id) is
1135 procedure Traverse_Block (N : Node_Id);
1136 procedure Traverse_Declaration_Or_Statement (N : Node_Id);
1137 procedure Traverse_Declarations_And_HSS (N : Node_Id);
1138 procedure Traverse_Declarations_Or_Statements (L : List_Id);
1139 procedure Traverse_Handled_Statement_Sequence (N : Node_Id);
1140 procedure Traverse_Package_Body (N : Node_Id);
1141 procedure Traverse_Visible_And_Private_Parts (N : Node_Id);
1142 procedure Traverse_Protected_Body (N : Node_Id);
1143 procedure Traverse_Subprogram_Body (N : Node_Id);
1144 procedure Traverse_Task_Body (N : Node_Id);
1146 -- Traverse corresponding construct, calling Process on all declarations
1148 --------------------
1149 -- Traverse_Block --
1150 --------------------
1152 procedure Traverse_Block (N : Node_Id) renames
1153 Traverse_Declarations_And_HSS;
1155 ---------------------------------------
1156 -- Traverse_Declaration_Or_Statement --
1157 ---------------------------------------
1159 procedure Traverse_Declaration_Or_Statement (N : Node_Id) is
1160 function Traverse_Stub (N : Node_Id) return Boolean;
1161 -- Returns True iff stub N should be traversed
1163 function Traverse_Stub (N : Node_Id) return Boolean is
1165 pragma Assert (Nkind_In (N, N_Package_Body_Stub,
1166 N_Protected_Body_Stub,
1167 N_Subprogram_Body_Stub,
1170 return Present (Library_Unit (N));
1173 -- Start of processing for Traverse_Declaration_Or_Statement
1177 when N_Package_Declaration =>
1178 Traverse_Visible_And_Private_Parts (Specification (N));
1180 when N_Package_Body =>
1181 Traverse_Package_Body (N);
1183 when N_Package_Body_Stub =>
1184 if Traverse_Stub (N) then
1185 Traverse_Package_Body (Get_Body_From_Stub (N));
1188 when N_Subprogram_Body =>
1189 Traverse_Subprogram_Body (N);
1191 when N_Entry_Body =>
1192 Traverse_Subprogram_Body (N);
1194 when N_Subprogram_Body_Stub =>
1195 if Traverse_Stub (N) then
1196 Traverse_Subprogram_Body (Get_Body_From_Stub (N));
1199 when N_Protected_Body =>
1200 Traverse_Protected_Body (N);
1202 when N_Protected_Body_Stub =>
1203 if Traverse_Stub (N) then
1204 Traverse_Protected_Body (Get_Body_From_Stub (N));
1207 when N_Protected_Type_Declaration =>
1208 Traverse_Visible_And_Private_Parts (Protected_Definition (N));
1210 when N_Task_Type_Declaration =>
1212 -- Task type definition is optional (unlike protected type
1213 -- definition, which is mandatory).
1216 Task_Def : constant Node_Id := Task_Definition (N);
1218 if Present (Task_Def) then
1219 Traverse_Visible_And_Private_Parts (Task_Def);
1224 Traverse_Task_Body (N);
1226 when N_Task_Body_Stub =>
1227 if Traverse_Stub (N) then
1228 Traverse_Task_Body (Get_Body_From_Stub (N));
1231 when N_Block_Statement =>
1234 when N_If_Statement =>
1236 -- Traverse the statements in the THEN part
1238 Traverse_Declarations_Or_Statements (Then_Statements (N));
1240 -- Loop through ELSIF parts if present
1242 if Present (Elsif_Parts (N)) then
1244 Elif : Node_Id := First (Elsif_Parts (N));
1247 while Present (Elif) loop
1248 Traverse_Declarations_Or_Statements
1249 (Then_Statements (Elif));
1255 -- Finally traverse the ELSE statements if present
1257 Traverse_Declarations_Or_Statements (Else_Statements (N));
1259 when N_Case_Statement =>
1261 -- Process case branches
1264 Alt : Node_Id := First (Alternatives (N));
1267 Traverse_Declarations_Or_Statements (Statements (Alt));
1273 when N_Extended_Return_Statement =>
1274 Traverse_Handled_Statement_Sequence
1275 (Handled_Statement_Sequence (N));
1277 when N_Loop_Statement =>
1278 Traverse_Declarations_Or_Statements (Statements (N));
1280 -- Generic declarations are ignored
1285 end Traverse_Declaration_Or_Statement;
1287 -----------------------------------
1288 -- Traverse_Declarations_And_HSS --
1289 -----------------------------------
1291 procedure Traverse_Declarations_And_HSS (N : Node_Id) is
1293 Traverse_Declarations_Or_Statements (Declarations (N));
1294 Traverse_Handled_Statement_Sequence (Handled_Statement_Sequence (N));
1295 end Traverse_Declarations_And_HSS;
1297 -----------------------------------------
1298 -- Traverse_Declarations_Or_Statements --
1299 -----------------------------------------
1301 procedure Traverse_Declarations_Or_Statements (L : List_Id) is
1305 -- Loop through statements or declarations
1308 while Present (N) loop
1310 -- Call Process on all declarations
1312 if Nkind (N) in N_Declaration
1313 or else Nkind (N) in N_Later_Decl_Item
1314 or else Nkind (N) = N_Entry_Body
1316 if Nkind (N) in N_Body_Stub then
1317 Process (Get_Body_From_Stub (N));
1323 Traverse_Declaration_Or_Statement (N);
1327 end Traverse_Declarations_Or_Statements;
1329 -----------------------------------------
1330 -- Traverse_Handled_Statement_Sequence --
1331 -----------------------------------------
1333 procedure Traverse_Handled_Statement_Sequence (N : Node_Id) is
1338 Traverse_Declarations_Or_Statements (Statements (N));
1340 if Present (Exception_Handlers (N)) then
1341 Handler := First (Exception_Handlers (N));
1342 while Present (Handler) loop
1343 Traverse_Declarations_Or_Statements (Statements (Handler));
1348 end Traverse_Handled_Statement_Sequence;
1350 ---------------------------
1351 -- Traverse_Package_Body --
1352 ---------------------------
1354 procedure Traverse_Package_Body (N : Node_Id) is
1355 Spec_E : constant Entity_Id := Unique_Defining_Entity (N);
1358 case Ekind (Spec_E) is
1360 Traverse_Declarations_And_HSS (N);
1362 when E_Generic_Package =>
1366 raise Program_Error;
1368 end Traverse_Package_Body;
1370 -----------------------------
1371 -- Traverse_Protected_Body --
1372 -----------------------------
1374 procedure Traverse_Protected_Body (N : Node_Id) is
1376 Traverse_Declarations_Or_Statements (Declarations (N));
1377 end Traverse_Protected_Body;
1379 ------------------------------
1380 -- Traverse_Subprogram_Body --
1381 ------------------------------
1383 procedure Traverse_Subprogram_Body (N : Node_Id) is
1384 Spec_E : constant Entity_Id := Unique_Defining_Entity (N);
1387 case Ekind (Spec_E) is
1392 Traverse_Declarations_And_HSS (N);
1394 when Generic_Subprogram_Kind =>
1398 raise Program_Error;
1400 end Traverse_Subprogram_Body;
1402 ------------------------
1403 -- Traverse_Task_Body --
1404 ------------------------
1406 procedure Traverse_Task_Body (N : Node_Id) renames
1407 Traverse_Declarations_And_HSS;
1409 ----------------------------------------
1410 -- Traverse_Visible_And_Private_Parts --
1411 ----------------------------------------
1413 procedure Traverse_Visible_And_Private_Parts (N : Node_Id) is
1415 Traverse_Declarations_Or_Statements (Visible_Declarations (N));
1416 Traverse_Declarations_Or_Statements (Private_Declarations (N));
1417 end Traverse_Visible_And_Private_Parts;
1423 -- Start of processing for Traverse_Compilation_Unit
1426 -- Get Unit (checking case of subunit)
1430 if Nkind (Lu) = N_Subunit then
1431 Lu := Proper_Body (Lu);
1434 -- Do not add scopes for generic units
1436 if Nkind (Lu) = N_Package_Body
1437 and then Ekind (Corresponding_Spec (Lu)) in Generic_Unit_Kind
1442 -- Call Process on all declarations
1444 if Nkind (Lu) in N_Declaration
1445 or else Nkind (Lu) in N_Later_Decl_Item
1450 -- Traverse the unit
1452 Traverse_Declaration_Or_Statement (Lu);
1453 end Traverse_Compilation_Unit;