| blob | dfbe4dd34190c7277e3fd08a473e515940c4a717 |
1 ------------------------------------------------------------------------------
2 -- --
3 -- GNAT COMPILER COMPONENTS --
4 -- --
5 -- L I B . X R E F . S P A R K _ S P E C I F I C --
6 -- --
7 -- B o d y --
8 -- --
9 -- Copyright (C) 2011-2016, Free Software Foundation, Inc. --
10 -- --
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. --
20 -- --
21 -- GNAT was originally developed by the GNAT team at New York University. --
22 -- Extensive contributions were provided by Ada Core Technologies Inc. --
23 -- --
24 ------------------------------------------------------------------------------
35 ---------------------
36 -- Local Constants --
37 ---------------------
39 -- Table of SPARK_Entities, True for each entity kind used in SPARK
54 -- True for each reference type used in SPARK
63 -- Size of hash table headers
65 ---------------------
66 -- Local Variables --
67 ---------------------
70 -- A special entity which denotes the heap object
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 -----------------------
89 -- Add file and corresponding scopes for unit to the tables
90 -- SPARK_File_Table and SPARK_Scope_Table. When two units are present
91 -- for the same compilation unit, as it happens for library-level
92 -- instantiations of generics, then Ubody is the number of the body
93 -- unit; otherwise it is No_Unit.
96 -- Filter table Xrefs to add all references used in SPARK to the table
97 -- SPARK_Xref_Table.
100 -- Hash function for hash table
102 --------------------
103 -- Add_SPARK_File --
104 --------------------
113 -- Add scope N to the table SPARK_Scope_Table
116 -- Call Add_SPARK_Scope on scopes
118 ---------------------
119 -- Add_SPARK_Scope --
120 ---------------------
126 -- The character describing the kind of scope is chosen to be the
127 -- same as the one describing the corresponding entity in cross
128 -- references, see Xref_Entity_Letters in lib-xrefs.ads
132 begin
133 -- Ignore scopes without a proper location
140 when E_Entry
141 | E_Entry_Family
142 | E_Generic_Function
143 | E_Generic_Package
144 | E_Generic_Procedure
145 | E_Package
146 | E_Protected_Type
147 | E_Task_Type
148 =>
151 when E_Function
152 | E_Procedure
153 =>
154 -- In SPARK we need to distinguish protected functions and
155 -- procedures from ordinary subprograms, but there are no
156 -- special Xref letters for them. Since this distiction is
157 -- only needed to detect protected calls, we pretend that
158 -- such calls are entry calls.
162 else
166 when E_Package_Body
167 | E_Protected_Body
168 | E_Subprogram_Body
169 | E_Task_Body
170 =>
175 -- Compilation of prj-attr.adb with -gnatn creates a node with
176 -- entity E_Void for the package defined at a-charac.ads16:13.
177 -- ??? TBD
185 -- File_Num and Scope_Num are filled later. From_Xref and To_Xref
186 -- are filled even later, but are initialized to represent an empty
187 -- range.
189 SPARK_Scope_Table.Append
191 File_Num => Dspec,
192 Scope_Num => Scope_Id,
193 Spec_File_Num => 0,
194 Spec_Scope_Num => 0,
195 Line => Nat (Get_Logical_Line_Number (Loc)),
196 Stype => Typ,
197 Col => Nat (Get_Column_Number (Loc)),
198 From_Xref => 1,
199 To_Xref => 0,
200 Scope_Entity => E));
202 Scope_Id := Scope_Id + 1;
203 end Add_SPARK_Scope;
205 --------------------------------
206 -- Detect_And_Add_SPARK_Scope --
207 --------------------------------
209 procedure Detect_And_Add_SPARK_Scope (N : Node_Id) is
210 begin
211 -- Entries
213 if Nkind_In (N, N_Entry_Body, N_Entry_Declaration)
215 -- Packages
217 or else Nkind_In (N, N_Package_Body,
218 N_Package_Body_Stub,
219 N_Package_Declaration)
220 -- Protected units
222 or else Nkind_In (N, N_Protected_Body,
223 N_Protected_Body_Stub,
224 N_Protected_Type_Declaration)
226 -- Subprograms
228 or else Nkind_In (N, N_Subprogram_Body,
229 N_Subprogram_Body_Stub,
230 N_Subprogram_Declaration)
232 -- Task units
234 or else Nkind_In (N, N_Task_Body,
235 N_Task_Body_Stub,
236 N_Task_Type_Declaration)
237 then
238 Add_SPARK_Scope (N);
239 end if;
240 end Detect_And_Add_SPARK_Scope;
242 procedure Traverse_Scopes is new
243 Traverse_Compilation_Unit (Detect_And_Add_SPARK_Scope);
245 -- Local variables
247 File_Name : String_Ptr;
248 Unit_File_Name : String_Ptr;
250 -- Start of processing for Add_SPARK_File
252 begin
253 -- Source file could be inexistant as a result of an error, if option
254 -- gnatQ is used.
256 if File = No_Source_File then
257 return;
258 end if;
260 -- Subunits are traversed as part of the top-level unit to which they
261 -- belong.
263 if Nkind (Unit (Cunit (Uspec))) = N_Subunit then
264 return;
265 end if;
267 Traverse_Scopes (CU => Cunit (Uspec), Inside_Stubs => True);
269 -- When two units are present for the same compilation unit, as it
270 -- happens for library-level instantiations of generics, then add all
271 -- scopes to the same SPARK file.
273 if Ubody /= No_Unit then
274 Traverse_Scopes (CU => Cunit (Ubody), Inside_Stubs => True);
275 end if;
277 -- Make entry for new file in file table
279 Get_Name_String (Reference_Name (File));
282 -- For subunits, also retrieve the file name of the unit. Only do so if
283 -- unit has an associated compilation unit.
287 then
290 else
291 Unit_File_Name := null;
292 end if;
294 SPARK_File_Table.Append (
295 (File_Name => File_Name,
296 Unit_File_Name => Unit_File_Name,
297 File_Num => Dspec,
298 From_Scope => From,
299 To_Scope => SPARK_Scope_Table.Last));
300 end Add_SPARK_File;
302 ---------------------
303 -- Add_SPARK_Xrefs --
304 ---------------------
306 procedure Add_SPARK_Xrefs is
307 function Entity_Of_Scope (S : Scope_Index) return Entity_Id;
308 -- Return the entity which maps to the input scope index
310 function Get_Entity_Type (E : Entity_Id) return Character;
311 -- Return a character representing the type of entity
313 function Get_Scope_Num (N : Entity_Id) return Nat;
314 -- Return the scope number associated to entity N
316 function Is_Constant_Object_Without_Variable_Input
317 (E : Entity_Id) return Boolean;
318 -- Return True if E is known to have no variable input, as defined in
319 -- SPARK RM.
321 function Is_Future_Scope_Entity
322 (E : Entity_Id;
323 S : Scope_Index) return Boolean;
324 -- Check whether entity E is in SPARK_Scope_Table at index S or higher
326 function Is_SPARK_Reference
327 (E : Entity_Id;
328 Typ : Character) return Boolean;
329 -- Return whether entity reference E meets SPARK requirements. Typ is
330 -- the reference type.
332 function Is_SPARK_Scope (E : Entity_Id) return Boolean;
333 -- Return whether the entity or reference scope meets requirements for
334 -- being a SPARK scope.
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 Set_Scope_Num (N : Entity_Id; Num : Nat);
343 -- Associate entity N to scope number Num
345 procedure Update_Scope_Range
346 (S : Scope_Index;
347 From : Xref_Index;
348 To : Xref_Index);
349 -- Update the scope which maps to S with the new range From .. To
351 package Sorting is new GNAT.Heap_Sort_G (Move, Lt);
353 No_Scope : constant Nat := 0;
354 -- Initial scope counter
356 type Scope_Rec is record
357 Num : Nat;
358 Entity : Entity_Id;
359 end record;
360 -- Type used to relate an entity and a scope number
362 package Scopes is new GNAT.HTable.Simple_HTable
363 (Header_Num => Entity_Hashed_Range,
364 Element => Scope_Rec,
365 No_Element => (Num => No_Scope, Entity => Empty),
366 Key => Entity_Id,
367 Hash => Entity_Hash,
368 Equal => "=");
369 -- Package used to build a correspondence between entities and scope
370 -- numbers used in SPARK cross references.
372 Nrefs : Nat := Xrefs.Last;
373 -- Number of references in table. This value may get reset (reduced)
374 -- when we eliminate duplicate reference entries as well as references
375 -- not suitable for local cross-references.
377 Nrefs_Add : constant Nat := Drefs.Last;
378 -- Number of additional references which correspond to dereferences in
379 -- the source code.
381 Rnums : array (0 .. Nrefs + Nrefs_Add) of Nat;
382 -- This array contains numbers of references in the Xrefs table. This
383 -- list is sorted in output order. The extra 0'th entry is convenient
384 -- for the call to sort. When we sort the table, we move the indices in
385 -- Rnums around, but we do not move the original table entries.
387 ---------------------
388 -- Entity_Of_Scope --
389 ---------------------
391 function Entity_Of_Scope (S : Scope_Index) return Entity_Id is
392 begin
393 return SPARK_Scope_Table.Table (S).Scope_Entity;
394 end Entity_Of_Scope;
396 ---------------------
397 -- Get_Entity_Type --
398 ---------------------
400 function Get_Entity_Type (E : Entity_Id) return Character is
401 begin
402 case Ekind (E) is
407 end case;
408 end Get_Entity_Type;
410 -------------------
411 -- Get_Scope_Num --
412 -------------------
414 function Get_Scope_Num (N : Entity_Id) return Nat is
415 begin
416 return Scopes.Get (N).Num;
417 end Get_Scope_Num;
419 -----------------------------------------------
420 -- Is_Constant_Object_Without_Variable_Input --
421 -----------------------------------------------
423 function Is_Constant_Object_Without_Variable_Input
424 (E : Entity_Id) return Boolean
425 is
426 Result : Boolean;
428 begin
429 case Ekind (E) is
431 -- A constant is known to have no variable input if its
432 -- initializing expression is static (a value which is
433 -- compile-time-known is not guaranteed to have no variable input
434 -- as defined in the SPARK RM). Otherwise, the constant may or not
435 -- have variable input.
437 when E_Constant =>
438 declare
439 Decl : Node_Id;
440 begin
441 if Present (Full_View (E)) then
442 Decl := Parent (Full_View (E));
443 else
444 Decl := Parent (E);
445 end if;
447 if Is_Imported (E) then
448 Result := False;
449 else
450 pragma Assert (Present (Expression (Decl)));
451 Result := Is_Static_Expression (Expression (Decl));
452 end if;
453 end;
455 when E_In_Parameter
456 | E_Loop_Parameter
457 =>
458 Result := True;
460 when others =>
461 Result := False;
462 end case;
464 return Result;
465 end Is_Constant_Object_Without_Variable_Input;
467 ----------------------------
468 -- Is_Future_Scope_Entity --
469 ----------------------------
471 function Is_Future_Scope_Entity
472 (E : Entity_Id;
473 S : Scope_Index) return Boolean
474 is
475 function Is_Past_Scope_Entity return Boolean;
476 -- Check whether entity E is in SPARK_Scope_Table at index strictly
477 -- lower than S.
479 --------------------------
480 -- Is_Past_Scope_Entity --
481 --------------------------
483 function Is_Past_Scope_Entity return Boolean is
484 begin
485 for Index in SPARK_Scope_Table.First .. S - 1 loop
486 if SPARK_Scope_Table.Table (Index).Scope_Entity = E then
487 return True;
488 end if;
489 end loop;
491 return False;
492 end Is_Past_Scope_Entity;
494 -- Start of processing for Is_Future_Scope_Entity
496 begin
497 for Index in S .. SPARK_Scope_Table.Last loop
498 if SPARK_Scope_Table.Table (Index).Scope_Entity = E then
499 return True;
500 end if;
501 end loop;
503 -- If this assertion fails, this means that the scope which we are
504 -- looking for has been treated already, which reveals a problem in
505 -- the order of cross-references.
507 pragma Assert (not Is_Past_Scope_Entity);
509 return False;
510 end Is_Future_Scope_Entity;
512 ------------------------
513 -- Is_SPARK_Reference --
514 ------------------------
516 function Is_SPARK_Reference
517 (E : Entity_Id;
518 Typ : Character) return Boolean
519 is
520 begin
521 -- The only references of interest on callable entities are calls. On
522 -- uncallable entities, the only references of interest are reads and
523 -- writes.
525 if Ekind (E) in Overloadable_Kind then
528 -- In all other cases, result is true for reference/modify cases,
529 -- and false for all other cases.
531 else
533 end if;
534 end Is_SPARK_Reference;
536 --------------------
537 -- Is_SPARK_Scope --
538 --------------------
540 function Is_SPARK_Scope (E : Entity_Id) return Boolean is
541 begin
542 return Present (E)
543 and then not Is_Generic_Unit (E)
544 and then Renamed_Entity (E) = Empty
545 and then Get_Scope_Num (E) /= No_Scope;
546 end Is_SPARK_Scope;
548 --------
549 -- Lt --
550 --------
552 function Lt (Op1 : Natural; Op2 : Natural) return Boolean is
553 T1 : constant Xref_Entry := Xrefs.Table (Rnums (Nat (Op1)));
554 T2 : constant Xref_Entry := Xrefs.Table (Rnums (Nat (Op2)));
556 begin
557 -- First test: if entity is in different unit, sort by unit. Note:
558 -- that we use Ent_Scope_File rather than Eun, as Eun may refer to
559 -- the file where the generic scope is defined, which may differ from
560 -- the file where the enclosing scope is defined. It is the latter
561 -- which matters for a correct order here.
563 if T1.Ent_Scope_File /= T2.Ent_Scope_File then
564 return Dependency_Num (T1.Ent_Scope_File) <
565 Dependency_Num (T2.Ent_Scope_File);
567 -- Second test: within same unit, sort by location of the scope of
568 -- the entity definition.
570 elsif Get_Scope_Num (T1.Key.Ent_Scope) /=
571 Get_Scope_Num (T2.Key.Ent_Scope)
572 then
573 return Get_Scope_Num (T1.Key.Ent_Scope) <
574 Get_Scope_Num (T2.Key.Ent_Scope);
576 -- Third test: within same unit and scope, sort by location of
577 -- entity definition.
579 elsif T1.Def /= T2.Def then
580 return T1.Def < T2.Def;
582 else
583 -- Both entities must be equal at this point
585 pragma Assert (T1.Key.Ent = T2.Key.Ent);
586 pragma Assert (T1.Key.Ent_Scope = T2.Key.Ent_Scope);
587 pragma Assert (T1.Ent_Scope_File = T2.Ent_Scope_File);
589 -- Fourth test: if reference is in same unit as entity definition,
590 -- sort first.
592 if T1.Key.Lun /= T2.Key.Lun
593 and then T1.Ent_Scope_File = T1.Key.Lun
594 then
595 return True;
597 elsif T1.Key.Lun /= T2.Key.Lun
598 and then T2.Ent_Scope_File = T2.Key.Lun
599 then
600 return False;
602 -- Fifth test: if reference is in same unit and same scope as
603 -- entity definition, sort first.
605 elsif T1.Ent_Scope_File = T1.Key.Lun
606 and then T1.Key.Ref_Scope /= T2.Key.Ref_Scope
607 and then T1.Key.Ent_Scope = T1.Key.Ref_Scope
608 then
609 return True;
611 elsif T2.Ent_Scope_File = T2.Key.Lun
612 and then T1.Key.Ref_Scope /= T2.Key.Ref_Scope
613 and then T2.Key.Ent_Scope = T2.Key.Ref_Scope
614 then
615 return False;
617 -- Sixth test: for same entity, sort by reference location unit
619 elsif T1.Key.Lun /= T2.Key.Lun then
620 return Dependency_Num (T1.Key.Lun) <
621 Dependency_Num (T2.Key.Lun);
623 -- Seventh test: for same entity, sort by reference location scope
625 elsif Get_Scope_Num (T1.Key.Ref_Scope) /=
626 Get_Scope_Num (T2.Key.Ref_Scope)
627 then
628 return Get_Scope_Num (T1.Key.Ref_Scope) <
629 Get_Scope_Num (T2.Key.Ref_Scope);
631 -- Eighth test: order of location within referencing unit
633 elsif T1.Key.Loc /= T2.Key.Loc then
634 return T1.Key.Loc < T2.Key.Loc;
636 -- Finally, for two locations at the same address prefer the one
638 -- extension takes preference, when there are more than one
639 -- reference at the same location. As a result, in the case of
640 -- entities that are in-out actuals, the read reference follows
641 -- the modify reference.
643 else
645 end if;
646 end if;
647 end Lt;
649 ----------
650 -- Move --
651 ----------
653 procedure Move (From : Natural; To : Natural) is
654 begin
655 Rnums (Nat (To)) := Rnums (Nat (From));
656 end Move;
658 -------------------
659 -- Set_Scope_Num --
660 -------------------
662 procedure Set_Scope_Num (N : Entity_Id; Num : Nat) is
663 begin
667 ------------------------
668 -- Update_Scope_Range --
669 ------------------------
671 procedure Update_Scope_Range
675 is
676 begin
681 -- Local variables
693 -- Start of processing for Add_SPARK_Xrefs
695 begin
697 declare
699 begin
704 declare
707 begin
712 -- Capture the definition Sloc values. As in the case of normal cross
713 -- references, we have to wait until now to get the correct value.
719 -- Eliminate entries not appropriate for SPARK. Done prior to sorting
720 -- cross-references, as it discards useless references which do not have
721 -- a proper format for the comparison function (like no location).
727 declare
730 begin
737 -- Discard references from unknown scopes, e.g. generic scopes
741 then
748 -- Sort the references
752 -- Eliminate duplicate entries
754 -- We need this test for Ref_Count because if we force ALI file
755 -- generation in case of errors detected, it may be the case that
756 -- Nrefs is 0, so we should not reset it here.
770 -- Eliminate the reference if it is at the same location as the previous
771 -- one, unless it is a read-reference indicating that the entity is an
772 -- in-out actual in a call.
780 declare
783 begin
786 then
795 -- The two steps have eliminated all references, nothing to do
805 -- Loop to output references
808 declare
813 begin
814 -- If this assertion fails, the scope which we are looking for is
815 -- not in SPARK scope table, which reveals either a problem in the
816 -- construction of the scope table, or an erroneous scope for the
817 -- current cross-reference.
821 -- Update the range of cross references to which the current scope
822 -- refers to. This may be the empty range only for the first scope
823 -- considered.
826 Update_Scope_Range
841 end if;
843 if Ref.Ent = Heap then
844 Line := 0;
845 Col := 0;
846 else
847 Line := Nat (Get_Logical_Line_Number (Ref_Entry.Def));
848 Col := Nat (Get_Column_Number (Ref_Entry.Def));
849 end if;
851 -- References to constant objects without variable inputs (see
852 -- SPARK RM 3.3.1) are considered specially in SPARK section,
853 -- because these will be translated as constants in the
854 -- intermediate language for formal verification, and should
855 -- therefore never appear in frame conditions. Other constants may
856 -- later be treated the same, up to GNATprove to decide based on
857 -- its flow analysis.
859 if Is_Constant_Object_Without_Variable_Input (Ref.Ent) then
861 else
862 Typ := Ref.Typ;
863 end if;
865 SPARK_Xref_Table.Append (
866 (Entity_Name => Ref_Name,
867 Entity_Line => Line,
868 Etype => Get_Entity_Type (Ref.Ent),
869 Entity_Col => Col,
870 File_Num => Dependency_Num (Ref.Lun),
871 Scope_Num => Get_Scope_Num (Ref.Ref_Scope),
872 Line => Nat (Get_Logical_Line_Number (Ref.Loc)),
873 Rtype => Typ,
874 Col => Nat (Get_Column_Number (Ref.Loc))));
875 end;
876 end loop;
878 -- Update the range of cross references to which the scope refers to
880 Update_Scope_Range
881 (S => Scope_Id,
882 From => From_Index,
883 To => SPARK_Xref_Table.Last);
884 end Add_SPARK_Xrefs;
886 -------------------------
887 -- Collect_SPARK_Xrefs --
888 -------------------------
890 procedure Collect_SPARK_Xrefs
891 (Sdep_Table : Unit_Ref_Table;
892 Num_Sdep : Nat)
893 is
894 Sdep : Pos;
895 Sdep_Next : Pos;
896 -- Index of the current and next source dependency
898 Sdep_File : Pos;
899 -- Index of the file to which the scopes need to be assigned; for
900 -- library-level instances of generic units this points to the unit
901 -- of the body, because this is where references are assigned to.
903 Ubody : Unit_Number_Type;
904 Uspec : Unit_Number_Type;
905 -- Unit numbers for the dependency spec and possibly its body (only in
906 -- the case of library-level instance of a generic package).
908 begin
909 -- Cross-references should have been computed first
911 pragma Assert (Xrefs.Last /= 0);
913 Initialize_SPARK_Tables;
915 -- Generate file and scope SPARK cross-reference information
917 Sdep := 1;
918 while Sdep <= Num_Sdep loop
920 -- Skip dependencies with no entity node, e.g. configuration files
921 -- with pragmas (.adc) or target description (.atp), since they
922 -- present no interest for SPARK cross references.
924 if No (Cunit_Entity (Sdep_Table (Sdep))) then
925 Sdep_Next := Sdep + 1;
927 -- For library-level instantiation of a generic, two consecutive
928 -- units refer to the same compilation unit node and entity (one to
929 -- body, one to spec). In that case, treat them as a single unit for
930 -- the sake of SPARK cross references by passing to Add_SPARK_File.
932 else
933 if Sdep < Num_Sdep
934 and then Cunit_Entity (Sdep_Table (Sdep)) =
935 Cunit_Entity (Sdep_Table (Sdep + 1))
936 then
937 declare
938 Cunit1 : Node_Id renames Cunit (Sdep_Table (Sdep));
939 Cunit2 : Node_Id renames Cunit (Sdep_Table (Sdep + 1));
941 begin
942 -- Both Cunits point to compilation unit nodes
944 pragma Assert
945 (Nkind (Cunit1) = N_Compilation_Unit
946 and then Nkind (Cunit2) = N_Compilation_Unit);
948 -- Do not depend on the sorting order, which is based on
949 -- Unit_Name, and for library-level instances of nested
950 -- generic packages they are equal.
952 -- If declaration comes before the body
954 if Nkind (Unit (Cunit1)) = N_Package_Declaration
955 and then Nkind (Unit (Cunit2)) = N_Package_Body
956 then
957 Uspec := Sdep_Table (Sdep);
958 Ubody := Sdep_Table (Sdep + 1);
960 Sdep_File := Sdep + 1;
962 -- If body comes before declaration
964 elsif Nkind (Unit (Cunit1)) = N_Package_Body
965 and then Nkind (Unit (Cunit2)) = N_Package_Declaration
966 then
967 Uspec := Sdep_Table (Sdep + 1);
968 Ubody := Sdep_Table (Sdep);
970 Sdep_File := Sdep;
972 -- Otherwise it is an error
974 else
975 raise Program_Error;
976 end if;
978 Sdep_Next := Sdep + 2;
979 end;
981 -- ??? otherwise?
983 else
984 Uspec := Sdep_Table (Sdep);
985 Ubody := No_Unit;
987 Sdep_File := Sdep;
988 Sdep_Next := Sdep + 1;
989 end if;
991 Add_SPARK_File
992 (Uspec => Uspec,
993 Ubody => Ubody,
994 Dspec => Sdep_File);
995 end if;
997 Sdep := Sdep_Next;
998 end loop;
1000 -- Fill in the spec information when relevant
1002 declare
1003 package Entity_Hash_Table is new
1004 GNAT.HTable.Simple_HTable
1005 (Header_Num => Entity_Hashed_Range,
1006 Element => Scope_Index,
1007 No_Element => 0,
1008 Key => Entity_Id,
1009 Hash => Entity_Hash,
1010 Equal => "=");
1012 begin
1013 -- Fill in the hash-table
1015 for S in SPARK_Scope_Table.First .. SPARK_Scope_Table.Last loop
1016 declare
1017 Srec : SPARK_Scope_Record renames SPARK_Scope_Table.Table (S);
1018 begin
1019 Entity_Hash_Table.Set (Srec.Scope_Entity, S);
1020 end;
1021 end loop;
1023 -- Use the hash-table to locate spec entities
1025 for S in SPARK_Scope_Table.First .. SPARK_Scope_Table.Last loop
1026 declare
1027 Srec : SPARK_Scope_Record renames SPARK_Scope_Table.Table (S);
1029 Spec_Entity : constant Entity_Id :=
1030 Unique_Entity (Srec.Scope_Entity);
1031 Spec_Scope : constant Scope_Index :=
1032 Entity_Hash_Table.Get (Spec_Entity);
1034 begin
1035 -- Generic spec may be missing in which case Spec_Scope is zero
1037 if Spec_Entity /= Srec.Scope_Entity
1038 and then Spec_Scope /= 0
1039 then
1040 Srec.Spec_File_Num :=
1041 SPARK_Scope_Table.Table (Spec_Scope).File_Num;
1042 Srec.Spec_Scope_Num :=
1043 SPARK_Scope_Table.Table (Spec_Scope).Scope_Num;
1044 end if;
1045 end;
1046 end loop;
1047 end;
1049 -- Generate SPARK cross-reference information
1051 Add_SPARK_Xrefs;
1052 end Collect_SPARK_Xrefs;
1054 -------------------------------------
1055 -- Enclosing_Subprogram_Or_Package --
1056 -------------------------------------
1058 function Enclosing_Subprogram_Or_Library_Package
1059 (N : Node_Id) return Entity_Id
1060 is
1061 Context : Entity_Id;
1063 begin
1064 -- If N is the defining identifier for a subprogram, then return the
1065 -- enclosing subprogram or package, not this subprogram.
1067 if Nkind_In (N, N_Defining_Identifier, N_Defining_Operator_Symbol)
1068 and then (Ekind (N) in Entry_Kind
1069 or else Ekind (N) = E_Subprogram_Body
1070 or else Ekind (N) in Generic_Subprogram_Kind
1071 or else Ekind (N) in Subprogram_Kind)
1072 then
1073 Context := Parent (Unit_Declaration_Node (N));
1075 -- If this was a library-level subprogram then replace Context with
1076 -- its Unit, which points to N_Subprogram_* node.
1078 if Nkind (Context) = N_Compilation_Unit then
1079 Context := Unit (Context);
1080 end if;
1081 else
1082 Context := N;
1083 end if;
1085 while Present (Context) loop
1086 case Nkind (Context) is
1087 when N_Package_Body
1088 | N_Package_Specification
1089 =>
1090 -- Only return a library-level package
1092 if Is_Library_Level_Entity (Defining_Entity (Context)) then
1093 Context := Defining_Entity (Context);
1094 exit;
1095 else
1096 Context := Parent (Context);
1097 end if;
1099 when N_Pragma =>
1101 -- The enclosing subprogram for a precondition, postcondition,
1102 -- or contract case should be the declaration preceding the
1103 -- pragma (skipping any other pragmas between this pragma and
1104 -- this declaration.
1106 while Nkind (Context) = N_Pragma
1107 and then Is_List_Member (Context)
1108 and then Present (Prev (Context))
1109 loop
1110 Context := Prev (Context);
1111 end loop;
1113 if Nkind (Context) = N_Pragma then
1114 Context := Parent (Context);
1115 end if;
1117 when N_Entry_Body
1118 | N_Entry_Declaration
1119 | N_Protected_Type_Declaration
1120 | N_Subprogram_Body
1121 | N_Subprogram_Declaration
1122 | N_Subprogram_Specification
1123 | N_Task_Body
1124 | N_Task_Type_Declaration
1125 =>
1126 Context := Defining_Entity (Context);
1127 exit;
1129 when others =>
1130 Context := Parent (Context);
1131 end case;
1132 end loop;
1134 if Nkind (Context) = N_Defining_Program_Unit_Name then
1135 Context := Defining_Identifier (Context);
1136 end if;
1138 -- Do not return a scope without a proper location
1140 if Present (Context)
1141 and then Sloc (Context) = No_Location
1142 then
1143 return Empty;
1144 end if;
1146 return Context;
1147 end Enclosing_Subprogram_Or_Library_Package;
1149 -----------------
1150 -- Entity_Hash --
1151 -----------------
1153 function Entity_Hash (E : Entity_Id) return Entity_Hashed_Range is
1154 begin
1155 return
1156 Entity_Hashed_Range (E mod (Entity_Id (Entity_Hashed_Range'Last) + 1));
1157 end Entity_Hash;
1159 --------------------------
1160 -- Generate_Dereference --
1161 --------------------------
1163 procedure Generate_Dereference
1164 (N : Node_Id;
1166 is
1167 procedure Create_Heap;
1168 -- Create and decorate the special entity which denotes the heap
1170 -----------------
1171 -- Create_Heap --
1172 -----------------
1174 procedure Create_Heap is
1175 begin
1176 Name_Len := Name_Of_Heap_Variable'Length;
1177 Name_Buffer (1 .. Name_Len) := Name_Of_Heap_Variable;
1179 Heap := Make_Defining_Identifier (Standard_Location, Name_Enter);
1181 Set_Ekind (Heap, E_Variable);
1182 Set_Is_Internal (Heap, True);
1183 Set_Has_Fully_Qualified_Name (Heap);
1184 end Create_Heap;
1186 -- Local variables
1188 Loc : constant Source_Ptr := Sloc (N);
1190 -- Start of processing for Generate_Dereference
1192 begin
1193 if Loc > No_Location then
1194 Drefs.Increment_Last;
1196 declare
1197 Deref_Entry : Xref_Entry renames Drefs.Table (Drefs.Last);
1198 Deref : Xref_Key renames Deref_Entry.Key;
1200 begin
1201 if No (Heap) then
1202 Create_Heap;
1203 end if;
1205 Deref.Ent := Heap;
1206 Deref.Loc := Loc;
1207 Deref.Typ := Typ;
1209 -- It is as if the special "Heap" was defined in the main unit,
1210 -- in the scope of the entity for the main unit. This single
1211 -- definition point is required to ensure that sorting cross
1212 -- references works for "Heap" references as well.
1214 Deref.Eun := Main_Unit;
1215 Deref.Lun := Get_Top_Level_Code_Unit (Loc);
1217 Deref.Ref_Scope := Enclosing_Subprogram_Or_Library_Package (N);
1218 Deref.Ent_Scope := Cunit_Entity (Main_Unit);
1220 Deref_Entry.Def := No_Location;
1222 Deref_Entry.Ent_Scope_File := Main_Unit;
1223 end;
1224 end if;
1225 end Generate_Dereference;
1227 -------------------------------
1228 -- Traverse_Compilation_Unit --
1229 -------------------------------
1231 procedure Traverse_Compilation_Unit
1232 (CU : Node_Id;
1233 Inside_Stubs : Boolean)
1234 is
1235 procedure Traverse_Block (N : Node_Id);
1236 procedure Traverse_Declaration_Or_Statement (N : Node_Id);
1237 procedure Traverse_Declarations_And_HSS (N : Node_Id);
1238 procedure Traverse_Declarations_Or_Statements (L : List_Id);
1239 procedure Traverse_Handled_Statement_Sequence (N : Node_Id);
1240 procedure Traverse_Package_Body (N : Node_Id);
1241 procedure Traverse_Visible_And_Private_Parts (N : Node_Id);
1242 procedure Traverse_Protected_Body (N : Node_Id);
1243 procedure Traverse_Subprogram_Body (N : Node_Id);
1244 procedure Traverse_Task_Body (N : Node_Id);
1246 -- Traverse corresponding construct, calling Process on all declarations
1248 --------------------
1249 -- Traverse_Block --
1250 --------------------
1252 procedure Traverse_Block (N : Node_Id) renames
1253 Traverse_Declarations_And_HSS;
1255 ---------------------------------------
1256 -- Traverse_Declaration_Or_Statement --
1257 ---------------------------------------
1259 procedure Traverse_Declaration_Or_Statement (N : Node_Id) is
1260 function Traverse_Stub (N : Node_Id) return Boolean;
1261 -- Returns True iff stub N should be traversed
1263 function Traverse_Stub (N : Node_Id) return Boolean is
1264 begin
1265 pragma Assert (Nkind_In (N, N_Package_Body_Stub,
1266 N_Protected_Body_Stub,
1267 N_Subprogram_Body_Stub,
1268 N_Task_Body_Stub));
1270 return Inside_Stubs and then Present (Library_Unit (N));
1271 end Traverse_Stub;
1273 -- Start of processing for Traverse_Declaration_Or_Statement
1275 begin
1276 case Nkind (N) is
1277 when N_Package_Declaration =>
1278 Traverse_Visible_And_Private_Parts (Specification (N));
1280 when N_Package_Body =>
1281 Traverse_Package_Body (N);
1283 when N_Package_Body_Stub =>
1284 if Traverse_Stub (N) then
1285 Traverse_Package_Body (Get_Body_From_Stub (N));
1286 end if;
1288 when N_Subprogram_Body =>
1289 Traverse_Subprogram_Body (N);
1291 when N_Entry_Body =>
1292 Traverse_Subprogram_Body (N);
1294 when N_Subprogram_Body_Stub =>
1295 if Traverse_Stub (N) then
1296 Traverse_Subprogram_Body (Get_Body_From_Stub (N));
1297 end if;
1299 when N_Protected_Body =>
1300 Traverse_Protected_Body (N);
1302 when N_Protected_Body_Stub =>
1303 if Traverse_Stub (N) then
1304 Traverse_Protected_Body (Get_Body_From_Stub (N));
1305 end if;
1307 when N_Protected_Type_Declaration =>
1308 Traverse_Visible_And_Private_Parts (Protected_Definition (N));
1310 when N_Task_Definition =>
1311 Traverse_Visible_And_Private_Parts (N);
1313 when N_Task_Body =>
1314 Traverse_Task_Body (N);
1316 when N_Task_Body_Stub =>
1317 if Traverse_Stub (N) then
1318 Traverse_Task_Body (Get_Body_From_Stub (N));
1319 end if;
1321 when N_Block_Statement =>
1322 Traverse_Block (N);
1324 when N_If_Statement =>
1326 -- Traverse the statements in the THEN part
1328 Traverse_Declarations_Or_Statements (Then_Statements (N));
1330 -- Loop through ELSIF parts if present
1332 if Present (Elsif_Parts (N)) then
1333 declare
1334 Elif : Node_Id := First (Elsif_Parts (N));
1336 begin
1337 while Present (Elif) loop
1338 Traverse_Declarations_Or_Statements
1339 (Then_Statements (Elif));
1340 Next (Elif);
1341 end loop;
1342 end;
1343 end if;
1345 -- Finally traverse the ELSE statements if present
1347 Traverse_Declarations_Or_Statements (Else_Statements (N));
1349 when N_Case_Statement =>
1351 -- Process case branches
1353 declare
1354 Alt : Node_Id := First (Alternatives (N));
1355 begin
1356 loop
1357 Traverse_Declarations_Or_Statements (Statements (Alt));
1358 Next (Alt);
1359 exit when No (Alt);
1360 end loop;
1361 end;
1363 when N_Extended_Return_Statement =>
1364 Traverse_Handled_Statement_Sequence
1365 (Handled_Statement_Sequence (N));
1367 when N_Loop_Statement =>
1368 Traverse_Declarations_Or_Statements (Statements (N));
1370 -- Generic declarations are ignored
1372 when others =>
1373 null;
1374 end case;
1375 end Traverse_Declaration_Or_Statement;
1377 -----------------------------------
1378 -- Traverse_Declarations_And_HSS --
1379 -----------------------------------
1381 procedure Traverse_Declarations_And_HSS (N : Node_Id) is
1382 begin
1383 Traverse_Declarations_Or_Statements (Declarations (N));
1384 Traverse_Handled_Statement_Sequence (Handled_Statement_Sequence (N));
1385 end Traverse_Declarations_And_HSS;
1387 -----------------------------------------
1388 -- Traverse_Declarations_Or_Statements --
1389 -----------------------------------------
1391 procedure Traverse_Declarations_Or_Statements (L : List_Id) is
1392 N : Node_Id;
1394 begin
1395 -- Loop through statements or declarations
1397 N := First (L);
1398 while Present (N) loop
1400 -- Call Process on all declarations
1402 if Nkind (N) in N_Declaration
1403 or else Nkind (N) in N_Later_Decl_Item
1404 or else Nkind (N) = N_Entry_Body
1405 then
1406 Process (N);
1407 end if;
1409 Traverse_Declaration_Or_Statement (N);
1411 Next (N);
1412 end loop;
1413 end Traverse_Declarations_Or_Statements;
1415 -----------------------------------------
1416 -- Traverse_Handled_Statement_Sequence --
1417 -----------------------------------------
1419 procedure Traverse_Handled_Statement_Sequence (N : Node_Id) is
1420 Handler : Node_Id;
1422 begin
1423 if Present (N) then
1424 Traverse_Declarations_Or_Statements (Statements (N));
1426 if Present (Exception_Handlers (N)) then
1427 Handler := First (Exception_Handlers (N));
1428 while Present (Handler) loop
1429 Traverse_Declarations_Or_Statements (Statements (Handler));
1430 Next (Handler);
1431 end loop;
1432 end if;
1433 end if;
1434 end Traverse_Handled_Statement_Sequence;
1436 ---------------------------
1437 -- Traverse_Package_Body --
1438 ---------------------------
1440 procedure Traverse_Package_Body (N : Node_Id) is
1441 Spec_E : constant Entity_Id := Unique_Defining_Entity (N);
1443 begin
1444 case Ekind (Spec_E) is
1445 when E_Package =>
1446 Traverse_Declarations_And_HSS (N);
1448 when E_Generic_Package =>
1449 null;
1451 when others =>
1452 raise Program_Error;
1453 end case;
1454 end Traverse_Package_Body;
1456 -----------------------------
1457 -- Traverse_Protected_Body --
1458 -----------------------------
1460 procedure Traverse_Protected_Body (N : Node_Id) is
1461 begin
1462 Traverse_Declarations_Or_Statements (Declarations (N));
1463 end Traverse_Protected_Body;
1465 ------------------------------
1466 -- Traverse_Subprogram_Body --
1467 ------------------------------
1469 procedure Traverse_Subprogram_Body (N : Node_Id) is
1470 Spec_E : constant Entity_Id := Unique_Defining_Entity (N);
1472 begin
1473 case Ekind (Spec_E) is
1474 when Entry_Kind
1475 | E_Function
1476 | E_Procedure
1477 =>
1478 Traverse_Declarations_And_HSS (N);
1480 when Generic_Subprogram_Kind =>
1481 null;
1483 when others =>
1484 raise Program_Error;
1485 end case;
1486 end Traverse_Subprogram_Body;
1488 ------------------------
1489 -- Traverse_Task_Body --
1490 ------------------------
1492 procedure Traverse_Task_Body (N : Node_Id) renames
1493 Traverse_Declarations_And_HSS;
1495 ----------------------------------------
1496 -- Traverse_Visible_And_Private_Parts --
1497 ----------------------------------------
1499 procedure Traverse_Visible_And_Private_Parts (N : Node_Id) is
1500 begin
1501 Traverse_Declarations_Or_Statements (Visible_Declarations (N));
1502 Traverse_Declarations_Or_Statements (Private_Declarations (N));
1503 end Traverse_Visible_And_Private_Parts;
1505 -- Local variables
1507 Lu : Node_Id;
1509 -- Start of processing for Traverse_Compilation_Unit
1511 begin
1512 -- Get Unit (checking case of subunit)
1514 Lu := Unit (CU);
1516 if Nkind (Lu) = N_Subunit then
1517 Lu := Proper_Body (Lu);
1518 end if;
1520 -- Do not add scopes for generic units
1522 if Nkind (Lu) = N_Package_Body
1523 and then Ekind (Corresponding_Spec (Lu)) in Generic_Unit_Kind
1524 then
1525 return;
1526 end if;
1528 -- Call Process on all declarations
1530 if Nkind (Lu) in N_Declaration
1531 or else Nkind (Lu) in N_Later_Decl_Item
1532 then
1533 Process (Lu);
1534 end if;
1536 -- Traverse the unit
1538 Traverse_Declaration_Or_Statement (Lu);
1539 end Traverse_Compilation_Unit;
1541 end SPARK_Specific;