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-2014, 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 :=
44 E_In_Out_Parameter
=> True,
45 E_In_Parameter
=> True,
46 E_Loop_Parameter
=> True,
48 E_Out_Parameter
=> True,
53 -- True for each reference type used in SPARK
55 SPARK_References
: constant array (Character) of Boolean :=
61 type Entity_Hashed_Range
is range 0 .. 255;
62 -- Size of hash table headers
68 Heap
: Entity_Id
:= Empty
;
69 -- A special entity which denotes the heap object
71 package Drefs
is new Table
.Table
(
72 Table_Component_Type
=> Xref_Entry
,
73 Table_Index_Type
=> Xref_Entry_Number
,
75 Table_Initial
=> Alloc
.Drefs_Initial
,
76 Table_Increment
=> Alloc
.Drefs_Increment
,
77 Table_Name
=> "Drefs");
78 -- Table of cross-references for reads and writes through explicit
79 -- dereferences, that are output as reads/writes to the special variable
80 -- "Heap". These references are added to the regular references when
81 -- computing SPARK cross-references.
83 -----------------------
84 -- Local Subprograms --
85 -----------------------
87 procedure Add_SPARK_File
(Ubody
, Uspec
: Unit_Number_Type
; Dspec
: Nat
);
88 -- Add file and corresponding scopes for unit to the tables
89 -- SPARK_File_Table and SPARK_Scope_Table. When two units are present for
90 -- the same compilation unit, as it happens for library-level
91 -- instantiations of generics, then Ubody /= Uspec, and all scopes are
92 -- added to the same SPARK file. Otherwise Ubody = Uspec.
94 procedure Add_SPARK_Scope
(N
: Node_Id
);
95 -- Add scope N to the table SPARK_Scope_Table
97 procedure Add_SPARK_Xrefs
;
98 -- Filter table Xrefs to add all references used in SPARK to the table
101 procedure Detect_And_Add_SPARK_Scope
(N
: Node_Id
);
102 -- Call Add_SPARK_Scope on scopes
104 function Entity_Hash
(E
: Entity_Id
) return Entity_Hashed_Range
;
105 -- Hash function for hash table
107 procedure Traverse_Declarations_Or_Statements
109 Process
: Node_Processing
;
110 Inside_Stubs
: Boolean);
111 procedure Traverse_Handled_Statement_Sequence
113 Process
: Node_Processing
;
114 Inside_Stubs
: Boolean);
115 procedure Traverse_Package_Body
117 Process
: Node_Processing
;
118 Inside_Stubs
: Boolean);
119 procedure Traverse_Package_Declaration
121 Process
: Node_Processing
;
122 Inside_Stubs
: Boolean);
123 procedure Traverse_Subprogram_Body
125 Process
: Node_Processing
;
126 Inside_Stubs
: Boolean);
127 -- Traverse corresponding construct, calling Process on all declarations
133 procedure Add_SPARK_File
(Ubody
, Uspec
: Unit_Number_Type
; Dspec
: Nat
) is
134 File
: constant Source_File_Index
:= Source_Index
(Uspec
);
137 File_Name
: String_Ptr
;
138 Unit_File_Name
: String_Ptr
;
141 -- Source file could be inexistant as a result of an error, if option
144 if File
= No_Source_File
then
148 From
:= SPARK_Scope_Table
.Last
+ 1;
150 -- Unit might not have an associated compilation unit, as seen in code
151 -- filling Sdep_Table in Write_ALI.
153 if Present
(Cunit
(Ubody
)) then
154 Traverse_Compilation_Unit
155 (CU
=> Cunit
(Ubody
),
156 Process
=> Detect_And_Add_SPARK_Scope
'Access,
157 Inside_Stubs
=> False);
160 -- When two units are present for the same compilation unit, as it
161 -- happens for library-level instantiations of generics, then add all
162 -- scopes to the same SPARK file.
164 if Ubody
/= Uspec
then
165 if Present
(Cunit
(Uspec
)) then
166 Traverse_Compilation_Unit
167 (CU
=> Cunit
(Uspec
),
168 Process
=> Detect_And_Add_SPARK_Scope
'Access,
169 Inside_Stubs
=> False);
173 -- Update scope numbers
179 for Index
in From
.. SPARK_Scope_Table
.Last
loop
181 S
: SPARK_Scope_Record
renames SPARK_Scope_Table
.Table
(Index
);
183 S
.Scope_Num
:= Scope_Id
;
185 Scope_Id
:= Scope_Id
+ 1;
190 -- Remove those scopes previously marked for removal
193 Scope_Id
: Scope_Index
;
197 for Index
in From
.. SPARK_Scope_Table
.Last
loop
199 S
: SPARK_Scope_Record
renames SPARK_Scope_Table
.Table
(Index
);
201 if S
.Scope_Num
/= 0 then
202 SPARK_Scope_Table
.Table
(Scope_Id
) := S
;
203 Scope_Id
:= Scope_Id
+ 1;
208 SPARK_Scope_Table
.Set_Last
(Scope_Id
- 1);
211 -- Make entry for new file in file table
213 Get_Name_String
(Reference_Name
(File
));
214 File_Name
:= new String'(Name_Buffer (1 .. Name_Len));
216 -- For subunits, also retrieve the file name of the unit. Only do so if
217 -- unit has an associated compilation unit.
219 if Present (Cunit (Uspec))
220 and then Present (Cunit (Unit (File)))
221 and then Nkind (Unit (Cunit (Unit (File)))) = N_Subunit
223 Get_Name_String (Reference_Name (Main_Source_File));
224 Unit_File_Name := new String'(Name_Buffer
(1 .. Name_Len
));
227 SPARK_File_Table
.Append
(
228 (File_Name
=> File_Name
,
229 Unit_File_Name
=> Unit_File_Name
,
232 To_Scope
=> SPARK_Scope_Table
.Last
));
235 ---------------------
236 -- Add_SPARK_Scope --
237 ---------------------
239 procedure Add_SPARK_Scope
(N
: Node_Id
) is
240 E
: constant Entity_Id
:= Defining_Entity
(N
);
241 Loc
: constant Source_Ptr
:= Sloc
(E
);
245 -- Ignore scopes without a proper location
247 if Sloc
(N
) = No_Location
then
252 when E_Function | E_Generic_Function
=>
255 when E_Procedure | E_Generic_Procedure
=>
258 when E_Subprogram_Body
=>
265 if Nkind
(Spec
) = N_Defining_Program_Unit_Name
then
266 Spec
:= Parent
(Spec
);
269 if Nkind
(Spec
) = N_Function_Specification
then
273 (Nkind
(Spec
) = N_Procedure_Specification
);
278 when E_Package | E_Package_Body | E_Generic_Package
=>
282 -- Compilation of prj-attr.adb with -gnatn creates a node with
283 -- entity E_Void for the package defined at a-charac.ads16:13
293 -- File_Num and Scope_Num are filled later. From_Xref and To_Xref are
294 -- filled even later, but are initialized to represent an empty range.
296 SPARK_Scope_Table
.Append
(
297 (Scope_Name
=> new String'(Unique_Name (E)),
302 Line => Nat (Get_Logical_Line_Number (Loc)),
304 Col => Nat (Get_Column_Number (Loc)),
310 ---------------------
311 -- Add_SPARK_Xrefs --
312 ---------------------
314 procedure Add_SPARK_Xrefs is
315 function Entity_Of_Scope (S : Scope_Index) return Entity_Id;
316 -- Return the entity which maps to the input scope index
318 function Get_Entity_Type (E : Entity_Id) return Character;
319 -- Return a character representing the type of entity
321 function Is_SPARK_Reference
323 Typ : Character) return Boolean;
324 -- Return whether entity reference E meets SPARK requirements. Typ is
325 -- the reference type.
327 function Is_SPARK_Scope (E : Entity_Id) return Boolean;
328 -- Return whether the entity or reference scope meets requirements for
329 -- being an SPARK scope.
331 function Is_Future_Scope_Entity
333 S : Scope_Index) return Boolean;
334 -- Check whether entity E is in SPARK_Scope_Table at index S or higher
336 function Lt (Op1 : Natural; Op2 : Natural) return Boolean;
337 -- Comparison function for Sort call
339 procedure Move (From : Natural; To : Natural);
340 -- Move procedure for Sort call
342 procedure Update_Scope_Range
346 -- Update the scope which maps to S with the new range From .. To
348 package Sorting is new GNAT.Heap_Sort_G (Move, Lt);
350 function Get_Scope_Num (N : Entity_Id) return Nat;
351 -- Return the scope number associated to entity N
353 procedure Set_Scope_Num (N : Entity_Id; Num : Nat);
354 -- Associate entity N to scope number Num
356 No_Scope : constant Nat := 0;
357 -- Initial scope counter
359 type Scope_Rec is record
363 -- Type used to relate an entity and a scope number
365 package Scopes is new GNAT.HTable.Simple_HTable
366 (Header_Num => Entity_Hashed_Range,
367 Element => Scope_Rec,
368 No_Element => (Num => No_Scope, Entity => Empty),
372 -- Package used to build a correspondance between entities and scope
373 -- numbers used in SPARK cross references.
375 Nrefs : Nat := Xrefs.Last;
376 -- Number of references in table. This value may get reset (reduced)
377 -- when we eliminate duplicate reference entries as well as references
378 -- not suitable for local cross-references.
380 Nrefs_Add : constant Nat := Drefs.Last;
381 -- Number of additional references which correspond to dereferences in
384 Rnums : array (0 .. Nrefs + Nrefs_Add) of Nat;
385 -- This array contains numbers of references in the Xrefs table. This
386 -- list is sorted in output order. The extra 0'th entry is convenient
387 -- for the call to sort. When we sort the table, we move the entries in
388 -- Rnums around, but we do not move the original table entries.
390 ---------------------
391 -- Entity_Of_Scope --
392 ---------------------
394 function Entity_Of_Scope (S : Scope_Index) return Entity_Id is
396 return SPARK_Scope_Table.Table (S).Scope_Entity;
399 ---------------------
400 -- Get_Entity_Type --
401 ---------------------
403 function Get_Entity_Type (E : Entity_Id) return Character is
406 when E_Out_Parameter => return '<';
407 when E_In_Out_Parameter => return '=';
408 when E_In_Parameter => return '>';
409 when others => return '*';
417 function Get_Scope_Num (N : Entity_Id) return Nat is
419 return Scopes.Get (N).Num;
422 ------------------------
423 -- Is_SPARK_Reference --
424 ------------------------
426 function Is_SPARK_Reference
428 Typ : Character) return Boolean
431 -- The only references of interest on callable entities are calls. On
432 -- non-callable entities, the only references of interest are reads
435 if Ekind (E) in Overloadable_Kind then
438 -- Objects of Task type or protected type are not SPARK references
440 elsif Present (Etype (E))
441 and then Ekind (Etype (E)) in Concurrent_Kind
445 -- In all other cases, result is true for reference/modify cases,
446 -- and false for all other cases.
449 return Typ = 'r
' or else Typ = 'm
';
451 end Is_SPARK_Reference;
457 function Is_SPARK_Scope (E : Entity_Id) return Boolean is
460 and then not Is_Generic_Unit (E)
461 and then Renamed_Entity (E) = Empty
462 and then Get_Scope_Num (E) /= No_Scope;
465 ----------------------------
466 -- Is_Future_Scope_Entity --
467 ----------------------------
469 function Is_Future_Scope_Entity
471 S : Scope_Index) return Boolean
473 function Is_Past_Scope_Entity return Boolean;
474 -- Check whether entity E is in SPARK_Scope_Table at index strictly
477 --------------------------
478 -- Is_Past_Scope_Entity --
479 --------------------------
481 function Is_Past_Scope_Entity return Boolean is
483 for Index in SPARK_Scope_Table.First .. S - 1 loop
484 if SPARK_Scope_Table.Table (Index).Scope_Entity = E then
486 Dummy : constant SPARK_Scope_Record :=
487 SPARK_Scope_Table.Table (Index);
495 end Is_Past_Scope_Entity;
497 -- Start of processing for Is_Future_Scope_Entity
500 for Index in S .. SPARK_Scope_Table.Last loop
501 if SPARK_Scope_Table.Table (Index).Scope_Entity = E then
506 -- If this assertion fails, this means that the scope which we are
507 -- looking for has been treated already, which reveals a problem in
508 -- the order of cross-references.
510 pragma Assert (not Is_Past_Scope_Entity);
513 end Is_Future_Scope_Entity;
519 function Lt (Op1, Op2 : Natural) return Boolean is
520 T1 : constant Xref_Entry := Xrefs.Table (Rnums (Nat (Op1)));
521 T2 : constant Xref_Entry := Xrefs.Table (Rnums (Nat (Op2)));
524 -- First test: if entity is in different unit, sort by unit. Note:
525 -- that we use Ent_Scope_File rather than Eun, as Eun may refer to
526 -- the file where the generic scope is defined, which may differ from
527 -- the file where the enclosing scope is defined. It is the latter
528 -- which matters for a correct order here.
530 if T1.Ent_Scope_File /= T2.Ent_Scope_File then
531 return Dependency_Num (T1.Ent_Scope_File) <
532 Dependency_Num (T2.Ent_Scope_File);
534 -- Second test: within same unit, sort by location of the scope of
535 -- the entity definition.
537 elsif Get_Scope_Num (T1.Key.Ent_Scope) /=
538 Get_Scope_Num (T2.Key.Ent_Scope)
540 return Get_Scope_Num (T1.Key.Ent_Scope) <
541 Get_Scope_Num (T2.Key.Ent_Scope);
543 -- Third test: within same unit and scope, sort by location of
544 -- entity definition.
546 elsif T1.Def /= T2.Def then
547 return T1.Def < T2.Def;
550 -- Both entities must be equal at this point
552 pragma Assert (T1.Key.Ent = T2.Key.Ent);
554 -- Fourth test: if reference is in same unit as entity definition,
557 if T1.Key.Lun /= T2.Key.Lun
558 and then T1.Ent_Scope_File = T1.Key.Lun
562 elsif T1.Key.Lun /= T2.Key.Lun
563 and then T2.Ent_Scope_File = T2.Key.Lun
567 -- Fifth test: if reference is in same unit and same scope as
568 -- entity definition, sort first.
570 elsif T1.Ent_Scope_File = T1.Key.Lun
571 and then T1.Key.Ref_Scope /= T2.Key.Ref_Scope
572 and then T1.Key.Ent_Scope = T1.Key.Ref_Scope
576 elsif T2.Ent_Scope_File = T2.Key.Lun
577 and then T1.Key.Ref_Scope /= T2.Key.Ref_Scope
578 and then T2.Key.Ent_Scope = T2.Key.Ref_Scope
582 -- Sixth test: for same entity, sort by reference location unit
584 elsif T1.Key.Lun /= T2.Key.Lun then
585 return Dependency_Num (T1.Key.Lun) <
586 Dependency_Num (T2.Key.Lun);
588 -- Seventh test: for same entity, sort by reference location scope
590 elsif Get_Scope_Num (T1.Key.Ref_Scope) /=
591 Get_Scope_Num (T2.Key.Ref_Scope)
593 return Get_Scope_Num (T1.Key.Ref_Scope) <
594 Get_Scope_Num (T2.Key.Ref_Scope);
596 -- Eighth test: order of location within referencing unit
598 elsif T1.Key.Loc /= T2.Key.Loc then
599 return T1.Key.Loc < T2.Key.Loc;
601 -- Finally, for two locations at the same address prefer the one
602 -- that does NOT have the type 'r
', so that a modification or
603 -- extension takes preference, when there are more than one
604 -- reference at the same location. As a result, in the case of
605 -- entities that are in-out actuals, the read reference follows
606 -- the modify reference.
609 return T2.Key.Typ = 'r
';
618 procedure Move (From : Natural; To : Natural) is
620 Rnums (Nat (To)) := Rnums (Nat (From));
627 procedure Set_Scope_Num (N : Entity_Id; Num : Nat) is
629 Scopes.Set (K => N, E => Scope_Rec'(Num
=> Num
, Entity
=> N
));
632 ------------------------
633 -- Update_Scope_Range --
634 ------------------------
636 procedure Update_Scope_Range
642 SPARK_Scope_Table
.Table
(S
).From_Xref
:= From
;
643 SPARK_Scope_Table
.Table
(S
).To_Xref
:= To
;
644 end Update_Scope_Range
;
649 From_Index
: Xref_Index
;
652 Prev_Typ
: Character;
655 Ref_Name
: String_Ptr
;
656 Scope_Id
: Scope_Index
;
658 -- Start of processing for Add_SPARK_Xrefs
661 for Index
in SPARK_Scope_Table
.First
.. SPARK_Scope_Table
.Last
loop
663 S
: SPARK_Scope_Record
renames SPARK_Scope_Table
.Table
(Index
);
665 Set_Scope_Num
(S
.Scope_Entity
, S
.Scope_Num
);
669 -- Set up the pointer vector for the sort
671 for Index
in 1 .. Nrefs
loop
672 Rnums
(Index
) := Index
;
675 for Index
in Drefs
.First
.. Drefs
.Last
loop
676 Xrefs
.Append
(Drefs
.Table
(Index
));
679 Rnums
(Nrefs
) := Xrefs
.Last
;
682 -- Capture the definition Sloc values. As in the case of normal cross
683 -- references, we have to wait until now to get the correct value.
685 for Index
in 1 .. Nrefs
loop
686 Xrefs
.Table
(Index
).Def
:= Sloc
(Xrefs
.Table
(Index
).Key
.Ent
);
689 -- Eliminate entries not appropriate for SPARK. Done prior to sorting
690 -- cross-references, as it discards useless references which do not have
691 -- a proper format for the comparison function (like no location).
696 for Index
in 1 .. Ref_Count
loop
698 Ref
: Xref_Key
renames Xrefs
.Table
(Rnums
(Index
)).Key
;
701 if SPARK_Entities
(Ekind
(Ref
.Ent
))
702 and then SPARK_References
(Ref
.Typ
)
703 and then Is_SPARK_Scope
(Ref
.Ent_Scope
)
704 and then Is_SPARK_Scope
(Ref
.Ref_Scope
)
705 and then Is_SPARK_Reference
(Ref
.Ent
, Ref
.Typ
)
707 -- Discard references from unknown scopes, e.g. generic scopes
709 and then Get_Scope_Num
(Ref
.Ent_Scope
) /= No_Scope
710 and then Get_Scope_Num
(Ref
.Ref_Scope
) /= No_Scope
713 Rnums
(Nrefs
) := Rnums
(Index
);
718 -- Sort the references
720 Sorting
.Sort
(Integer (Nrefs
));
722 -- Eliminate duplicate entries
724 -- We need this test for Ref_Count because if we force ALI file
725 -- generation in case of errors detected, it may be the case that
726 -- Nrefs is 0, so we should not reset it here.
732 for Index
in 2 .. Ref_Count
loop
733 if Xrefs
.Table
(Rnums
(Index
)) /=
734 Xrefs
.Table
(Rnums
(Nrefs
))
737 Rnums
(Nrefs
) := Rnums
(Index
);
742 -- Eliminate the reference if it is at the same location as the previous
743 -- one, unless it is a read-reference indicating that the entity is an
744 -- in-out actual in a call.
751 for Index
in 1 .. Ref_Count
loop
753 Ref
: Xref_Key
renames Xrefs
.Table
(Rnums
(Index
)).Key
;
757 or else (Prev_Typ
= 'm' and then Ref
.Typ
= 'r')
762 Rnums
(Nrefs
) := Rnums
(Index
);
767 -- The two steps have eliminated all references, nothing to do
769 if SPARK_Scope_Table
.Last
= 0 then
777 -- Loop to output references
779 for Refno
in 1 .. Nrefs
loop
781 Ref_Entry
: Xref_Entry
renames Xrefs
.Table
(Rnums
(Refno
));
782 Ref
: Xref_Key
renames Ref_Entry
.Key
;
786 -- If this assertion fails, the scope which we are looking for is
787 -- not in SPARK scope table, which reveals either a problem in the
788 -- construction of the scope table, or an erroneous scope for the
789 -- current cross-reference.
791 pragma Assert
(Is_Future_Scope_Entity
(Ref
.Ent_Scope
, Scope_Id
));
793 -- Update the range of cross references to which the current scope
794 -- refers to. This may be the empty range only for the first scope
797 if Ref
.Ent_Scope
/= Entity_Of_Scope
(Scope_Id
) then
801 To
=> SPARK_Xref_Table
.Last
);
803 From_Index
:= SPARK_Xref_Table
.Last
+ 1;
806 while Ref
.Ent_Scope
/= Entity_Of_Scope
(Scope_Id
) loop
807 Scope_Id
:= Scope_Id
+ 1;
808 pragma Assert
(Scope_Id
<= SPARK_Scope_Table
.Last
);
811 if Ref
.Ent
/= Ref_Id
then
812 Ref_Name
:= new String'(Unique_Name (Ref.Ent));
815 if Ref.Ent = Heap then
819 Line := Int (Get_Logical_Line_Number (Ref_Entry.Def));
820 Col := Int (Get_Column_Number (Ref_Entry.Def));
823 -- References to constant objects are considered specially in
824 -- SPARK section, because these will be translated as constants in
825 -- the intermediate language for formal verification, and should
826 -- therefore never appear in frame conditions.
828 if Is_Constant_Object (Ref.Ent) then
834 SPARK_Xref_Table.Append (
835 (Entity_Name => Ref_Name,
837 Etype => Get_Entity_Type (Ref.Ent),
839 File_Num => Dependency_Num (Ref.Lun),
840 Scope_Num => Get_Scope_Num (Ref.Ref_Scope),
841 Line => Int (Get_Logical_Line_Number (Ref.Loc)),
843 Col => Int (Get_Column_Number (Ref.Loc))));
847 -- Update the range of cross references to which the scope refers to
852 To => SPARK_Xref_Table.Last);
855 -------------------------
856 -- Collect_SPARK_Xrefs --
857 -------------------------
859 procedure Collect_SPARK_Xrefs
860 (Sdep_Table : Unit_Ref_Table;
867 -- Cross-references should have been computed first
869 pragma Assert (Xrefs.Last /= 0);
871 Initialize_SPARK_Tables;
873 -- Generate file and scope SPARK cross-reference information
876 while D1 <= Num_Sdep loop
878 -- In rare cases, when treating the library-level instantiation of a
879 -- generic, two consecutive units refer to the same compilation unit
880 -- node and entity. In that case, treat them as a single unit for the
881 -- sake of SPARK cross references by passing to Add_SPARK_File.
884 and then Cunit_Entity (Sdep_Table (D1)) =
885 Cunit_Entity (Sdep_Table (D1 + 1))
893 (Ubody => Sdep_Table (D1),
894 Uspec => Sdep_Table (D2),
899 -- Fill in the spec information when relevant
902 package Entity_Hash_Table is new
903 GNAT.HTable.Simple_HTable
904 (Header_Num => Entity_Hashed_Range,
905 Element => Scope_Index,
912 -- Fill in the hash-table
914 for S in SPARK_Scope_Table.First .. SPARK_Scope_Table.Last loop
916 Srec : SPARK_Scope_Record renames SPARK_Scope_Table.Table (S);
918 Entity_Hash_Table.Set (Srec.Scope_Entity, S);
922 -- Use the hash-table to locate spec entities
924 for S in SPARK_Scope_Table.First .. SPARK_Scope_Table.Last loop
926 Srec : SPARK_Scope_Record renames SPARK_Scope_Table.Table (S);
928 Spec_Entity : constant Entity_Id :=
929 Unique_Entity (Srec.Scope_Entity);
930 Spec_Scope : constant Scope_Index :=
931 Entity_Hash_Table.Get (Spec_Entity);
934 -- Generic spec may be missing in which case Spec_Scope is zero
936 if Spec_Entity /= Srec.Scope_Entity
937 and then Spec_Scope /= 0
939 Srec.Spec_File_Num :=
940 SPARK_Scope_Table.Table (Spec_Scope).File_Num;
941 Srec.Spec_Scope_Num :=
942 SPARK_Scope_Table.Table (Spec_Scope).Scope_Num;
948 -- Generate SPARK cross-reference information
951 end Collect_SPARK_Xrefs;
953 --------------------------------
954 -- Detect_And_Add_SPARK_Scope --
955 --------------------------------
957 procedure Detect_And_Add_SPARK_Scope (N : Node_Id) is
959 if Nkind_In (N, N_Subprogram_Declaration,
961 N_Subprogram_Body_Stub,
962 N_Package_Declaration,
967 end Detect_And_Add_SPARK_Scope;
969 -------------------------------------
970 -- Enclosing_Subprogram_Or_Package --
971 -------------------------------------
973 function Enclosing_Subprogram_Or_Library_Package
974 (N : Node_Id) return Entity_Id
979 -- If N is the defining identifier for a subprogram, then return the
980 -- enclosing subprogram or package, not this subprogram.
982 if Nkind_In (N, N_Defining_Identifier, N_Defining_Operator_Symbol)
983 and then Nkind (Parent (N)) in N_Subprogram_Specification
985 Result := Parent (Parent (Parent (N)));
990 while Present (Result) loop
991 case Nkind (Result) is
992 when N_Package_Specification =>
994 -- Only return a library-level package
996 if Is_Library_Level_Entity (Defining_Entity (Result)) then
997 Result := Defining_Entity (Result);
1000 Result := Parent (Result);
1003 when N_Package_Body =>
1005 -- Only return a library-level package
1007 if Is_Library_Level_Entity (Defining_Entity (Result)) then
1008 Result := Defining_Entity (Result);
1011 Result := Parent (Result);
1014 when N_Subprogram_Specification =>
1015 Result := Defining_Unit_Name (Result);
1018 when N_Subprogram_Declaration =>
1019 Result := Defining_Unit_Name (Specification (Result));
1022 when N_Subprogram_Body =>
1023 Result := Defining_Unit_Name (Specification (Result));
1028 -- The enclosing subprogram for a precondition, postcondition,
1029 -- or contract case should be the declaration preceding the
1030 -- pragma (skipping any other pragmas between this pragma and
1031 -- this declaration.
1033 while Nkind (Result) = N_Pragma
1034 and then Is_List_Member (Result)
1035 and then Present (Prev (Result))
1037 Result := Prev (Result);
1040 if Nkind (Result) = N_Pragma then
1041 Result := Parent (Result);
1045 Result := Parent (Result);
1049 if Nkind (Result) = N_Defining_Program_Unit_Name then
1050 Result := Defining_Identifier (Result);
1053 -- Do not return a scope without a proper location
1056 and then Sloc (Result) = No_Location
1062 end Enclosing_Subprogram_Or_Library_Package;
1068 function Entity_Hash (E : Entity_Id) return Entity_Hashed_Range is
1071 Entity_Hashed_Range (E mod (Entity_Id (Entity_Hashed_Range'Last) + 1));
1074 --------------------------
1075 -- Generate_Dereference --
1076 --------------------------
1078 procedure Generate_Dereference
1080 Typ : Character := 'r
')
1082 procedure Create_Heap;
1083 -- Create and decorate the special entity which denotes the heap
1089 procedure Create_Heap is
1091 Name_Len := Name_Of_Heap_Variable'Length;
1092 Name_Buffer (1 .. Name_Len) := Name_Of_Heap_Variable;
1094 Heap := Make_Defining_Identifier (Standard_Location, Name_Enter);
1096 Set_Ekind (Heap, E_Variable);
1097 Set_Is_Internal (Heap, True);
1098 Set_Has_Fully_Qualified_Name (Heap);
1103 Loc : constant Source_Ptr := Sloc (N);
1105 Ref_Scope : Entity_Id;
1107 -- Start of processing for Generate_Dereference
1111 if Loc > No_Location then
1112 Drefs.Increment_Last;
1113 Index := Drefs.Last;
1116 Deref_Entry : Xref_Entry renames Drefs.Table (Index);
1117 Deref : Xref_Key renames Deref_Entry.Key;
1124 Ref_Scope := Enclosing_Subprogram_Or_Library_Package (N);
1130 -- It is as if the special "Heap" was defined in every scope where
1131 -- it is referenced.
1133 Deref.Eun := Get_Code_Unit (Loc);
1134 Deref.Lun := Get_Code_Unit (Loc);
1136 Deref.Ref_Scope := Ref_Scope;
1137 Deref.Ent_Scope := Ref_Scope;
1139 Deref_Entry.Def := No_Location;
1141 Deref_Entry.Ent_Scope_File := Get_Code_Unit (N);
1144 end Generate_Dereference;
1146 ------------------------------------
1147 -- Traverse_All_Compilation_Units --
1148 ------------------------------------
1150 procedure Traverse_All_Compilation_Units (Process : Node_Processing) is
1152 for U in Units.First .. Last_Unit loop
1153 Traverse_Compilation_Unit (Cunit (U), Process, Inside_Stubs => False);
1155 end Traverse_All_Compilation_Units;
1157 -------------------------------
1158 -- Traverse_Compilation_Unit --
1159 -------------------------------
1161 procedure Traverse_Compilation_Unit
1163 Process : Node_Processing;
1164 Inside_Stubs : Boolean)
1169 -- Get Unit (checking case of subunit)
1173 if Nkind (Lu) = N_Subunit then
1174 Lu := Proper_Body (Lu);
1177 -- Do not add scopes for generic units
1179 if Nkind (Lu) = N_Package_Body
1180 and then Ekind (Corresponding_Spec (Lu)) in Generic_Unit_Kind
1185 -- Call Process on all declarations
1187 if Nkind (Lu) in N_Declaration
1188 or else Nkind (Lu) in N_Later_Decl_Item
1193 -- Traverse the unit
1195 if Nkind (Lu) = N_Subprogram_Body then
1196 Traverse_Subprogram_Body (Lu, Process, Inside_Stubs);
1198 elsif Nkind (Lu) = N_Subprogram_Declaration then
1201 elsif Nkind (Lu) = N_Package_Declaration then
1202 Traverse_Package_Declaration (Lu, Process, Inside_Stubs);
1204 elsif Nkind (Lu) = N_Package_Body then
1205 Traverse_Package_Body (Lu, Process, Inside_Stubs);
1207 -- All other cases of compilation units (e.g. renamings), are not
1208 -- declarations, or else generic declarations which are ignored.
1213 end Traverse_Compilation_Unit;
1215 -----------------------------------------
1216 -- Traverse_Declarations_Or_Statements --
1217 -----------------------------------------
1219 procedure Traverse_Declarations_Or_Statements
1221 Process : Node_Processing;
1222 Inside_Stubs : Boolean)
1227 -- Loop through statements or declarations
1230 while Present (N) loop
1231 -- Call Process on all declarations
1233 if Nkind (N) in N_Declaration
1235 Nkind (N) in N_Later_Decl_Item
1242 -- Package declaration
1244 when N_Package_Declaration =>
1245 Traverse_Package_Declaration (N, Process, Inside_Stubs);
1249 when N_Package_Body =>
1250 if Ekind (Defining_Entity (N)) /= E_Generic_Package then
1251 Traverse_Package_Body (N, Process, Inside_Stubs);
1254 when N_Package_Body_Stub =>
1255 if Present (Library_Unit (N)) then
1257 Body_N : constant Node_Id := Get_Body_From_Stub (N);
1261 Ekind (Defining_Entity (Body_N)) /= E_Generic_Package
1263 Traverse_Package_Body (Body_N, Process, Inside_Stubs);
1268 -- Subprogram declaration
1270 when N_Subprogram_Declaration =>
1275 when N_Subprogram_Body =>
1276 if not Is_Generic_Subprogram (Defining_Entity (N)) then
1277 Traverse_Subprogram_Body (N, Process, Inside_Stubs);
1280 when N_Subprogram_Body_Stub =>
1281 if Present (Library_Unit (N)) then
1283 Body_N : constant Node_Id := Get_Body_From_Stub (N);
1287 not Is_Generic_Subprogram (Defining_Entity (Body_N))
1289 Traverse_Subprogram_Body
1290 (Body_N, Process, Inside_Stubs);
1297 when N_Block_Statement =>
1298 Traverse_Declarations_Or_Statements
1299 (Declarations (N), Process, Inside_Stubs);
1300 Traverse_Handled_Statement_Sequence
1301 (Handled_Statement_Sequence (N), Process, Inside_Stubs);
1303 when N_If_Statement =>
1305 -- Traverse the statements in the THEN part
1307 Traverse_Declarations_Or_Statements
1308 (Then_Statements (N), Process, Inside_Stubs);
1310 -- Loop through ELSIF parts if present
1312 if Present (Elsif_Parts (N)) then
1314 Elif : Node_Id := First (Elsif_Parts (N));
1317 while Present (Elif) loop
1318 Traverse_Declarations_Or_Statements
1319 (Then_Statements (Elif), Process, Inside_Stubs);
1325 -- Finally traverse the ELSE statements if present
1327 Traverse_Declarations_Or_Statements
1328 (Else_Statements (N), Process, Inside_Stubs);
1332 when N_Case_Statement =>
1334 -- Process case branches
1339 Alt := First (Alternatives (N));
1340 while Present (Alt) loop
1341 Traverse_Declarations_Or_Statements
1342 (Statements (Alt), Process, Inside_Stubs);
1347 -- Extended return statement
1349 when N_Extended_Return_Statement =>
1350 Traverse_Handled_Statement_Sequence
1351 (Handled_Statement_Sequence (N), Process, Inside_Stubs);
1355 when N_Loop_Statement =>
1356 Traverse_Declarations_Or_Statements
1357 (Statements (N), Process, Inside_Stubs);
1359 -- Generic declarations are ignored
1367 end Traverse_Declarations_Or_Statements;
1369 -----------------------------------------
1370 -- Traverse_Handled_Statement_Sequence --
1371 -----------------------------------------
1373 procedure Traverse_Handled_Statement_Sequence
1375 Process : Node_Processing;
1376 Inside_Stubs : Boolean)
1382 Traverse_Declarations_Or_Statements
1383 (Statements (N), Process, Inside_Stubs);
1385 if Present (Exception_Handlers (N)) then
1386 Handler := First (Exception_Handlers (N));
1387 while Present (Handler) loop
1388 Traverse_Declarations_Or_Statements
1389 (Statements (Handler), Process, Inside_Stubs);
1394 end Traverse_Handled_Statement_Sequence;
1396 ---------------------------
1397 -- Traverse_Package_Body --
1398 ---------------------------
1400 procedure Traverse_Package_Body
1402 Process : Node_Processing;
1403 Inside_Stubs : Boolean) is
1405 Traverse_Declarations_Or_Statements
1406 (Declarations (N), Process, Inside_Stubs);
1407 Traverse_Handled_Statement_Sequence
1408 (Handled_Statement_Sequence (N), Process, Inside_Stubs);
1409 end Traverse_Package_Body;
1411 ----------------------------------
1412 -- Traverse_Package_Declaration --
1413 ----------------------------------
1415 procedure Traverse_Package_Declaration
1417 Process : Node_Processing;
1418 Inside_Stubs : Boolean)
1420 Spec : constant Node_Id := Specification (N);
1422 Traverse_Declarations_Or_Statements
1423 (Visible_Declarations (Spec), Process, Inside_Stubs);
1424 Traverse_Declarations_Or_Statements
1425 (Private_Declarations (Spec), Process, Inside_Stubs);
1426 end Traverse_Package_Declaration;
1428 ------------------------------
1429 -- Traverse_Subprogram_Body --
1430 ------------------------------
1432 procedure Traverse_Subprogram_Body
1434 Process : Node_Processing;
1435 Inside_Stubs : Boolean)
1438 Traverse_Declarations_Or_Statements
1439 (Declarations (N), Process, Inside_Stubs);
1440 Traverse_Handled_Statement_Sequence
1441 (Handled_Statement_Sequence (N), Process, Inside_Stubs);
1442 end Traverse_Subprogram_Body;