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 Heap
: Entity_Id
:= Empty
;
70 -- A special entity which denotes the heap object
72 package Drefs
is new Table
.Table
(
73 Table_Component_Type
=> Xref_Entry
,
74 Table_Index_Type
=> Xref_Entry_Number
,
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.
84 -----------------------
85 -- Local Subprograms --
86 -----------------------
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.
95 procedure Add_SPARK_Xrefs
;
96 -- Filter table Xrefs to add all references used in SPARK to the table
99 function Entity_Hash
(E
: Entity_Id
) return Entity_Hashed_Range
;
100 -- Hash function for hash table
106 procedure Add_SPARK_File
(Uspec
, Ubody
: Unit_Number_Type
; Dspec
: Nat
) is
107 File
: constant Source_File_Index
:= Source_Index
(Uspec
);
108 From
: constant Scope_Index
:= SPARK_Scope_Table
.Last
+ 1;
112 procedure Add_SPARK_Scope
(N
: Node_Id
);
113 -- Add scope N to the table SPARK_Scope_Table
115 procedure Detect_And_Add_SPARK_Scope
(N
: Node_Id
);
116 -- Call Add_SPARK_Scope on scopes
118 ---------------------
119 -- Add_SPARK_Scope --
120 ---------------------
122 procedure Add_SPARK_Scope
(N
: Node_Id
) is
123 E
: constant Entity_Id
:= Defining_Entity
(N
);
124 Loc
: constant Source_Ptr
:= Sloc
(E
);
126 -- The character describing the kind of scope is chosen to be the
127 -- same as the one describing the corresponding entity in cross
128 -- references, see Xref_Entity_Letters in lib-xrefs.ads
133 -- Ignore scopes without a proper location
135 if Sloc
(N
) = No_Location
then
144 | E_Generic_Procedure
149 Typ
:= Xref_Entity_Letters
(Ekind
(E
));
154 -- In SPARK we need to distinguish protected functions and
155 -- procedures from ordinary subprograms, but there are no
156 -- special Xref letters for them. Since this distiction is
157 -- only needed to detect protected calls, we pretend that
158 -- such calls are entry calls.
160 if Ekind
(Scope
(E
)) = E_Protected_Type
then
161 Typ
:= Xref_Entity_Letters
(E_Entry
);
163 Typ
:= Xref_Entity_Letters
(Ekind
(E
));
171 Typ
:= Xref_Entity_Letters
(Ekind
(Unique_Entity
(E
)));
175 -- Compilation of prj-attr.adb with -gnatn creates a node with
176 -- entity E_Void for the package defined at a-charac.ads16:13.
185 -- File_Num and Scope_Num are filled later. From_Xref and To_Xref
186 -- are filled even later, but are initialized to represent an empty
189 SPARK_Scope_Table
.Append
190 ((Scope_Name
=> new String'(Unique_Name (E)),
192 Scope_Num => Scope_Id,
195 Line => Nat (Get_Logical_Line_Number (Loc)),
197 Col => Nat (Get_Column_Number (Loc)),
202 Scope_Id := Scope_Id + 1;
205 --------------------------------
206 -- Detect_And_Add_SPARK_Scope --
207 --------------------------------
209 procedure Detect_And_Add_SPARK_Scope (N : Node_Id) is
213 if Nkind_In (N, N_Entry_Body, N_Entry_Declaration)
217 or else Nkind_In (N, N_Package_Body,
218 N_Package_Declaration)
221 or else Nkind_In (N, N_Protected_Body,
222 N_Protected_Type_Declaration)
226 or else Nkind_In (N, N_Subprogram_Body,
227 N_Subprogram_Declaration)
231 or else Nkind_In (N, N_Task_Body,
232 N_Task_Type_Declaration)
236 end Detect_And_Add_SPARK_Scope;
238 procedure Traverse_Scopes is new
239 Traverse_Compilation_Unit (Detect_And_Add_SPARK_Scope);
243 File_Name : String_Ptr;
244 Unit_File_Name : String_Ptr;
246 -- Start of processing for Add_SPARK_File
249 -- Source file could be inexistant as a result of an error, if option
252 if File = No_Source_File then
256 -- Subunits are traversed as part of the top-level unit to which they
259 if Nkind (Unit (Cunit (Uspec))) = N_Subunit then
263 Traverse_Scopes (CU => Cunit (Uspec), Inside_Stubs => True);
265 -- When two units are present for the same compilation unit, as it
266 -- happens for library-level instantiations of generics, then add all
267 -- scopes to the same SPARK file.
269 if Ubody /= No_Unit then
270 Traverse_Scopes (CU => Cunit (Ubody), Inside_Stubs => True);
273 -- Make entry for new file in file table
275 Get_Name_String (Reference_Name (File));
276 File_Name := new String'(Name_Buffer
(1 .. Name_Len
));
278 -- For subunits, also retrieve the file name of the unit. Only do so if
279 -- unit has an associated compilation unit.
281 if Present
(Cunit
(Unit
(File
)))
282 and then Nkind
(Unit
(Cunit
(Unit
(File
)))) = N_Subunit
284 Get_Name_String
(Reference_Name
(Main_Source_File
));
285 Unit_File_Name
:= new String'(Name_Buffer (1 .. Name_Len));
287 Unit_File_Name := null;
290 SPARK_File_Table.Append (
291 (File_Name => File_Name,
292 Unit_File_Name => Unit_File_Name,
295 To_Scope => SPARK_Scope_Table.Last));
298 ---------------------
299 -- Add_SPARK_Xrefs --
300 ---------------------
302 procedure Add_SPARK_Xrefs is
303 function Entity_Of_Scope (S : Scope_Index) return Entity_Id;
304 -- Return the entity which maps to the input scope index
306 function Get_Entity_Type (E : Entity_Id) return Character;
307 -- Return a character representing the type of entity
309 function Get_Scope_Num (E : Entity_Id) return Nat;
310 -- Return the scope number associated with the entity E
312 function Is_Constant_Object_Without_Variable_Input
313 (E : Entity_Id) return Boolean;
314 -- Return True if E is known to have no variable input, as defined in
317 function Is_Future_Scope_Entity
319 S : Scope_Index) return Boolean;
320 -- Check whether entity E is in SPARK_Scope_Table at index S or higher
322 function Is_SPARK_Reference
324 Typ : Character) return Boolean;
325 -- Return whether entity reference E meets SPARK requirements. Typ is
326 -- the reference type.
328 function Is_SPARK_Scope (E : Entity_Id) return Boolean;
329 -- Return whether the entity or reference scope meets requirements for
330 -- being a SPARK scope.
332 function Lt (Op1 : Natural; Op2 : Natural) return Boolean;
333 -- Comparison function for Sort call
335 procedure Move (From : Natural; To : Natural);
336 -- Move procedure for Sort call
338 procedure Set_Scope_Num (E : Entity_Id; Num : Nat);
339 -- Associate entity E with the scope number Num
341 procedure Update_Scope_Range
345 -- Update the scope which maps to S with the new range From .. To
347 package Sorting is new GNAT.Heap_Sort_G (Move, Lt);
349 No_Scope : constant Nat := 0;
350 -- Initial scope counter
352 package Scopes is new GNAT.HTable.Simple_HTable
353 (Header_Num => Entity_Hashed_Range,
355 No_Element => No_Scope,
359 -- Package used to build a correspondence between entities and scope
360 -- numbers used in SPARK cross references.
362 Nrefs : Nat := Xrefs.Last;
363 -- Number of references in table. This value may get reset (reduced)
364 -- when we eliminate duplicate reference entries as well as references
365 -- not suitable for local cross-references.
367 Nrefs_Add : constant Nat := Drefs.Last;
368 -- Number of additional references which correspond to dereferences in
371 Rnums : array (0 .. Nrefs + Nrefs_Add) of Nat;
372 -- This array contains numbers of references in the Xrefs table. This
373 -- list is sorted in output order. The extra 0'th entry is convenient
374 -- for the call to sort. When we sort the table, we move the indices in
375 -- Rnums around, but we do not move the original table entries.
377 ---------------------
378 -- Entity_Of_Scope --
379 ---------------------
381 function Entity_Of_Scope (S : Scope_Index) return Entity_Id is
383 return SPARK_Scope_Table.Table (S).Scope_Entity;
386 ---------------------
387 -- Get_Entity_Type --
388 ---------------------
390 function Get_Entity_Type (E : Entity_Id) return Character is
393 when E_Out_Parameter => return '<';
394 when E_In_Out_Parameter => return '=';
395 when E_In_Parameter => return '>';
396 when others => return '*';
404 function Get_Scope_Num (E : Entity_Id) return Nat renames Scopes.Get;
406 -----------------------------------------------
407 -- Is_Constant_Object_Without_Variable_Input --
408 -----------------------------------------------
410 function Is_Constant_Object_Without_Variable_Input
411 (E : Entity_Id) return Boolean
416 -- A constant is known to have no variable input if its
417 -- initializing expression is static (a value which is
418 -- compile-time-known is not guaranteed to have no variable input
419 -- as defined in the SPARK RM). Otherwise, the constant may or not
420 -- have variable input.
426 if Present (Full_View (E)) then
427 Decl := Parent (Full_View (E));
432 if Is_Imported (E) then
435 pragma Assert (Present (Expression (Decl)));
436 return Is_Static_Expression (Expression (Decl));
448 end Is_Constant_Object_Without_Variable_Input;
450 ----------------------------
451 -- Is_Future_Scope_Entity --
452 ----------------------------
454 function Is_Future_Scope_Entity
456 S : Scope_Index) return Boolean
458 function Is_Past_Scope_Entity return Boolean;
459 -- Check whether entity E is in SPARK_Scope_Table at index strictly
462 --------------------------
463 -- Is_Past_Scope_Entity --
464 --------------------------
466 function Is_Past_Scope_Entity return Boolean is
468 for Index in SPARK_Scope_Table.First .. S - 1 loop
469 if SPARK_Scope_Table.Table (Index).Scope_Entity = E then
475 end Is_Past_Scope_Entity;
477 -- Start of processing for Is_Future_Scope_Entity
480 for Index in S .. SPARK_Scope_Table.Last loop
481 if SPARK_Scope_Table.Table (Index).Scope_Entity = E then
486 -- If this assertion fails, this means that the scope which we are
487 -- looking for has been treated already, which reveals a problem in
488 -- the order of cross-references.
490 pragma Assert (not Is_Past_Scope_Entity);
493 end Is_Future_Scope_Entity;
495 ------------------------
496 -- Is_SPARK_Reference --
497 ------------------------
499 function Is_SPARK_Reference
501 Typ : Character) return Boolean
504 -- The only references of interest on callable entities are calls. On
505 -- uncallable entities, the only references of interest are reads and
508 if Ekind (E) in Overloadable_Kind then
511 -- In all other cases, result is true for reference/modify cases,
512 -- and false for all other cases.
515 return Typ = 'r
' or else Typ = 'm
';
517 end Is_SPARK_Reference;
523 function Is_SPARK_Scope (E : Entity_Id) return Boolean is
524 Can_Be_Renamed : constant Boolean :=
526 and then (Is_Subprogram_Or_Entry (E)
527 or else Ekind (E) = E_Package);
530 and then not Is_Generic_Unit (E)
531 and then (not Can_Be_Renamed or else No (Renamed_Entity (E)))
532 and then Get_Scope_Num (E) /= No_Scope;
539 function Lt (Op1 : Natural; Op2 : Natural) return Boolean is
540 T1 : constant Xref_Entry := Xrefs.Table (Rnums (Nat (Op1)));
541 T2 : constant Xref_Entry := Xrefs.Table (Rnums (Nat (Op2)));
544 -- First test: if entity is in different unit, sort by unit. Note:
545 -- that we use Ent_Scope_File rather than Eun, as Eun may refer to
546 -- the file where the generic scope is defined, which may differ from
547 -- the file where the enclosing scope is defined. It is the latter
548 -- which matters for a correct order here.
550 if T1.Ent_Scope_File /= T2.Ent_Scope_File then
551 return Dependency_Num (T1.Ent_Scope_File) <
552 Dependency_Num (T2.Ent_Scope_File);
554 -- Second test: within same unit, sort by location of the scope of
555 -- the entity definition.
557 elsif Get_Scope_Num (T1.Key.Ent_Scope) /=
558 Get_Scope_Num (T2.Key.Ent_Scope)
560 return Get_Scope_Num (T1.Key.Ent_Scope) <
561 Get_Scope_Num (T2.Key.Ent_Scope);
563 -- Third test: within same unit and scope, sort by location of
564 -- entity definition.
566 elsif T1.Def /= T2.Def then
567 return T1.Def < T2.Def;
570 -- Both entities must be equal at this point
572 pragma Assert (T1.Key.Ent = T2.Key.Ent);
573 pragma Assert (T1.Key.Ent_Scope = T2.Key.Ent_Scope);
574 pragma Assert (T1.Ent_Scope_File = T2.Ent_Scope_File);
576 -- Fourth test: if reference is in same unit as entity definition,
579 if T1.Key.Lun /= T2.Key.Lun
580 and then T1.Ent_Scope_File = T1.Key.Lun
584 elsif T1.Key.Lun /= T2.Key.Lun
585 and then T2.Ent_Scope_File = T2.Key.Lun
589 -- Fifth test: if reference is in same unit and same scope as
590 -- entity definition, sort first.
592 elsif T1.Ent_Scope_File = T1.Key.Lun
593 and then T1.Key.Ref_Scope /= T2.Key.Ref_Scope
594 and then T1.Key.Ent_Scope = T1.Key.Ref_Scope
598 elsif T2.Ent_Scope_File = T2.Key.Lun
599 and then T1.Key.Ref_Scope /= T2.Key.Ref_Scope
600 and then T2.Key.Ent_Scope = T2.Key.Ref_Scope
604 -- Sixth test: for same entity, sort by reference location unit
606 elsif T1.Key.Lun /= T2.Key.Lun then
607 return Dependency_Num (T1.Key.Lun) <
608 Dependency_Num (T2.Key.Lun);
610 -- Seventh test: for same entity, sort by reference location scope
612 elsif Get_Scope_Num (T1.Key.Ref_Scope) /=
613 Get_Scope_Num (T2.Key.Ref_Scope)
615 return Get_Scope_Num (T1.Key.Ref_Scope) <
616 Get_Scope_Num (T2.Key.Ref_Scope);
618 -- Eighth test: order of location within referencing unit
620 elsif T1.Key.Loc /= T2.Key.Loc then
621 return T1.Key.Loc < T2.Key.Loc;
623 -- Finally, for two locations at the same address prefer the one
624 -- that does NOT have the type 'r
', so that a modification or
625 -- extension takes preference, when there are more than one
626 -- reference at the same location. As a result, in the case of
627 -- entities that are in-out actuals, the read reference follows
628 -- the modify reference.
631 return T2.Key.Typ = 'r
';
640 procedure Move (From : Natural; To : Natural) is
642 Rnums (Nat (To)) := Rnums (Nat (From));
649 procedure Set_Scope_Num (E : Entity_Id; Num : Nat) renames Scopes.Set;
651 ------------------------
652 -- Update_Scope_Range --
653 ------------------------
655 procedure Update_Scope_Range
661 SPARK_Scope_Table.Table (S).From_Xref := From;
662 SPARK_Scope_Table.Table (S).To_Xref := To;
663 end Update_Scope_Range;
668 From_Index : Xref_Index;
670 Prev_Loc : Source_Ptr;
671 Prev_Typ : Character;
674 Ref_Name : String_Ptr;
675 Scope_Id : Scope_Index;
677 -- Start of processing for Add_SPARK_Xrefs
680 for Index in SPARK_Scope_Table.First .. SPARK_Scope_Table.Last loop
682 S : SPARK_Scope_Record renames SPARK_Scope_Table.Table (Index);
684 Set_Scope_Num (S.Scope_Entity, S.Scope_Num);
689 Drefs_Table : Drefs.Table_Type
690 renames Drefs.Table (Drefs.First .. Drefs.Last);
692 Xrefs.Append_All (Xrefs.Table_Type (Drefs_Table));
693 Nrefs := Nrefs + Drefs_Table'Length;
696 -- Capture the definition Sloc values. As in the case of normal cross
697 -- references, we have to wait until now to get the correct value.
699 for Index in 1 .. Nrefs loop
700 Xrefs.Table (Index).Def := Sloc (Xrefs.Table (Index).Key.Ent);
703 -- Eliminate entries not appropriate for SPARK. Done prior to sorting
704 -- cross-references, as it discards useless references which do not have
705 -- a proper format for the comparison function (like no location).
710 for Index in 1 .. Ref_Count loop
712 Ref : Xref_Key renames Xrefs.Table (Index).Key;
715 if SPARK_Entities (Ekind (Ref.Ent))
716 and then SPARK_References (Ref.Typ)
717 and then Is_SPARK_Scope (Ref.Ent_Scope)
718 and then Is_SPARK_Scope (Ref.Ref_Scope)
719 and then Is_SPARK_Reference (Ref.Ent, Ref.Typ)
721 -- Discard references from unknown scopes, e.g. generic scopes
723 and then Get_Scope_Num (Ref.Ent_Scope) /= No_Scope
724 and then Get_Scope_Num (Ref.Ref_Scope) /= No_Scope
726 -- Discard references to loop parameters introduced within
727 -- expression functions, as they give two references: one from
728 -- the analysis of the expression function itself and one from
729 -- the analysis of the expanded body. We don't lose any globals
730 -- by discarding them, because such loop parameters can only be
731 -- accessed locally from within the expression function body.
734 (Ekind (Ref.Ent) = E_Loop_Parameter
735 and then Scope_Within
736 (Ref.Ent, Unique_Entity (Ref.Ref_Scope))
737 and then Is_Expression_Function (Ref.Ref_Scope))
740 Rnums (Nrefs) := Index;
745 -- Sort the references
747 Sorting.Sort (Integer (Nrefs));
749 -- Eliminate duplicate entries
751 -- We need this test for Ref_Count because if we force ALI file
752 -- generation in case of errors detected, it may be the case that
753 -- Nrefs is 0, so we should not reset it here.
759 for Index in 2 .. Ref_Count loop
760 if Xrefs.Table (Rnums (Index)) /= Xrefs.Table (Rnums (Nrefs)) then
762 Rnums (Nrefs) := Rnums (Index);
767 -- Eliminate the reference if it is at the same location as the previous
768 -- one, unless it is a read-reference indicating that the entity is an
769 -- in-out actual in a call.
773 Prev_Loc := No_Location;
776 for Index in 1 .. Ref_Count loop
778 Ref : Xref_Key renames Xrefs.Table (Rnums (Index)).Key;
781 if Ref.Loc /= Prev_Loc
782 or else (Prev_Typ = 'm
' and then Ref.Typ = 'r
')
787 Rnums (Nrefs) := Rnums (Index);
792 -- The two steps have eliminated all references, nothing to do
794 if SPARK_Scope_Table.Last = 0 then
802 -- Loop to output references
804 for Refno in 1 .. Nrefs loop
806 Ref_Entry : Xref_Entry renames Xrefs.Table (Rnums (Refno));
807 Ref : Xref_Key renames Ref_Entry.Key;
811 -- If this assertion fails, the scope which we are looking for is
812 -- not in SPARK scope table, which reveals either a problem in the
813 -- construction of the scope table, or an erroneous scope for the
814 -- current cross-reference.
816 pragma Assert (Is_Future_Scope_Entity (Ref.Ent_Scope, Scope_Id));
818 -- Update the range of cross references to which the current scope
819 -- refers to. This may be the empty range only for the first scope
822 if Ref.Ent_Scope /= Entity_Of_Scope (Scope_Id) then
826 To => SPARK_Xref_Table.Last);
828 From_Index := SPARK_Xref_Table.Last + 1;
831 while Ref.Ent_Scope /= Entity_Of_Scope (Scope_Id) loop
832 Scope_Id := Scope_Id + 1;
833 pragma Assert (Scope_Id <= SPARK_Scope_Table.Last);
836 if Ref.Ent /= Ref_Id then
837 Ref_Name := new String'(Unique_Name
(Ref
.Ent
));
840 if Ref
.Ent
= Heap
then
844 Line
:= Nat
(Get_Logical_Line_Number
(Ref_Entry
.Def
));
845 Col
:= Nat
(Get_Column_Number
(Ref_Entry
.Def
));
848 -- References to constant objects without variable inputs (see
849 -- SPARK RM 3.3.1) are considered specially in SPARK section,
850 -- because these will be translated as constants in the
851 -- intermediate language for formal verification, and should
852 -- therefore never appear in frame conditions. Other constants may
853 -- later be treated the same, up to GNATprove to decide based on
854 -- its flow analysis.
856 if Is_Constant_Object_Without_Variable_Input
(Ref
.Ent
) then
862 SPARK_Xref_Table
.Append
(
863 (Entity_Name
=> Ref_Name
,
865 Etype
=> Get_Entity_Type
(Ref
.Ent
),
867 File_Num
=> Dependency_Num
(Ref
.Lun
),
868 Scope_Num
=> Get_Scope_Num
(Ref
.Ref_Scope
),
869 Line
=> Nat
(Get_Logical_Line_Number
(Ref
.Loc
)),
871 Col
=> Nat
(Get_Column_Number
(Ref
.Loc
))));
875 -- Update the range of cross references to which the scope refers to
880 To
=> SPARK_Xref_Table
.Last
);
883 -------------------------
884 -- Collect_SPARK_Xrefs --
885 -------------------------
887 procedure Collect_SPARK_Xrefs
888 (Sdep_Table
: Unit_Ref_Table
;
893 -- Index of the current and next source dependency
896 -- Index of the file to which the scopes need to be assigned; for
897 -- library-level instances of generic units this points to the unit
898 -- of the body, because this is where references are assigned to.
900 Ubody
: Unit_Number_Type
;
901 Uspec
: Unit_Number_Type
;
902 -- Unit numbers for the dependency spec and possibly its body (only in
903 -- the case of library-level instance of a generic package).
906 -- Cross-references should have been computed first
908 pragma Assert
(Xrefs
.Last
/= 0);
910 Initialize_SPARK_Tables
;
912 -- Generate file and scope SPARK cross-reference information
915 while Sdep
<= Num_Sdep
loop
917 -- Skip dependencies with no entity node, e.g. configuration files
918 -- with pragmas (.adc) or target description (.atp), since they
919 -- present no interest for SPARK cross references.
921 if No
(Cunit_Entity
(Sdep_Table
(Sdep
))) then
922 Sdep_Next
:= Sdep
+ 1;
924 -- For library-level instantiation of a generic, two consecutive
925 -- units refer to the same compilation unit node and entity (one to
926 -- body, one to spec). In that case, treat them as a single unit for
927 -- the sake of SPARK cross references by passing to Add_SPARK_File.
931 and then Cunit_Entity
(Sdep_Table
(Sdep
)) =
932 Cunit_Entity
(Sdep_Table
(Sdep
+ 1))
935 Cunit1
: Node_Id
renames Cunit
(Sdep_Table
(Sdep
));
936 Cunit2
: Node_Id
renames Cunit
(Sdep_Table
(Sdep
+ 1));
939 -- Both Cunits point to compilation unit nodes
942 (Nkind
(Cunit1
) = N_Compilation_Unit
943 and then Nkind
(Cunit2
) = N_Compilation_Unit
);
945 -- Do not depend on the sorting order, which is based on
946 -- Unit_Name, and for library-level instances of nested
947 -- generic packages they are equal.
949 -- If declaration comes before the body
951 if Nkind
(Unit
(Cunit1
)) = N_Package_Declaration
952 and then Nkind
(Unit
(Cunit2
)) = N_Package_Body
954 Uspec
:= Sdep_Table
(Sdep
);
955 Ubody
:= Sdep_Table
(Sdep
+ 1);
957 Sdep_File
:= Sdep
+ 1;
959 -- If body comes before declaration
961 elsif Nkind
(Unit
(Cunit1
)) = N_Package_Body
962 and then Nkind
(Unit
(Cunit2
)) = N_Package_Declaration
964 Uspec
:= Sdep_Table
(Sdep
+ 1);
965 Ubody
:= Sdep_Table
(Sdep
);
969 -- Otherwise it is an error
975 Sdep_Next
:= Sdep
+ 2;
981 Uspec
:= Sdep_Table
(Sdep
);
985 Sdep_Next
:= Sdep
+ 1;
997 -- Fill in the spec information when relevant
1000 package Entity_Hash_Table
is new
1001 GNAT
.HTable
.Simple_HTable
1002 (Header_Num
=> Entity_Hashed_Range
,
1003 Element
=> Scope_Index
,
1006 Hash
=> Entity_Hash
,
1010 -- Fill in the hash-table
1012 for S
in SPARK_Scope_Table
.First
.. SPARK_Scope_Table
.Last
loop
1014 Srec
: SPARK_Scope_Record
renames SPARK_Scope_Table
.Table
(S
);
1016 Entity_Hash_Table
.Set
(Srec
.Scope_Entity
, S
);
1020 -- Use the hash-table to locate spec entities
1022 for S
in SPARK_Scope_Table
.First
.. SPARK_Scope_Table
.Last
loop
1024 Srec
: SPARK_Scope_Record
renames SPARK_Scope_Table
.Table
(S
);
1026 Spec_Entity
: constant Entity_Id
:=
1027 Unique_Entity
(Srec
.Scope_Entity
);
1028 Spec_Scope
: constant Scope_Index
:=
1029 Entity_Hash_Table
.Get
(Spec_Entity
);
1032 -- Generic spec may be missing in which case Spec_Scope is zero
1034 if Spec_Entity
/= Srec
.Scope_Entity
1035 and then Spec_Scope
/= 0
1037 Srec
.Spec_File_Num
:=
1038 SPARK_Scope_Table
.Table
(Spec_Scope
).File_Num
;
1039 Srec
.Spec_Scope_Num
:=
1040 SPARK_Scope_Table
.Table
(Spec_Scope
).Scope_Num
;
1046 -- Generate SPARK cross-reference information
1049 end Collect_SPARK_Xrefs
;
1051 -------------------------------------
1052 -- Enclosing_Subprogram_Or_Package --
1053 -------------------------------------
1055 function Enclosing_Subprogram_Or_Library_Package
1056 (N
: Node_Id
) return Entity_Id
1058 Context
: Entity_Id
;
1061 -- If N is the defining identifier for a subprogram, then return the
1062 -- enclosing subprogram or package, not this subprogram.
1064 if Nkind_In
(N
, N_Defining_Identifier
, N_Defining_Operator_Symbol
)
1065 and then (Ekind
(N
) in Entry_Kind
1066 or else Ekind
(N
) = E_Subprogram_Body
1067 or else Ekind
(N
) in Generic_Subprogram_Kind
1068 or else Ekind
(N
) in Subprogram_Kind
)
1070 Context
:= Parent
(Unit_Declaration_Node
(N
));
1072 -- If this was a library-level subprogram then replace Context with
1073 -- its Unit, which points to N_Subprogram_* node.
1075 if Nkind
(Context
) = N_Compilation_Unit
then
1076 Context
:= Unit
(Context
);
1082 while Present
(Context
) loop
1083 case Nkind
(Context
) is
1085 | N_Package_Specification
1087 -- Only return a library-level package
1089 if Is_Library_Level_Entity
(Defining_Entity
(Context
)) then
1090 Context
:= Defining_Entity
(Context
);
1093 Context
:= Parent
(Context
);
1098 -- The enclosing subprogram for a precondition, postcondition,
1099 -- or contract case should be the declaration preceding the
1100 -- pragma (skipping any other pragmas between this pragma and
1101 -- this declaration.
1103 while Nkind
(Context
) = N_Pragma
1104 and then Is_List_Member
(Context
)
1105 and then Present
(Prev
(Context
))
1107 Context
:= Prev
(Context
);
1110 if Nkind
(Context
) = N_Pragma
then
1111 Context
:= Parent
(Context
);
1115 | N_Entry_Declaration
1116 | N_Protected_Type_Declaration
1118 | N_Subprogram_Declaration
1119 | N_Subprogram_Specification
1121 | N_Task_Type_Declaration
1123 Context
:= Defining_Entity
(Context
);
1127 Context
:= Parent
(Context
);
1131 if Nkind
(Context
) = N_Defining_Program_Unit_Name
then
1132 Context
:= Defining_Identifier
(Context
);
1135 -- Do not return a scope without a proper location
1137 if Present
(Context
)
1138 and then Sloc
(Context
) = No_Location
1144 end Enclosing_Subprogram_Or_Library_Package
;
1150 function Entity_Hash
(E
: Entity_Id
) return Entity_Hashed_Range
is
1153 Entity_Hashed_Range
(E
mod (Entity_Id
(Entity_Hashed_Range
'Last) + 1));
1156 --------------------------
1157 -- Generate_Dereference --
1158 --------------------------
1160 procedure Generate_Dereference
1162 Typ
: Character := 'r')
1164 procedure Create_Heap
;
1165 -- Create and decorate the special entity which denotes the heap
1171 procedure Create_Heap
is
1173 Name_Len
:= Name_Of_Heap_Variable
'Length;
1174 Name_Buffer
(1 .. Name_Len
) := Name_Of_Heap_Variable
;
1176 Heap
:= Make_Defining_Identifier
(Standard_Location
, Name_Enter
);
1178 Set_Ekind
(Heap
, E_Variable
);
1179 Set_Is_Internal
(Heap
, True);
1180 Set_Has_Fully_Qualified_Name
(Heap
);
1185 Loc
: constant Source_Ptr
:= Sloc
(N
);
1187 -- Start of processing for Generate_Dereference
1190 if Loc
> No_Location
then
1191 Drefs
.Increment_Last
;
1194 Deref_Entry
: Xref_Entry
renames Drefs
.Table
(Drefs
.Last
);
1195 Deref
: Xref_Key
renames Deref_Entry
.Key
;
1206 -- It is as if the special "Heap" was defined in the main unit,
1207 -- in the scope of the entity for the main unit. This single
1208 -- definition point is required to ensure that sorting cross
1209 -- references works for "Heap" references as well.
1211 Deref
.Eun
:= Main_Unit
;
1212 Deref
.Lun
:= Get_Top_Level_Code_Unit
(Loc
);
1214 Deref
.Ref_Scope
:= Enclosing_Subprogram_Or_Library_Package
(N
);
1215 Deref
.Ent_Scope
:= Cunit_Entity
(Main_Unit
);
1217 Deref_Entry
.Def
:= No_Location
;
1219 Deref_Entry
.Ent_Scope_File
:= Main_Unit
;
1222 end Generate_Dereference
;
1224 -------------------------------
1225 -- Traverse_Compilation_Unit --
1226 -------------------------------
1228 procedure Traverse_Compilation_Unit
1230 Inside_Stubs
: Boolean)
1232 procedure Traverse_Block
(N
: Node_Id
);
1233 procedure Traverse_Declaration_Or_Statement
(N
: Node_Id
);
1234 procedure Traverse_Declarations_And_HSS
(N
: Node_Id
);
1235 procedure Traverse_Declarations_Or_Statements
(L
: List_Id
);
1236 procedure Traverse_Handled_Statement_Sequence
(N
: Node_Id
);
1237 procedure Traverse_Package_Body
(N
: Node_Id
);
1238 procedure Traverse_Visible_And_Private_Parts
(N
: Node_Id
);
1239 procedure Traverse_Protected_Body
(N
: Node_Id
);
1240 procedure Traverse_Subprogram_Body
(N
: Node_Id
);
1241 procedure Traverse_Task_Body
(N
: Node_Id
);
1243 -- Traverse corresponding construct, calling Process on all declarations
1245 --------------------
1246 -- Traverse_Block --
1247 --------------------
1249 procedure Traverse_Block
(N
: Node_Id
) renames
1250 Traverse_Declarations_And_HSS
;
1252 ---------------------------------------
1253 -- Traverse_Declaration_Or_Statement --
1254 ---------------------------------------
1256 procedure Traverse_Declaration_Or_Statement
(N
: Node_Id
) is
1257 function Traverse_Stub
(N
: Node_Id
) return Boolean;
1258 -- Returns True iff stub N should be traversed
1260 function Traverse_Stub
(N
: Node_Id
) return Boolean is
1262 pragma Assert
(Nkind_In
(N
, N_Package_Body_Stub
,
1263 N_Protected_Body_Stub
,
1264 N_Subprogram_Body_Stub
,
1267 return Inside_Stubs
and then Present
(Library_Unit
(N
));
1270 -- Start of processing for Traverse_Declaration_Or_Statement
1274 when N_Package_Declaration
=>
1275 Traverse_Visible_And_Private_Parts
(Specification
(N
));
1277 when N_Package_Body
=>
1278 Traverse_Package_Body
(N
);
1280 when N_Package_Body_Stub
=>
1281 if Traverse_Stub
(N
) then
1282 Traverse_Package_Body
(Get_Body_From_Stub
(N
));
1285 when N_Subprogram_Body
=>
1286 Traverse_Subprogram_Body
(N
);
1288 when N_Entry_Body
=>
1289 Traverse_Subprogram_Body
(N
);
1291 when N_Subprogram_Body_Stub
=>
1292 if Traverse_Stub
(N
) then
1293 Traverse_Subprogram_Body
(Get_Body_From_Stub
(N
));
1296 when N_Protected_Body
=>
1297 Traverse_Protected_Body
(N
);
1299 when N_Protected_Body_Stub
=>
1300 if Traverse_Stub
(N
) then
1301 Traverse_Protected_Body
(Get_Body_From_Stub
(N
));
1304 when N_Protected_Type_Declaration
=>
1305 Traverse_Visible_And_Private_Parts
(Protected_Definition
(N
));
1307 when N_Task_Type_Declaration
=>
1309 -- Task type definition is optional (unlike protected type
1310 -- definition, which is mandatory).
1313 Task_Def
: constant Node_Id
:= Task_Definition
(N
);
1315 if Present
(Task_Def
) then
1316 Traverse_Visible_And_Private_Parts
(Task_Def
);
1321 Traverse_Task_Body
(N
);
1323 when N_Task_Body_Stub
=>
1324 if Traverse_Stub
(N
) then
1325 Traverse_Task_Body
(Get_Body_From_Stub
(N
));
1328 when N_Block_Statement
=>
1331 when N_If_Statement
=>
1333 -- Traverse the statements in the THEN part
1335 Traverse_Declarations_Or_Statements
(Then_Statements
(N
));
1337 -- Loop through ELSIF parts if present
1339 if Present
(Elsif_Parts
(N
)) then
1341 Elif
: Node_Id
:= First
(Elsif_Parts
(N
));
1344 while Present
(Elif
) loop
1345 Traverse_Declarations_Or_Statements
1346 (Then_Statements
(Elif
));
1352 -- Finally traverse the ELSE statements if present
1354 Traverse_Declarations_Or_Statements
(Else_Statements
(N
));
1356 when N_Case_Statement
=>
1358 -- Process case branches
1361 Alt
: Node_Id
:= First
(Alternatives
(N
));
1364 Traverse_Declarations_Or_Statements
(Statements
(Alt
));
1370 when N_Extended_Return_Statement
=>
1371 Traverse_Handled_Statement_Sequence
1372 (Handled_Statement_Sequence
(N
));
1374 when N_Loop_Statement
=>
1375 Traverse_Declarations_Or_Statements
(Statements
(N
));
1377 -- Generic declarations are ignored
1382 end Traverse_Declaration_Or_Statement
;
1384 -----------------------------------
1385 -- Traverse_Declarations_And_HSS --
1386 -----------------------------------
1388 procedure Traverse_Declarations_And_HSS
(N
: Node_Id
) is
1390 Traverse_Declarations_Or_Statements
(Declarations
(N
));
1391 Traverse_Handled_Statement_Sequence
(Handled_Statement_Sequence
(N
));
1392 end Traverse_Declarations_And_HSS
;
1394 -----------------------------------------
1395 -- Traverse_Declarations_Or_Statements --
1396 -----------------------------------------
1398 procedure Traverse_Declarations_Or_Statements
(L
: List_Id
) is
1402 -- Loop through statements or declarations
1405 while Present
(N
) loop
1407 -- Call Process on all declarations
1409 if Nkind
(N
) in N_Declaration
1410 or else Nkind
(N
) in N_Later_Decl_Item
1411 or else Nkind
(N
) = N_Entry_Body
1413 if Nkind
(N
) in N_Body_Stub
then
1414 Process
(Get_Body_From_Stub
(N
));
1420 Traverse_Declaration_Or_Statement
(N
);
1424 end Traverse_Declarations_Or_Statements
;
1426 -----------------------------------------
1427 -- Traverse_Handled_Statement_Sequence --
1428 -----------------------------------------
1430 procedure Traverse_Handled_Statement_Sequence
(N
: Node_Id
) is
1435 Traverse_Declarations_Or_Statements
(Statements
(N
));
1437 if Present
(Exception_Handlers
(N
)) then
1438 Handler
:= First
(Exception_Handlers
(N
));
1439 while Present
(Handler
) loop
1440 Traverse_Declarations_Or_Statements
(Statements
(Handler
));
1445 end Traverse_Handled_Statement_Sequence
;
1447 ---------------------------
1448 -- Traverse_Package_Body --
1449 ---------------------------
1451 procedure Traverse_Package_Body
(N
: Node_Id
) is
1452 Spec_E
: constant Entity_Id
:= Unique_Defining_Entity
(N
);
1455 case Ekind
(Spec_E
) is
1457 Traverse_Declarations_And_HSS
(N
);
1459 when E_Generic_Package
=>
1463 raise Program_Error
;
1465 end Traverse_Package_Body
;
1467 -----------------------------
1468 -- Traverse_Protected_Body --
1469 -----------------------------
1471 procedure Traverse_Protected_Body
(N
: Node_Id
) is
1473 Traverse_Declarations_Or_Statements
(Declarations
(N
));
1474 end Traverse_Protected_Body
;
1476 ------------------------------
1477 -- Traverse_Subprogram_Body --
1478 ------------------------------
1480 procedure Traverse_Subprogram_Body
(N
: Node_Id
) is
1481 Spec_E
: constant Entity_Id
:= Unique_Defining_Entity
(N
);
1484 case Ekind
(Spec_E
) is
1489 Traverse_Declarations_And_HSS
(N
);
1491 when Generic_Subprogram_Kind
=>
1495 raise Program_Error
;
1497 end Traverse_Subprogram_Body
;
1499 ------------------------
1500 -- Traverse_Task_Body --
1501 ------------------------
1503 procedure Traverse_Task_Body
(N
: Node_Id
) renames
1504 Traverse_Declarations_And_HSS
;
1506 ----------------------------------------
1507 -- Traverse_Visible_And_Private_Parts --
1508 ----------------------------------------
1510 procedure Traverse_Visible_And_Private_Parts
(N
: Node_Id
) is
1512 Traverse_Declarations_Or_Statements
(Visible_Declarations
(N
));
1513 Traverse_Declarations_Or_Statements
(Private_Declarations
(N
));
1514 end Traverse_Visible_And_Private_Parts
;
1520 -- Start of processing for Traverse_Compilation_Unit
1523 -- Get Unit (checking case of subunit)
1527 if Nkind
(Lu
) = N_Subunit
then
1528 Lu
:= Proper_Body
(Lu
);
1531 -- Do not add scopes for generic units
1533 if Nkind
(Lu
) = N_Package_Body
1534 and then Ekind
(Corresponding_Spec
(Lu
)) in Generic_Unit_Kind
1539 -- Call Process on all declarations
1541 if Nkind
(Lu
) in N_Declaration
1542 or else Nkind
(Lu
) in N_Later_Decl_Item
1547 -- Traverse the unit
1549 Traverse_Declaration_Or_Statement
(Lu
);
1550 end Traverse_Compilation_Unit
;