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-2013, 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 SPARK_Xrefs
; use SPARK_Xrefs
;
27 with Einfo
; use Einfo
;
28 with Nmake
; use Nmake
;
34 package body SPARK_Specific
is
40 -- Table of SPARK_Entities, True for each entity kind used in SPARK
42 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
(Ubody
, Uspec
: 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 for
91 -- the same compilation unit, as it happens for library-level
92 -- instantiations of generics, then Ubody /= Uspec, and all scopes are
93 -- added to the same SPARK file. Otherwise Ubody = Uspec.
95 procedure Add_SPARK_Scope
(N
: Node_Id
);
96 -- Add scope N to the table SPARK_Scope_Table
98 procedure Add_SPARK_Xrefs
;
99 -- Filter table Xrefs to add all references used in SPARK to the table
102 procedure Detect_And_Add_SPARK_Scope
(N
: Node_Id
);
103 -- Call Add_SPARK_Scope on scopes
105 function Entity_Hash
(E
: Entity_Id
) return Entity_Hashed_Range
;
106 -- Hash function for hash table
108 procedure Traverse_Declarations_Or_Statements
110 Process
: Node_Processing
;
111 Inside_Stubs
: Boolean);
112 procedure Traverse_Handled_Statement_Sequence
114 Process
: Node_Processing
;
115 Inside_Stubs
: Boolean);
116 procedure Traverse_Package_Body
118 Process
: Node_Processing
;
119 Inside_Stubs
: Boolean);
120 procedure Traverse_Package_Declaration
122 Process
: Node_Processing
;
123 Inside_Stubs
: Boolean);
124 procedure Traverse_Subprogram_Body
126 Process
: Node_Processing
;
127 Inside_Stubs
: Boolean);
128 -- Traverse corresponding construct, calling Process on all declarations
134 procedure Add_SPARK_File
(Ubody
, Uspec
: Unit_Number_Type
; Dspec
: Nat
) is
135 File
: constant Source_File_Index
:= Source_Index
(Uspec
);
138 File_Name
: String_Ptr
;
139 Unit_File_Name
: String_Ptr
;
142 -- Source file could be inexistant as a result of an error, if option
145 if File
= No_Source_File
then
149 From
:= SPARK_Scope_Table
.Last
+ 1;
151 -- Unit might not have an associated compilation unit, as seen in code
152 -- filling Sdep_Table in Write_ALI.
154 if Present
(Cunit
(Ubody
)) then
155 Traverse_Compilation_Unit
156 (CU
=> Cunit
(Ubody
),
157 Process
=> Detect_And_Add_SPARK_Scope
'Access,
158 Inside_Stubs
=> False);
161 -- When two units are present for the same compilation unit, as it
162 -- happens for library-level instantiations of generics, then add all
163 -- scopes to the same SPARK file.
165 if Ubody
/= Uspec
then
166 if Present
(Cunit
(Uspec
)) then
167 Traverse_Compilation_Unit
168 (CU
=> Cunit
(Uspec
),
169 Process
=> Detect_And_Add_SPARK_Scope
'Access,
170 Inside_Stubs
=> False);
174 -- Update scope numbers
180 for Index
in From
.. SPARK_Scope_Table
.Last
loop
182 S
: SPARK_Scope_Record
renames SPARK_Scope_Table
.Table
(Index
);
184 S
.Scope_Num
:= Scope_Id
;
186 Scope_Id
:= Scope_Id
+ 1;
191 -- Remove those scopes previously marked for removal
194 Scope_Id
: Scope_Index
;
198 for Index
in From
.. SPARK_Scope_Table
.Last
loop
200 S
: SPARK_Scope_Record
renames SPARK_Scope_Table
.Table
(Index
);
202 if S
.Scope_Num
/= 0 then
203 SPARK_Scope_Table
.Table
(Scope_Id
) := S
;
204 Scope_Id
:= Scope_Id
+ 1;
209 SPARK_Scope_Table
.Set_Last
(Scope_Id
- 1);
212 -- Make entry for new file in file table
214 Get_Name_String
(Reference_Name
(File
));
215 File_Name
:= new String'(Name_Buffer (1 .. Name_Len));
217 -- For subunits, also retrieve the file name of the unit. Only do so if
218 -- unit has an associated compilation unit.
220 if Present (Cunit (Uspec))
221 and then Present (Cunit (Unit (File)))
222 and then Nkind (Unit (Cunit (Unit (File)))) = N_Subunit
224 Get_Name_String (Reference_Name (Main_Source_File));
225 Unit_File_Name := new String'(Name_Buffer
(1 .. Name_Len
));
228 SPARK_File_Table
.Append
(
229 (File_Name
=> File_Name
,
230 Unit_File_Name
=> Unit_File_Name
,
233 To_Scope
=> SPARK_Scope_Table
.Last
));
236 ---------------------
237 -- Add_SPARK_Scope --
238 ---------------------
240 procedure Add_SPARK_Scope
(N
: Node_Id
) is
241 E
: constant Entity_Id
:= Defining_Entity
(N
);
242 Loc
: constant Source_Ptr
:= Sloc
(E
);
246 -- Ignore scopes without a proper location
248 if Sloc
(N
) = No_Location
then
253 when E_Function | E_Generic_Function
=>
256 when E_Procedure | E_Generic_Procedure
=>
259 when E_Subprogram_Body
=>
266 if Nkind
(Spec
) = N_Defining_Program_Unit_Name
then
267 Spec
:= Parent
(Spec
);
270 if Nkind
(Spec
) = N_Function_Specification
then
274 (Nkind
(Spec
) = N_Procedure_Specification
);
279 when E_Package | E_Package_Body | E_Generic_Package
=>
283 -- Compilation of prj-attr.adb with -gnatn creates a node with
284 -- entity E_Void for the package defined at a-charac.ads16:13
294 -- File_Num and Scope_Num are filled later. From_Xref and To_Xref are
295 -- filled even later, but are initialized to represent an empty range.
297 SPARK_Scope_Table
.Append
(
298 (Scope_Name
=> new String'(Unique_Name (E)),
303 Line => Nat (Get_Logical_Line_Number (Loc)),
305 Col => Nat (Get_Column_Number (Loc)),
311 ---------------------
312 -- Add_SPARK_Xrefs --
313 ---------------------
315 procedure Add_SPARK_Xrefs is
316 function Entity_Of_Scope (S : Scope_Index) return Entity_Id;
317 -- Return the entity which maps to the input scope index
319 function Get_Entity_Type (E : Entity_Id) return Character;
320 -- Return a character representing the type of entity
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 an SPARK scope.
332 function Is_Future_Scope_Entity
334 S : Scope_Index) return Boolean;
335 -- Check whether entity E is in SPARK_Scope_Table at index S or higher
337 function Is_Global_Constant (E : Entity_Id) return Boolean;
338 -- Return True if E is a global constant for which we should ignore
341 function Lt (Op1 : Natural; Op2 : Natural) return Boolean;
342 -- Comparison function for Sort call
344 procedure Move (From : Natural; To : Natural);
345 -- Move procedure for Sort call
347 procedure Update_Scope_Range
351 -- Update the scope which maps to S with the new range From .. To
353 package Sorting is new GNAT.Heap_Sort_G (Move, Lt);
355 function Get_Scope_Num (N : Entity_Id) return Nat;
356 -- Return the scope number associated to entity N
358 procedure Set_Scope_Num (N : Entity_Id; Num : Nat);
359 -- Associate entity N to scope number Num
361 No_Scope : constant Nat := 0;
362 -- Initial scope counter
364 type Scope_Rec is record
368 -- Type used to relate an entity and a scope number
370 package Scopes is new GNAT.HTable.Simple_HTable
371 (Header_Num => Entity_Hashed_Range,
372 Element => Scope_Rec,
373 No_Element => (Num => No_Scope, Entity => Empty),
377 -- Package used to build a correspondance between entities and scope
378 -- numbers used in SPARK cross references.
380 Nrefs : Nat := Xrefs.Last;
381 -- Number of references in table. This value may get reset (reduced)
382 -- when we eliminate duplicate reference entries as well as references
383 -- not suitable for local cross-references.
385 Nrefs_Add : constant Nat := Drefs.Last;
386 -- Number of additional references which correspond to dereferences in
389 Rnums : array (0 .. Nrefs + Nrefs_Add) of Nat;
390 -- This array contains numbers of references in the Xrefs table. This
391 -- list is sorted in output order. The extra 0'th entry is convenient
392 -- for the call to sort. When we sort the table, we move the entries in
393 -- Rnums around, but we do not move the original table entries.
395 ---------------------
396 -- Entity_Of_Scope --
397 ---------------------
399 function Entity_Of_Scope (S : Scope_Index) return Entity_Id is
401 return SPARK_Scope_Table.Table (S).Scope_Entity;
404 ---------------------
405 -- Get_Entity_Type --
406 ---------------------
408 function Get_Entity_Type (E : Entity_Id) return Character is
411 when E_Out_Parameter => return '<';
412 when E_In_Out_Parameter => return '=';
413 when E_In_Parameter => return '>';
414 when others => return '*';
422 function Get_Scope_Num (N : Entity_Id) return Nat is
424 return Scopes.Get (N).Num;
427 ------------------------
428 -- Is_SPARK_Reference --
429 ------------------------
431 function Is_SPARK_Reference
433 Typ : Character) return Boolean
436 -- The only references of interest on callable entities are calls. On
437 -- non-callable entities, the only references of interest are reads
440 if Ekind (E) in Overloadable_Kind then
443 -- References to constant objects are not considered in SPARK
444 -- section, as these will be translated as constants in the
445 -- intermediate language for formal verification, and should
446 -- therefore never appear in frame conditions.
448 elsif Is_Constant_Object (E) then
451 -- Objects of Task type or protected type are not SPARK references
453 elsif Present (Etype (E))
454 and then Ekind (Etype (E)) in Concurrent_Kind
458 -- In all other cases, result is true for reference/modify cases,
459 -- and false for all other cases.
462 return Typ = 'r
' or else Typ = 'm
';
464 end Is_SPARK_Reference;
470 function Is_SPARK_Scope (E : Entity_Id) return Boolean is
473 and then not Is_Generic_Unit (E)
474 and then Renamed_Entity (E) = Empty
475 and then Get_Scope_Num (E) /= No_Scope;
478 ----------------------------
479 -- Is_Future_Scope_Entity --
480 ----------------------------
482 function Is_Future_Scope_Entity
484 S : Scope_Index) return Boolean
486 function Is_Past_Scope_Entity return Boolean;
487 -- Check whether entity E is in SPARK_Scope_Table at index strictly
490 --------------------------
491 -- Is_Past_Scope_Entity --
492 --------------------------
494 function Is_Past_Scope_Entity return Boolean is
496 for Index in SPARK_Scope_Table.First .. S - 1 loop
497 if SPARK_Scope_Table.Table (Index).Scope_Entity = E then
499 Dummy : constant SPARK_Scope_Record :=
500 SPARK_Scope_Table.Table (Index);
501 pragma Unreferenced (Dummy);
509 end Is_Past_Scope_Entity;
511 -- Start of processing for Is_Future_Scope_Entity
514 for Index in S .. SPARK_Scope_Table.Last loop
515 if SPARK_Scope_Table.Table (Index).Scope_Entity = E then
520 -- If this assertion fails, this means that the scope which we are
521 -- looking for has been treated already, which reveals a problem in
522 -- the order of cross-references.
524 pragma Assert (not Is_Past_Scope_Entity);
527 end Is_Future_Scope_Entity;
529 ------------------------
530 -- Is_Global_Constant --
531 ------------------------
533 function Is_Global_Constant (E : Entity_Id) return Boolean is
535 return Ekind (E) = E_Constant
536 and then Ekind_In (Scope (E), E_Package, E_Package_Body);
537 end Is_Global_Constant;
543 function Lt (Op1, Op2 : Natural) return Boolean is
544 T1 : constant Xref_Entry := Xrefs.Table (Rnums (Nat (Op1)));
545 T2 : constant Xref_Entry := Xrefs.Table (Rnums (Nat (Op2)));
548 -- First test: if entity is in different unit, sort by unit. Note:
549 -- that we use Ent_Scope_File rather than Eun, as Eun may refer to
550 -- the file where the generic scope is defined, which may differ from
551 -- the file where the enclosing scope is defined. It is the latter
552 -- which matters for a correct order here.
554 if T1.Ent_Scope_File /= T2.Ent_Scope_File then
555 return Dependency_Num (T1.Ent_Scope_File) <
556 Dependency_Num (T2.Ent_Scope_File);
558 -- Second test: within same unit, sort by location of the scope of
559 -- the entity definition.
561 elsif Get_Scope_Num (T1.Key.Ent_Scope) /=
562 Get_Scope_Num (T2.Key.Ent_Scope)
564 return Get_Scope_Num (T1.Key.Ent_Scope) <
565 Get_Scope_Num (T2.Key.Ent_Scope);
567 -- Third test: within same unit and scope, sort by location of
568 -- entity definition.
570 elsif T1.Def /= T2.Def then
571 return T1.Def < T2.Def;
574 -- Both entities must be equal at this point
576 pragma Assert (T1.Key.Ent = T2.Key.Ent);
578 -- Fourth test: if reference is in same unit as entity definition,
581 if T1.Key.Lun /= T2.Key.Lun
582 and then T1.Ent_Scope_File = T1.Key.Lun
586 elsif T1.Key.Lun /= T2.Key.Lun
587 and then T2.Ent_Scope_File = T2.Key.Lun
591 -- Fifth test: if reference is in same unit and same scope as
592 -- entity definition, sort first.
594 elsif T1.Ent_Scope_File = T1.Key.Lun
595 and then T1.Key.Ref_Scope /= T2.Key.Ref_Scope
596 and then T1.Key.Ent_Scope = T1.Key.Ref_Scope
600 elsif T2.Ent_Scope_File = T2.Key.Lun
601 and then T1.Key.Ref_Scope /= T2.Key.Ref_Scope
602 and then T2.Key.Ent_Scope = T2.Key.Ref_Scope
606 -- Sixth test: for same entity, sort by reference location unit
608 elsif T1.Key.Lun /= T2.Key.Lun then
609 return Dependency_Num (T1.Key.Lun) <
610 Dependency_Num (T2.Key.Lun);
612 -- Seventh test: for same entity, sort by reference location scope
614 elsif Get_Scope_Num (T1.Key.Ref_Scope) /=
615 Get_Scope_Num (T2.Key.Ref_Scope)
617 return Get_Scope_Num (T1.Key.Ref_Scope) <
618 Get_Scope_Num (T2.Key.Ref_Scope);
620 -- Eighth test: order of location within referencing unit
622 elsif T1.Key.Loc /= T2.Key.Loc then
623 return T1.Key.Loc < T2.Key.Loc;
625 -- Finally, for two locations at the same address prefer the one
626 -- that does NOT have the type 'r
', so that a modification or
627 -- extension takes preference, when there are more than one
628 -- reference at the same location. As a result, in the case of
629 -- entities that are in-out actuals, the read reference follows
630 -- the modify reference.
633 return T2.Key.Typ = 'r
';
642 procedure Move (From : Natural; To : Natural) is
644 Rnums (Nat (To)) := Rnums (Nat (From));
651 procedure Set_Scope_Num (N : Entity_Id; Num : Nat) is
653 Scopes.Set (K => N, E => Scope_Rec'(Num
=> Num
, Entity
=> N
));
656 ------------------------
657 -- Update_Scope_Range --
658 ------------------------
660 procedure Update_Scope_Range
666 SPARK_Scope_Table
.Table
(S
).From_Xref
:= From
;
667 SPARK_Scope_Table
.Table
(S
).To_Xref
:= To
;
668 end Update_Scope_Range
;
673 From_Index
: Xref_Index
;
676 Prev_Typ
: Character;
679 Ref_Name
: String_Ptr
;
680 Scope_Id
: Scope_Index
;
682 -- Start of processing for Add_SPARK_Xrefs
685 for Index
in SPARK_Scope_Table
.First
.. SPARK_Scope_Table
.Last
loop
687 S
: SPARK_Scope_Record
renames SPARK_Scope_Table
.Table
(Index
);
689 Set_Scope_Num
(S
.Scope_Entity
, S
.Scope_Num
);
693 -- Set up the pointer vector for the sort
695 for Index
in 1 .. Nrefs
loop
696 Rnums
(Index
) := Index
;
699 for Index
in Drefs
.First
.. Drefs
.Last
loop
700 Xrefs
.Append
(Drefs
.Table
(Index
));
703 Rnums
(Nrefs
) := Xrefs
.Last
;
706 -- Capture the definition Sloc values. As in the case of normal cross
707 -- references, we have to wait until now to get the correct value.
709 for Index
in 1 .. Nrefs
loop
710 Xrefs
.Table
(Index
).Def
:= Sloc
(Xrefs
.Table
(Index
).Key
.Ent
);
713 -- Eliminate entries not appropriate for SPARK. Done prior to sorting
714 -- cross-references, as it discards useless references which do not have
715 -- a proper format for the comparison function (like no location).
720 for Index
in 1 .. Ref_Count
loop
722 Ref
: Xref_Key
renames Xrefs
.Table
(Rnums
(Index
)).Key
;
725 if SPARK_Entities
(Ekind
(Ref
.Ent
))
726 and then SPARK_References
(Ref
.Typ
)
727 and then Is_SPARK_Scope
(Ref
.Ent_Scope
)
728 and then Is_SPARK_Scope
(Ref
.Ref_Scope
)
729 and then not Is_Global_Constant
(Ref
.Ent
)
730 and then Is_SPARK_Reference
(Ref
.Ent
, Ref
.Typ
)
732 -- Discard references from unknown scopes, e.g. generic scopes
734 and then Get_Scope_Num
(Ref
.Ent_Scope
) /= No_Scope
735 and then Get_Scope_Num
(Ref
.Ref_Scope
) /= No_Scope
738 Rnums
(Nrefs
) := Rnums
(Index
);
743 -- Sort the references
745 Sorting
.Sort
(Integer (Nrefs
));
747 -- Eliminate duplicate entries
749 -- We need this test for Ref_Count because if we force ALI file
750 -- generation in case of errors detected, it may be the case that
751 -- Nrefs is 0, so we should not reset it here.
757 for Index
in 2 .. Ref_Count
loop
758 if Xrefs
.Table
(Rnums
(Index
)) /=
759 Xrefs
.Table
(Rnums
(Nrefs
))
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.
776 for Index
in 1 .. Ref_Count
loop
778 Ref
: Xref_Key
renames Xrefs
.Table
(Rnums
(Index
)).Key
;
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
;
810 -- If this assertion fails, the scope which we are looking for is
811 -- not in SPARK scope table, which reveals either a problem in the
812 -- construction of the scope table, or an erroneous scope for the
813 -- current cross-reference.
815 pragma Assert
(Is_Future_Scope_Entity
(Ref
.Ent_Scope
, Scope_Id
));
817 -- Update the range of cross references to which the current scope
818 -- refers to. This may be the empty range only for the first scope
821 if Ref
.Ent_Scope
/= Entity_Of_Scope
(Scope_Id
) then
825 To
=> SPARK_Xref_Table
.Last
);
827 From_Index
:= SPARK_Xref_Table
.Last
+ 1;
830 while Ref
.Ent_Scope
/= Entity_Of_Scope
(Scope_Id
) loop
831 Scope_Id
:= Scope_Id
+ 1;
832 pragma Assert
(Scope_Id
<= SPARK_Scope_Table
.Last
);
835 if Ref
.Ent
/= Ref_Id
then
836 Ref_Name
:= new String'(Unique_Name (Ref.Ent));
839 if Ref.Ent = Heap then
843 Line := Int (Get_Logical_Line_Number (Ref_Entry.Def));
844 Col := Int (Get_Column_Number (Ref_Entry.Def));
847 SPARK_Xref_Table.Append (
848 (Entity_Name => Ref_Name,
850 Etype => Get_Entity_Type (Ref.Ent),
852 File_Num => Dependency_Num (Ref.Lun),
853 Scope_Num => Get_Scope_Num (Ref.Ref_Scope),
854 Line => Int (Get_Logical_Line_Number (Ref.Loc)),
856 Col => Int (Get_Column_Number (Ref.Loc))));
860 -- Update the range of cross references to which the scope refers to
865 To => SPARK_Xref_Table.Last);
868 -------------------------
869 -- Collect_SPARK_Xrefs --
870 -------------------------
872 procedure Collect_SPARK_Xrefs
873 (Sdep_Table : Unit_Ref_Table;
880 -- Cross-references should have been computed first
882 pragma Assert (Xrefs.Last /= 0);
884 Initialize_SPARK_Tables;
886 -- Generate file and scope SPARK cross-reference information
889 while D1 <= Num_Sdep loop
891 -- In rare cases, when treating the library-level instantiation of a
892 -- generic, two consecutive units refer to the same compilation unit
893 -- node and entity. In that case, treat them as a single unit for the
894 -- sake of SPARK cross references by passing to Add_SPARK_File.
897 and then Cunit_Entity (Sdep_Table (D1)) =
898 Cunit_Entity (Sdep_Table (D1 + 1))
906 (Ubody => Sdep_Table (D1),
907 Uspec => Sdep_Table (D2),
912 -- Fill in the spec information when relevant
915 package Entity_Hash_Table is new
916 GNAT.HTable.Simple_HTable
917 (Header_Num => Entity_Hashed_Range,
918 Element => Scope_Index,
925 -- Fill in the hash-table
927 for S in SPARK_Scope_Table.First .. SPARK_Scope_Table.Last loop
929 Srec : SPARK_Scope_Record renames SPARK_Scope_Table.Table (S);
931 Entity_Hash_Table.Set (Srec.Scope_Entity, S);
935 -- Use the hash-table to locate spec entities
937 for S in SPARK_Scope_Table.First .. SPARK_Scope_Table.Last loop
939 Srec : SPARK_Scope_Record renames SPARK_Scope_Table.Table (S);
941 Spec_Entity : constant Entity_Id :=
942 Unique_Entity (Srec.Scope_Entity);
943 Spec_Scope : constant Scope_Index :=
944 Entity_Hash_Table.Get (Spec_Entity);
947 -- Generic spec may be missing in which case Spec_Scope is zero
949 if Spec_Entity /= Srec.Scope_Entity
950 and then Spec_Scope /= 0
952 Srec.Spec_File_Num :=
953 SPARK_Scope_Table.Table (Spec_Scope).File_Num;
954 Srec.Spec_Scope_Num :=
955 SPARK_Scope_Table.Table (Spec_Scope).Scope_Num;
961 -- Generate SPARK cross-reference information
964 end Collect_SPARK_Xrefs;
966 --------------------------------
967 -- Detect_And_Add_SPARK_Scope --
968 --------------------------------
970 procedure Detect_And_Add_SPARK_Scope (N : Node_Id) is
972 if Nkind_In (N, N_Subprogram_Declaration,
974 N_Subprogram_Body_Stub,
975 N_Package_Declaration,
980 end Detect_And_Add_SPARK_Scope;
982 -------------------------------------
983 -- Enclosing_Subprogram_Or_Package --
984 -------------------------------------
986 function Enclosing_Subprogram_Or_Package (N : Node_Id) return Entity_Id is
990 -- If N is the defining identifier for a subprogram, then return the
991 -- enclosing subprogram or package, not this subprogram.
993 if Nkind_In (N, N_Defining_Identifier, N_Defining_Operator_Symbol)
994 and then Nkind (Parent (N)) in N_Subprogram_Specification
996 Result := Parent (Parent (Parent (N)));
1001 while Present (Result) loop
1002 case Nkind (Result) is
1003 when N_Package_Specification =>
1004 Result := Defining_Unit_Name (Result);
1007 when N_Package_Body =>
1008 Result := Defining_Unit_Name (Result);
1011 when N_Subprogram_Specification =>
1012 Result := Defining_Unit_Name (Result);
1015 when N_Subprogram_Declaration =>
1016 Result := Defining_Unit_Name (Specification (Result));
1019 when N_Subprogram_Body =>
1020 Result := Defining_Unit_Name (Specification (Result));
1023 -- The enclosing subprogram for a pre- or postconditions should be
1024 -- the subprogram to which the pragma is attached. This is not
1025 -- always the case in the AST, as the pragma may be declared after
1026 -- the declaration of the subprogram. Return Empty in this case.
1029 if Get_Pragma_Id (Result) = Pragma_Precondition
1031 Get_Pragma_Id (Result) = Pragma_Postcondition
1035 Result := Parent (Result);
1039 Result := Parent (Result);
1043 if Nkind (Result) = N_Defining_Program_Unit_Name then
1044 Result := Defining_Identifier (Result);
1047 -- Do not return a scope without a proper location
1050 and then Sloc (Result) = No_Location
1056 end Enclosing_Subprogram_Or_Package;
1062 function Entity_Hash (E : Entity_Id) return Entity_Hashed_Range is
1065 Entity_Hashed_Range (E mod (Entity_Id (Entity_Hashed_Range'Last) + 1));
1068 --------------------------
1069 -- Generate_Dereference --
1070 --------------------------
1072 procedure Generate_Dereference
1074 Typ : Character := 'r
')
1076 procedure Create_Heap;
1077 -- Create and decorate the special entity which denotes the heap
1083 procedure Create_Heap is
1085 Name_Len := Name_Of_Heap_Variable'Length;
1086 Name_Buffer (1 .. Name_Len) := Name_Of_Heap_Variable;
1088 Heap := Make_Defining_Identifier (Standard_Location, Name_Enter);
1090 Set_Ekind (Heap, E_Variable);
1091 Set_Is_Internal (Heap, True);
1092 Set_Has_Fully_Qualified_Name (Heap);
1097 Loc : constant Source_Ptr := Sloc (N);
1099 Ref_Scope : Entity_Id;
1101 -- Start of processing for Generate_Dereference
1105 if Loc > No_Location then
1106 Drefs.Increment_Last;
1107 Index := Drefs.Last;
1110 Deref_Entry : Xref_Entry renames Drefs.Table (Index);
1111 Deref : Xref_Key renames Deref_Entry.Key;
1118 Ref_Scope := Enclosing_Subprogram_Or_Package (N);
1124 -- It is as if the special "Heap" was defined in every scope where
1125 -- it is referenced.
1127 Deref.Eun := Get_Code_Unit (Loc);
1128 Deref.Lun := Get_Code_Unit (Loc);
1130 Deref.Ref_Scope := Ref_Scope;
1131 Deref.Ent_Scope := Ref_Scope;
1133 Deref_Entry.Def := No_Location;
1135 Deref_Entry.Ent_Scope_File := Get_Code_Unit (N);
1138 end Generate_Dereference;
1140 ------------------------------------
1141 -- Traverse_All_Compilation_Units --
1142 ------------------------------------
1144 procedure Traverse_All_Compilation_Units (Process : Node_Processing) is
1146 for U in Units.First .. Last_Unit loop
1147 Traverse_Compilation_Unit (Cunit (U), Process, Inside_Stubs => False);
1149 end Traverse_All_Compilation_Units;
1151 -------------------------------
1152 -- Traverse_Compilation_Unit --
1153 -------------------------------
1155 procedure Traverse_Compilation_Unit
1157 Process : Node_Processing;
1158 Inside_Stubs : Boolean)
1163 -- Get Unit (checking case of subunit)
1167 if Nkind (Lu) = N_Subunit then
1168 Lu := Proper_Body (Lu);
1171 -- Do not add scopes for generic units
1173 if Nkind (Lu) = N_Package_Body
1174 and then Ekind (Corresponding_Spec (Lu)) in Generic_Unit_Kind
1179 -- Call Process on all declarations
1181 if Nkind (Lu) in N_Declaration
1182 or else Nkind (Lu) in N_Later_Decl_Item
1187 -- Traverse the unit
1189 if Nkind (Lu) = N_Subprogram_Body then
1190 Traverse_Subprogram_Body (Lu, Process, Inside_Stubs);
1192 elsif Nkind (Lu) = N_Subprogram_Declaration then
1195 elsif Nkind (Lu) = N_Package_Declaration then
1196 Traverse_Package_Declaration (Lu, Process, Inside_Stubs);
1198 elsif Nkind (Lu) = N_Package_Body then
1199 Traverse_Package_Body (Lu, Process, Inside_Stubs);
1201 -- All other cases of compilation units (e.g. renamings), are not
1202 -- declarations, or else generic declarations which are ignored.
1207 end Traverse_Compilation_Unit;
1209 -----------------------------------------
1210 -- Traverse_Declarations_Or_Statements --
1211 -----------------------------------------
1213 procedure Traverse_Declarations_Or_Statements
1215 Process : Node_Processing;
1216 Inside_Stubs : Boolean)
1221 -- Loop through statements or declarations
1224 while Present (N) loop
1225 -- Call Process on all declarations
1227 if Nkind (N) in N_Declaration
1229 Nkind (N) in N_Later_Decl_Item
1236 -- Package declaration
1238 when N_Package_Declaration =>
1239 Traverse_Package_Declaration (N, Process, Inside_Stubs);
1243 when N_Package_Body =>
1244 if Ekind (Defining_Entity (N)) /= E_Generic_Package then
1245 Traverse_Package_Body (N, Process, Inside_Stubs);
1248 when N_Package_Body_Stub =>
1249 if Present (Library_Unit (N)) then
1251 Body_N : constant Node_Id := Get_Body_From_Stub (N);
1255 Ekind (Defining_Entity (Body_N)) /= E_Generic_Package
1257 Traverse_Package_Body (Body_N, Process, Inside_Stubs);
1262 -- Subprogram declaration
1264 when N_Subprogram_Declaration =>
1269 when N_Subprogram_Body =>
1270 if not Is_Generic_Subprogram (Defining_Entity (N)) then
1271 Traverse_Subprogram_Body (N, Process, Inside_Stubs);
1274 when N_Subprogram_Body_Stub =>
1275 if Present (Library_Unit (N)) then
1277 Body_N : constant Node_Id := Get_Body_From_Stub (N);
1281 not Is_Generic_Subprogram (Defining_Entity (Body_N))
1283 Traverse_Subprogram_Body
1284 (Body_N, Process, Inside_Stubs);
1291 when N_Block_Statement =>
1292 Traverse_Declarations_Or_Statements
1293 (Declarations (N), Process, Inside_Stubs);
1294 Traverse_Handled_Statement_Sequence
1295 (Handled_Statement_Sequence (N), Process, Inside_Stubs);
1297 when N_If_Statement =>
1299 -- Traverse the statements in the THEN part
1301 Traverse_Declarations_Or_Statements
1302 (Then_Statements (N), Process, Inside_Stubs);
1304 -- Loop through ELSIF parts if present
1306 if Present (Elsif_Parts (N)) then
1308 Elif : Node_Id := First (Elsif_Parts (N));
1311 while Present (Elif) loop
1312 Traverse_Declarations_Or_Statements
1313 (Then_Statements (Elif), Process, Inside_Stubs);
1319 -- Finally traverse the ELSE statements if present
1321 Traverse_Declarations_Or_Statements
1322 (Else_Statements (N), Process, Inside_Stubs);
1326 when N_Case_Statement =>
1328 -- Process case branches
1333 Alt := First (Alternatives (N));
1334 while Present (Alt) loop
1335 Traverse_Declarations_Or_Statements
1336 (Statements (Alt), Process, Inside_Stubs);
1341 -- Extended return statement
1343 when N_Extended_Return_Statement =>
1344 Traverse_Handled_Statement_Sequence
1345 (Handled_Statement_Sequence (N), Process, Inside_Stubs);
1349 when N_Loop_Statement =>
1350 Traverse_Declarations_Or_Statements
1351 (Statements (N), Process, Inside_Stubs);
1353 -- Generic declarations are ignored
1361 end Traverse_Declarations_Or_Statements;
1363 -----------------------------------------
1364 -- Traverse_Handled_Statement_Sequence --
1365 -----------------------------------------
1367 procedure Traverse_Handled_Statement_Sequence
1369 Process : Node_Processing;
1370 Inside_Stubs : Boolean)
1376 Traverse_Declarations_Or_Statements
1377 (Statements (N), Process, Inside_Stubs);
1379 if Present (Exception_Handlers (N)) then
1380 Handler := First (Exception_Handlers (N));
1381 while Present (Handler) loop
1382 Traverse_Declarations_Or_Statements
1383 (Statements (Handler), Process, Inside_Stubs);
1388 end Traverse_Handled_Statement_Sequence;
1390 ---------------------------
1391 -- Traverse_Package_Body --
1392 ---------------------------
1394 procedure Traverse_Package_Body
1396 Process : Node_Processing;
1397 Inside_Stubs : Boolean) is
1399 Traverse_Declarations_Or_Statements
1400 (Declarations (N), Process, Inside_Stubs);
1401 Traverse_Handled_Statement_Sequence
1402 (Handled_Statement_Sequence (N), Process, Inside_Stubs);
1403 end Traverse_Package_Body;
1405 ----------------------------------
1406 -- Traverse_Package_Declaration --
1407 ----------------------------------
1409 procedure Traverse_Package_Declaration
1411 Process : Node_Processing;
1412 Inside_Stubs : Boolean)
1414 Spec : constant Node_Id := Specification (N);
1416 Traverse_Declarations_Or_Statements
1417 (Visible_Declarations (Spec), Process, Inside_Stubs);
1418 Traverse_Declarations_Or_Statements
1419 (Private_Declarations (Spec), Process, Inside_Stubs);
1420 end Traverse_Package_Declaration;
1422 ------------------------------
1423 -- Traverse_Subprogram_Body --
1424 ------------------------------
1426 procedure Traverse_Subprogram_Body
1428 Process : Node_Processing;
1429 Inside_Stubs : Boolean)
1432 Traverse_Declarations_Or_Statements
1433 (Declarations (N), Process, Inside_Stubs);
1434 Traverse_Handled_Statement_Sequence
1435 (Handled_Statement_Sequence (N), Process, Inside_Stubs);
1436 end Traverse_Subprogram_Body;