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));
1025 -- The enclosing subprogram for a precondition, postcondition,
1026 -- or contract case should be the subprogram to which the
1027 -- pragma is attached, which can be found by following
1028 -- previous elements in the list to which the pragma belongs.
1030 if Get_Pragma_Id (Result) = Pragma_Precondition
1032 Get_Pragma_Id (Result) = Pragma_Postcondition
1034 Get_Pragma_Id (Result) = Pragma_Contract_Cases
1036 if Is_List_Member (Result)
1037 and then Present (Prev (Result))
1039 Result := Prev (Result);
1041 Result := Parent (Result);
1045 Result := Parent (Result);
1049 Result := Parent (Result);
1053 if Nkind (Result) = N_Defining_Program_Unit_Name then
1054 Result := Defining_Identifier (Result);
1057 -- Do not return a scope without a proper location
1060 and then Sloc (Result) = No_Location
1066 end Enclosing_Subprogram_Or_Package;
1072 function Entity_Hash (E : Entity_Id) return Entity_Hashed_Range is
1075 Entity_Hashed_Range (E mod (Entity_Id (Entity_Hashed_Range'Last) + 1));
1078 --------------------------
1079 -- Generate_Dereference --
1080 --------------------------
1082 procedure Generate_Dereference
1084 Typ : Character := 'r
')
1086 procedure Create_Heap;
1087 -- Create and decorate the special entity which denotes the heap
1093 procedure Create_Heap is
1095 Name_Len := Name_Of_Heap_Variable'Length;
1096 Name_Buffer (1 .. Name_Len) := Name_Of_Heap_Variable;
1098 Heap := Make_Defining_Identifier (Standard_Location, Name_Enter);
1100 Set_Ekind (Heap, E_Variable);
1101 Set_Is_Internal (Heap, True);
1102 Set_Has_Fully_Qualified_Name (Heap);
1107 Loc : constant Source_Ptr := Sloc (N);
1109 Ref_Scope : Entity_Id;
1111 -- Start of processing for Generate_Dereference
1115 if Loc > No_Location then
1116 Drefs.Increment_Last;
1117 Index := Drefs.Last;
1120 Deref_Entry : Xref_Entry renames Drefs.Table (Index);
1121 Deref : Xref_Key renames Deref_Entry.Key;
1128 Ref_Scope := Enclosing_Subprogram_Or_Package (N);
1134 -- It is as if the special "Heap" was defined in every scope where
1135 -- it is referenced.
1137 Deref.Eun := Get_Code_Unit (Loc);
1138 Deref.Lun := Get_Code_Unit (Loc);
1140 Deref.Ref_Scope := Ref_Scope;
1141 Deref.Ent_Scope := Ref_Scope;
1143 Deref_Entry.Def := No_Location;
1145 Deref_Entry.Ent_Scope_File := Get_Code_Unit (N);
1148 end Generate_Dereference;
1150 ------------------------------------
1151 -- Traverse_All_Compilation_Units --
1152 ------------------------------------
1154 procedure Traverse_All_Compilation_Units (Process : Node_Processing) is
1156 for U in Units.First .. Last_Unit loop
1157 Traverse_Compilation_Unit (Cunit (U), Process, Inside_Stubs => False);
1159 end Traverse_All_Compilation_Units;
1161 -------------------------------
1162 -- Traverse_Compilation_Unit --
1163 -------------------------------
1165 procedure Traverse_Compilation_Unit
1167 Process : Node_Processing;
1168 Inside_Stubs : Boolean)
1173 -- Get Unit (checking case of subunit)
1177 if Nkind (Lu) = N_Subunit then
1178 Lu := Proper_Body (Lu);
1181 -- Do not add scopes for generic units
1183 if Nkind (Lu) = N_Package_Body
1184 and then Ekind (Corresponding_Spec (Lu)) in Generic_Unit_Kind
1189 -- Call Process on all declarations
1191 if Nkind (Lu) in N_Declaration
1192 or else Nkind (Lu) in N_Later_Decl_Item
1197 -- Traverse the unit
1199 if Nkind (Lu) = N_Subprogram_Body then
1200 Traverse_Subprogram_Body (Lu, Process, Inside_Stubs);
1202 elsif Nkind (Lu) = N_Subprogram_Declaration then
1205 elsif Nkind (Lu) = N_Package_Declaration then
1206 Traverse_Package_Declaration (Lu, Process, Inside_Stubs);
1208 elsif Nkind (Lu) = N_Package_Body then
1209 Traverse_Package_Body (Lu, Process, Inside_Stubs);
1211 -- All other cases of compilation units (e.g. renamings), are not
1212 -- declarations, or else generic declarations which are ignored.
1217 end Traverse_Compilation_Unit;
1219 -----------------------------------------
1220 -- Traverse_Declarations_Or_Statements --
1221 -----------------------------------------
1223 procedure Traverse_Declarations_Or_Statements
1225 Process : Node_Processing;
1226 Inside_Stubs : Boolean)
1231 -- Loop through statements or declarations
1234 while Present (N) loop
1235 -- Call Process on all declarations
1237 if Nkind (N) in N_Declaration
1239 Nkind (N) in N_Later_Decl_Item
1246 -- Package declaration
1248 when N_Package_Declaration =>
1249 Traverse_Package_Declaration (N, Process, Inside_Stubs);
1253 when N_Package_Body =>
1254 if Ekind (Defining_Entity (N)) /= E_Generic_Package then
1255 Traverse_Package_Body (N, Process, Inside_Stubs);
1258 when N_Package_Body_Stub =>
1259 if Present (Library_Unit (N)) then
1261 Body_N : constant Node_Id := Get_Body_From_Stub (N);
1265 Ekind (Defining_Entity (Body_N)) /= E_Generic_Package
1267 Traverse_Package_Body (Body_N, Process, Inside_Stubs);
1272 -- Subprogram declaration
1274 when N_Subprogram_Declaration =>
1279 when N_Subprogram_Body =>
1280 if not Is_Generic_Subprogram (Defining_Entity (N)) then
1281 Traverse_Subprogram_Body (N, Process, Inside_Stubs);
1284 when N_Subprogram_Body_Stub =>
1285 if Present (Library_Unit (N)) then
1287 Body_N : constant Node_Id := Get_Body_From_Stub (N);
1291 not Is_Generic_Subprogram (Defining_Entity (Body_N))
1293 Traverse_Subprogram_Body
1294 (Body_N, Process, Inside_Stubs);
1301 when N_Block_Statement =>
1302 Traverse_Declarations_Or_Statements
1303 (Declarations (N), Process, Inside_Stubs);
1304 Traverse_Handled_Statement_Sequence
1305 (Handled_Statement_Sequence (N), Process, Inside_Stubs);
1307 when N_If_Statement =>
1309 -- Traverse the statements in the THEN part
1311 Traverse_Declarations_Or_Statements
1312 (Then_Statements (N), Process, Inside_Stubs);
1314 -- Loop through ELSIF parts if present
1316 if Present (Elsif_Parts (N)) then
1318 Elif : Node_Id := First (Elsif_Parts (N));
1321 while Present (Elif) loop
1322 Traverse_Declarations_Or_Statements
1323 (Then_Statements (Elif), Process, Inside_Stubs);
1329 -- Finally traverse the ELSE statements if present
1331 Traverse_Declarations_Or_Statements
1332 (Else_Statements (N), Process, Inside_Stubs);
1336 when N_Case_Statement =>
1338 -- Process case branches
1343 Alt := First (Alternatives (N));
1344 while Present (Alt) loop
1345 Traverse_Declarations_Or_Statements
1346 (Statements (Alt), Process, Inside_Stubs);
1351 -- Extended return statement
1353 when N_Extended_Return_Statement =>
1354 Traverse_Handled_Statement_Sequence
1355 (Handled_Statement_Sequence (N), Process, Inside_Stubs);
1359 when N_Loop_Statement =>
1360 Traverse_Declarations_Or_Statements
1361 (Statements (N), Process, Inside_Stubs);
1363 -- Generic declarations are ignored
1371 end Traverse_Declarations_Or_Statements;
1373 -----------------------------------------
1374 -- Traverse_Handled_Statement_Sequence --
1375 -----------------------------------------
1377 procedure Traverse_Handled_Statement_Sequence
1379 Process : Node_Processing;
1380 Inside_Stubs : Boolean)
1386 Traverse_Declarations_Or_Statements
1387 (Statements (N), Process, Inside_Stubs);
1389 if Present (Exception_Handlers (N)) then
1390 Handler := First (Exception_Handlers (N));
1391 while Present (Handler) loop
1392 Traverse_Declarations_Or_Statements
1393 (Statements (Handler), Process, Inside_Stubs);
1398 end Traverse_Handled_Statement_Sequence;
1400 ---------------------------
1401 -- Traverse_Package_Body --
1402 ---------------------------
1404 procedure Traverse_Package_Body
1406 Process : Node_Processing;
1407 Inside_Stubs : Boolean) is
1409 Traverse_Declarations_Or_Statements
1410 (Declarations (N), Process, Inside_Stubs);
1411 Traverse_Handled_Statement_Sequence
1412 (Handled_Statement_Sequence (N), Process, Inside_Stubs);
1413 end Traverse_Package_Body;
1415 ----------------------------------
1416 -- Traverse_Package_Declaration --
1417 ----------------------------------
1419 procedure Traverse_Package_Declaration
1421 Process : Node_Processing;
1422 Inside_Stubs : Boolean)
1424 Spec : constant Node_Id := Specification (N);
1426 Traverse_Declarations_Or_Statements
1427 (Visible_Declarations (Spec), Process, Inside_Stubs);
1428 Traverse_Declarations_Or_Statements
1429 (Private_Declarations (Spec), Process, Inside_Stubs);
1430 end Traverse_Package_Declaration;
1432 ------------------------------
1433 -- Traverse_Subprogram_Body --
1434 ------------------------------
1436 procedure Traverse_Subprogram_Body
1438 Process : Node_Processing;
1439 Inside_Stubs : Boolean)
1442 Traverse_Declarations_Or_Statements
1443 (Declarations (N), Process, Inside_Stubs);
1444 Traverse_Handled_Statement_Sequence
1445 (Handled_Statement_Sequence (N), Process, Inside_Stubs);
1446 end Traverse_Subprogram_Body;