| blob | 95056e09ace4a004e12c06fcb8f74d3c2859d36f |
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 generic
105 -- Call Process on all declarations within compilation unit CU. If flag
106 -- Inside_Stubs is True, then the body of stubs is also traversed. Generic
107 -- declarations are ignored.
109 --------------------
110 -- Add_SPARK_File --
111 --------------------
120 -- Add scope N to the table SPARK_Scope_Table
123 -- Call Add_SPARK_Scope on scopes
125 ---------------------
126 -- Add_SPARK_Scope --
127 ---------------------
133 -- The character describing the kind of scope is chosen to be the
134 -- same as the one describing the corresponding entity in cross
135 -- references, see Xref_Entity_Letters in lib-xrefs.ads
139 begin
140 -- Ignore scopes without a proper location
147 when E_Entry |
148 E_Entry_Family |
149 E_Generic_Function |
150 E_Generic_Package |
151 E_Generic_Procedure |
152 E_Package |
153 E_Protected_Type |
154 E_Task_Type =>
159 -- In SPARK we need to distinguish protected functions and
160 -- procedures from ordinary subprograms, but there are no
161 -- special Xref letters for them. Since this distiction is
162 -- only needed to detect protected calls, we pretend that
163 -- such calls are entry calls.
167 else
171 when E_Package_Body |
172 E_Protected_Body |
173 E_Subprogram_Body |
174 E_Task_Body =>
179 -- Compilation of prj-attr.adb with -gnatn creates a node with
180 -- entity E_Void for the package defined at a-charac.ads16:13.
181 -- ??? TBD
189 -- File_Num and Scope_Num are filled later. From_Xref and To_Xref
190 -- are filled even later, but are initialized to represent an empty
191 -- range.
193 SPARK_Scope_Table.Append
195 File_Num => Dspec,
196 Scope_Num => Scope_Id,
197 Spec_File_Num => 0,
198 Spec_Scope_Num => 0,
199 Line => Nat (Get_Logical_Line_Number (Loc)),
200 Stype => Typ,
201 Col => Nat (Get_Column_Number (Loc)),
202 From_Xref => 1,
203 To_Xref => 0,
204 Scope_Entity => E));
206 Scope_Id := Scope_Id + 1;
207 end Add_SPARK_Scope;
209 --------------------------------
210 -- Detect_And_Add_SPARK_Scope --
211 --------------------------------
213 procedure Detect_And_Add_SPARK_Scope (N : Node_Id) is
214 begin
215 -- Entries
217 if Nkind_In (N, N_Entry_Body, N_Entry_Declaration)
219 -- Packages
221 or else Nkind_In (N, N_Package_Body,
222 N_Package_Body_Stub,
223 N_Package_Declaration)
224 -- Protected units
226 or else Nkind_In (N, N_Protected_Body,
227 N_Protected_Body_Stub,
228 N_Protected_Type_Declaration)
230 -- Subprograms
232 or else Nkind_In (N, N_Subprogram_Body,
233 N_Subprogram_Body_Stub,
234 N_Subprogram_Declaration)
236 -- Task units
238 or else Nkind_In (N, N_Task_Body,
239 N_Task_Body_Stub,
240 N_Task_Type_Declaration)
241 then
242 Add_SPARK_Scope (N);
243 end if;
244 end Detect_And_Add_SPARK_Scope;
246 procedure Traverse_Scopes is new
247 Traverse_Compilation_Unit (Detect_And_Add_SPARK_Scope);
249 -- Local variables
251 File_Name : String_Ptr;
252 Unit_File_Name : String_Ptr;
254 -- Start of processing for Add_SPARK_File
256 begin
257 -- Source file could be inexistant as a result of an error, if option
258 -- gnatQ is used.
260 if File = No_Source_File then
261 return;
262 end if;
264 -- Subunits are traversed as part of the top-level unit to which they
265 -- belong.
267 if Nkind (Unit (Cunit (Uspec))) = N_Subunit then
268 return;
269 end if;
271 Traverse_Scopes (CU => Cunit (Uspec), Inside_Stubs => True);
273 -- When two units are present for the same compilation unit, as it
274 -- happens for library-level instantiations of generics, then add all
275 -- scopes to the same SPARK file.
277 if Ubody /= No_Unit then
278 Traverse_Scopes (CU => Cunit (Ubody), Inside_Stubs => True);
279 end if;
281 -- Make entry for new file in file table
283 Get_Name_String (Reference_Name (File));
286 -- For subunits, also retrieve the file name of the unit. Only do so if
287 -- unit has an associated compilation unit.
291 then
294 else
295 Unit_File_Name := null;
296 end if;
298 SPARK_File_Table.Append (
299 (File_Name => File_Name,
300 Unit_File_Name => Unit_File_Name,
301 File_Num => Dspec,
302 From_Scope => From,
303 To_Scope => SPARK_Scope_Table.Last));
304 end Add_SPARK_File;
306 ---------------------
307 -- Add_SPARK_Xrefs --
308 ---------------------
310 procedure Add_SPARK_Xrefs is
311 function Entity_Of_Scope (S : Scope_Index) return Entity_Id;
312 -- Return the entity which maps to the input scope index
314 function Get_Entity_Type (E : Entity_Id) return Character;
315 -- Return a character representing the type of entity
317 function Get_Scope_Num (N : Entity_Id) return Nat;
318 -- Return the scope number associated to entity N
320 function Is_Constant_Object_Without_Variable_Input
321 (E : Entity_Id) return Boolean;
322 -- Return True if E is known to have no variable input, as defined in
323 -- SPARK RM.
325 function Is_Future_Scope_Entity
326 (E : Entity_Id;
327 S : Scope_Index) return Boolean;
328 -- Check whether entity E is in SPARK_Scope_Table at index S or higher
330 function Is_SPARK_Reference
331 (E : Entity_Id;
332 Typ : Character) return Boolean;
333 -- Return whether entity reference E meets SPARK requirements. Typ is
334 -- the reference type.
336 function Is_SPARK_Scope (E : Entity_Id) return Boolean;
337 -- Return whether the entity or reference scope meets requirements for
338 -- being a SPARK scope.
340 function Lt (Op1 : Natural; Op2 : Natural) return Boolean;
341 -- Comparison function for Sort call
343 procedure Move (From : Natural; To : Natural);
344 -- Move procedure for Sort call
346 procedure Set_Scope_Num (N : Entity_Id; Num : Nat);
347 -- Associate entity N to scope number Num
349 procedure Update_Scope_Range
350 (S : Scope_Index;
351 From : Xref_Index;
352 To : Xref_Index);
353 -- Update the scope which maps to S with the new range From .. To
355 package Sorting is new GNAT.Heap_Sort_G (Move, Lt);
357 No_Scope : constant Nat := 0;
358 -- Initial scope counter
360 type Scope_Rec is record
361 Num : Nat;
362 Entity : Entity_Id;
363 end record;
364 -- Type used to relate an entity and a scope number
366 package Scopes is new GNAT.HTable.Simple_HTable
367 (Header_Num => Entity_Hashed_Range,
368 Element => Scope_Rec,
369 No_Element => (Num => No_Scope, Entity => Empty),
370 Key => Entity_Id,
371 Hash => Entity_Hash,
372 Equal => "=");
373 -- Package used to build a correspondence between entities and scope
374 -- numbers used in SPARK cross references.
376 Nrefs : Nat := Xrefs.Last;
377 -- Number of references in table. This value may get reset (reduced)
378 -- when we eliminate duplicate reference entries as well as references
379 -- not suitable for local cross-references.
381 Nrefs_Add : constant Nat := Drefs.Last;
382 -- Number of additional references which correspond to dereferences in
383 -- the source code.
385 Rnums : array (0 .. Nrefs + Nrefs_Add) of Nat;
386 -- This array contains numbers of references in the Xrefs table. This
387 -- list is sorted in output order. The extra 0'th entry is convenient
388 -- for the call to sort. When we sort the table, we move the entries in
389 -- Rnums around, but we do not move the original table entries.
391 ---------------------
392 -- Entity_Of_Scope --
393 ---------------------
395 function Entity_Of_Scope (S : Scope_Index) return Entity_Id is
396 begin
397 return SPARK_Scope_Table.Table (S).Scope_Entity;
398 end Entity_Of_Scope;
400 ---------------------
401 -- Get_Entity_Type --
402 ---------------------
404 function Get_Entity_Type (E : Entity_Id) return Character is
405 begin
406 case Ekind (E) is
411 end case;
412 end Get_Entity_Type;
414 -------------------
415 -- Get_Scope_Num --
416 -------------------
418 function Get_Scope_Num (N : Entity_Id) return Nat is
419 begin
420 return Scopes.Get (N).Num;
421 end Get_Scope_Num;
423 -----------------------------------------------
424 -- Is_Constant_Object_Without_Variable_Input --
425 -----------------------------------------------
427 function Is_Constant_Object_Without_Variable_Input
428 (E : Entity_Id) return Boolean
429 is
430 Result : Boolean;
432 begin
433 case Ekind (E) is
435 -- A constant is known to have no variable input if its
436 -- initializing expression is static (a value which is
437 -- compile-time-known is not guaranteed to have no variable input
438 -- as defined in the SPARK RM). Otherwise, the constant may or not
439 -- have variable input.
441 when E_Constant =>
442 declare
443 Decl : Node_Id;
444 begin
445 if Present (Full_View (E)) then
446 Decl := Parent (Full_View (E));
447 else
448 Decl := Parent (E);
449 end if;
451 if Is_Imported (E) then
452 Result := False;
453 else
454 pragma Assert (Present (Expression (Decl)));
455 Result := Is_Static_Expression (Expression (Decl));
456 end if;
457 end;
459 when E_Loop_Parameter | E_In_Parameter =>
460 Result := True;
462 when others =>
463 Result := False;
464 end case;
466 return Result;
467 end Is_Constant_Object_Without_Variable_Input;
469 ----------------------------
470 -- Is_Future_Scope_Entity --
471 ----------------------------
473 function Is_Future_Scope_Entity
474 (E : Entity_Id;
475 S : Scope_Index) return Boolean
476 is
477 function Is_Past_Scope_Entity return Boolean;
478 -- Check whether entity E is in SPARK_Scope_Table at index strictly
479 -- lower than S.
481 --------------------------
482 -- Is_Past_Scope_Entity --
483 --------------------------
485 function Is_Past_Scope_Entity return Boolean is
486 begin
487 for Index in SPARK_Scope_Table.First .. S - 1 loop
488 if SPARK_Scope_Table.Table (Index).Scope_Entity = E then
489 return True;
490 end if;
491 end loop;
493 return False;
494 end Is_Past_Scope_Entity;
496 -- Start of processing for Is_Future_Scope_Entity
498 begin
499 for Index in S .. SPARK_Scope_Table.Last loop
500 if SPARK_Scope_Table.Table (Index).Scope_Entity = E then
501 return True;
502 end if;
503 end loop;
505 -- If this assertion fails, this means that the scope which we are
506 -- looking for has been treated already, which reveals a problem in
507 -- the order of cross-references.
509 pragma Assert (not Is_Past_Scope_Entity);
511 return False;
512 end Is_Future_Scope_Entity;
514 ------------------------
515 -- Is_SPARK_Reference --
516 ------------------------
518 function Is_SPARK_Reference
519 (E : Entity_Id;
520 Typ : Character) return Boolean
521 is
522 begin
523 -- The only references of interest on callable entities are calls. On
524 -- uncallable entities, the only references of interest are reads and
525 -- writes.
527 if Ekind (E) in Overloadable_Kind then
530 -- Objects of task or protected types are not SPARK references
532 elsif Present (Etype (E))
533 and then Ekind (Etype (E)) in Concurrent_Kind
534 then
535 return False;
537 -- In all other cases, result is true for reference/modify cases,
538 -- and false for all other cases.
540 else
542 end if;
543 end Is_SPARK_Reference;
545 --------------------
546 -- Is_SPARK_Scope --
547 --------------------
549 function Is_SPARK_Scope (E : Entity_Id) return Boolean is
550 begin
551 return Present (E)
552 and then not Is_Generic_Unit (E)
553 and then Renamed_Entity (E) = Empty
554 and then Get_Scope_Num (E) /= No_Scope;
555 end Is_SPARK_Scope;
557 --------
558 -- Lt --
559 --------
561 function Lt (Op1 : Natural; Op2 : Natural) return Boolean is
562 T1 : constant Xref_Entry := Xrefs.Table (Rnums (Nat (Op1)));
563 T2 : constant Xref_Entry := Xrefs.Table (Rnums (Nat (Op2)));
565 begin
566 -- First test: if entity is in different unit, sort by unit. Note:
567 -- that we use Ent_Scope_File rather than Eun, as Eun may refer to
568 -- the file where the generic scope is defined, which may differ from
569 -- the file where the enclosing scope is defined. It is the latter
570 -- which matters for a correct order here.
572 if T1.Ent_Scope_File /= T2.Ent_Scope_File then
573 return Dependency_Num (T1.Ent_Scope_File) <
574 Dependency_Num (T2.Ent_Scope_File);
576 -- Second test: within same unit, sort by location of the scope of
577 -- the entity definition.
579 elsif Get_Scope_Num (T1.Key.Ent_Scope) /=
580 Get_Scope_Num (T2.Key.Ent_Scope)
581 then
582 return Get_Scope_Num (T1.Key.Ent_Scope) <
583 Get_Scope_Num (T2.Key.Ent_Scope);
585 -- Third test: within same unit and scope, sort by location of
586 -- entity definition.
588 elsif T1.Def /= T2.Def then
589 return T1.Def < T2.Def;
591 else
592 -- Both entities must be equal at this point
594 pragma Assert (T1.Key.Ent = T2.Key.Ent);
595 pragma Assert (T1.Key.Ent_Scope = T2.Key.Ent_Scope);
596 pragma Assert (T1.Ent_Scope_File = T2.Ent_Scope_File);
598 -- Fourth test: if reference is in same unit as entity definition,
599 -- sort first.
601 if T1.Key.Lun /= T2.Key.Lun
602 and then T1.Ent_Scope_File = T1.Key.Lun
603 then
604 return True;
606 elsif T1.Key.Lun /= T2.Key.Lun
607 and then T2.Ent_Scope_File = T2.Key.Lun
608 then
609 return False;
611 -- Fifth test: if reference is in same unit and same scope as
612 -- entity definition, sort first.
614 elsif T1.Ent_Scope_File = T1.Key.Lun
615 and then T1.Key.Ref_Scope /= T2.Key.Ref_Scope
616 and then T1.Key.Ent_Scope = T1.Key.Ref_Scope
617 then
618 return True;
620 elsif T2.Ent_Scope_File = T2.Key.Lun
621 and then T1.Key.Ref_Scope /= T2.Key.Ref_Scope
622 and then T2.Key.Ent_Scope = T2.Key.Ref_Scope
623 then
624 return False;
626 -- Sixth test: for same entity, sort by reference location unit
628 elsif T1.Key.Lun /= T2.Key.Lun then
629 return Dependency_Num (T1.Key.Lun) <
630 Dependency_Num (T2.Key.Lun);
632 -- Seventh test: for same entity, sort by reference location scope
634 elsif Get_Scope_Num (T1.Key.Ref_Scope) /=
635 Get_Scope_Num (T2.Key.Ref_Scope)
636 then
637 return Get_Scope_Num (T1.Key.Ref_Scope) <
638 Get_Scope_Num (T2.Key.Ref_Scope);
640 -- Eighth test: order of location within referencing unit
642 elsif T1.Key.Loc /= T2.Key.Loc then
643 return T1.Key.Loc < T2.Key.Loc;
645 -- Finally, for two locations at the same address prefer the one
647 -- extension takes preference, when there are more than one
648 -- reference at the same location. As a result, in the case of
649 -- entities that are in-out actuals, the read reference follows
650 -- the modify reference.
652 else
654 end if;
655 end if;
656 end Lt;
658 ----------
659 -- Move --
660 ----------
662 procedure Move (From : Natural; To : Natural) is
663 begin
664 Rnums (Nat (To)) := Rnums (Nat (From));
665 end Move;
667 -------------------
668 -- Set_Scope_Num --
669 -------------------
671 procedure Set_Scope_Num (N : Entity_Id; Num : Nat) is
672 begin
676 ------------------------
677 -- Update_Scope_Range --
678 ------------------------
680 procedure Update_Scope_Range
684 is
685 begin
690 -- Local variables
702 -- Start of processing for Add_SPARK_Xrefs
704 begin
706 declare
708 begin
713 -- Set up the pointer vector for the sort
726 -- Capture the definition Sloc values. As in the case of normal cross
727 -- references, we have to wait until now to get the correct value.
733 -- Eliminate entries not appropriate for SPARK. Done prior to sorting
734 -- cross-references, as it discards useless references which do not have
735 -- a proper format for the comparison function (like no location).
741 declare
744 begin
751 -- Discard references from unknown scopes, e.g. generic scopes
755 then
762 -- Sort the references
766 -- Eliminate duplicate entries
768 -- We need this test for Ref_Count because if we force ALI file
769 -- generation in case of errors detected, it may be the case that
770 -- Nrefs is 0, so we should not reset it here.
784 -- Eliminate the reference if it is at the same location as the previous
785 -- one, unless it is a read-reference indicating that the entity is an
786 -- in-out actual in a call.
794 declare
797 begin
800 then
809 -- The two steps have eliminated all references, nothing to do
819 -- Loop to output references
822 declare
827 begin
828 -- If this assertion fails, the scope which we are looking for is
829 -- not in SPARK scope table, which reveals either a problem in the
830 -- construction of the scope table, or an erroneous scope for the
831 -- current cross-reference.
835 -- Update the range of cross references to which the current scope
836 -- refers to. This may be the empty range only for the first scope
837 -- considered.
840 Update_Scope_Range
855 end if;
857 if Ref.Ent = Heap then
858 Line := 0;
859 Col := 0;
860 else
861 Line := Nat (Get_Logical_Line_Number (Ref_Entry.Def));
862 Col := Nat (Get_Column_Number (Ref_Entry.Def));
863 end if;
865 -- References to constant objects without variable inputs (see
866 -- SPARK RM 3.3.1) are considered specially in SPARK section,
867 -- because these will be translated as constants in the
868 -- intermediate language for formal verification, and should
869 -- therefore never appear in frame conditions. Other constants may
870 -- later be treated the same, up to GNATprove to decide based on
871 -- its flow analysis.
873 if Is_Constant_Object_Without_Variable_Input (Ref.Ent) then
875 else
876 Typ := Ref.Typ;
877 end if;
879 SPARK_Xref_Table.Append (
880 (Entity_Name => Ref_Name,
881 Entity_Line => Line,
882 Etype => Get_Entity_Type (Ref.Ent),
883 Entity_Col => Col,
884 File_Num => Dependency_Num (Ref.Lun),
885 Scope_Num => Get_Scope_Num (Ref.Ref_Scope),
886 Line => Nat (Get_Logical_Line_Number (Ref.Loc)),
887 Rtype => Typ,
888 Col => Nat (Get_Column_Number (Ref.Loc))));
889 end;
890 end loop;
892 -- Update the range of cross references to which the scope refers to
894 Update_Scope_Range
895 (S => Scope_Id,
896 From => From_Index,
897 To => SPARK_Xref_Table.Last);
898 end Add_SPARK_Xrefs;
900 -------------------------
901 -- Collect_SPARK_Xrefs --
902 -------------------------
904 procedure Collect_SPARK_Xrefs
905 (Sdep_Table : Unit_Ref_Table;
906 Num_Sdep : Nat)
907 is
908 Sdep : Pos;
909 Sdep_Next : Pos;
910 -- Index of the current and next source dependency
912 Sdep_File : Pos;
913 -- Index of the file to which the scopes need to be assigned; for
914 -- library-level instances of generic units this points to the unit
915 -- of the body, because this is where references are assigned to.
917 Ubody : Unit_Number_Type;
918 Uspec : Unit_Number_Type;
919 -- Unit numbers for the dependency spec and possibly its body (only in
920 -- the case of library-level instance of a generic package).
922 begin
923 -- Cross-references should have been computed first
925 pragma Assert (Xrefs.Last /= 0);
927 Initialize_SPARK_Tables;
929 -- Generate file and scope SPARK cross-reference information
931 Sdep := 1;
932 while Sdep <= Num_Sdep loop
934 -- Skip dependencies with no entity node, e.g. configuration files
935 -- with pragmas (.adc) or target description (.atp), since they
936 -- present no interest for SPARK cross references.
938 if No (Cunit_Entity (Sdep_Table (Sdep))) then
939 Sdep_Next := Sdep + 1;
941 -- For library-level instantiation of a generic, two consecutive
942 -- units refer to the same compilation unit node and entity (one to
943 -- body, one to spec). In that case, treat them as a single unit for
944 -- the sake of SPARK cross references by passing to Add_SPARK_File.
946 else
947 if Sdep < Num_Sdep
948 and then Cunit_Entity (Sdep_Table (Sdep)) =
949 Cunit_Entity (Sdep_Table (Sdep + 1))
950 then
951 declare
952 Cunit1 : Node_Id renames Cunit (Sdep_Table (Sdep));
953 Cunit2 : Node_Id renames Cunit (Sdep_Table (Sdep + 1));
955 begin
956 -- Both Cunits point to compilation unit nodes
958 pragma Assert
959 (Nkind (Cunit1) = N_Compilation_Unit
960 and then Nkind (Cunit2) = N_Compilation_Unit);
962 -- Do not depend on the sorting order, which is based on
963 -- Unit_Name, and for library-level instances of nested
964 -- generic packages they are equal.
966 -- If declaration comes before the body
968 if Nkind (Unit (Cunit1)) = N_Package_Declaration
969 and then Nkind (Unit (Cunit2)) = N_Package_Body
970 then
971 Uspec := Sdep_Table (Sdep);
972 Ubody := Sdep_Table (Sdep + 1);
974 Sdep_File := Sdep + 1;
976 -- If body comes before declaration
978 elsif Nkind (Unit (Cunit1)) = N_Package_Body
979 and then Nkind (Unit (Cunit2)) = N_Package_Declaration
980 then
981 Uspec := Sdep_Table (Sdep + 1);
982 Ubody := Sdep_Table (Sdep);
984 Sdep_File := Sdep;
986 -- Otherwise it is an error
988 else
989 raise Program_Error;
990 end if;
992 Sdep_Next := Sdep + 2;
993 end;
995 -- ??? otherwise?
997 else
998 Uspec := Sdep_Table (Sdep);
999 Ubody := No_Unit;
1001 Sdep_File := Sdep;
1002 Sdep_Next := Sdep + 1;
1003 end if;
1005 Add_SPARK_File
1006 (Uspec => Uspec,
1007 Ubody => Ubody,
1008 Dspec => Sdep_File);
1009 end if;
1011 Sdep := Sdep_Next;
1012 end loop;
1014 -- Fill in the spec information when relevant
1016 declare
1017 package Entity_Hash_Table is new
1018 GNAT.HTable.Simple_HTable
1019 (Header_Num => Entity_Hashed_Range,
1020 Element => Scope_Index,
1021 No_Element => 0,
1022 Key => Entity_Id,
1023 Hash => Entity_Hash,
1024 Equal => "=");
1026 begin
1027 -- Fill in the hash-table
1029 for S in SPARK_Scope_Table.First .. SPARK_Scope_Table.Last loop
1030 declare
1031 Srec : SPARK_Scope_Record renames SPARK_Scope_Table.Table (S);
1032 begin
1033 Entity_Hash_Table.Set (Srec.Scope_Entity, S);
1034 end;
1035 end loop;
1037 -- Use the hash-table to locate spec entities
1039 for S in SPARK_Scope_Table.First .. SPARK_Scope_Table.Last loop
1040 declare
1041 Srec : SPARK_Scope_Record renames SPARK_Scope_Table.Table (S);
1043 Spec_Entity : constant Entity_Id :=
1044 Unique_Entity (Srec.Scope_Entity);
1045 Spec_Scope : constant Scope_Index :=
1046 Entity_Hash_Table.Get (Spec_Entity);
1048 begin
1049 -- Generic spec may be missing in which case Spec_Scope is zero
1051 if Spec_Entity /= Srec.Scope_Entity
1052 and then Spec_Scope /= 0
1053 then
1054 Srec.Spec_File_Num :=
1055 SPARK_Scope_Table.Table (Spec_Scope).File_Num;
1056 Srec.Spec_Scope_Num :=
1057 SPARK_Scope_Table.Table (Spec_Scope).Scope_Num;
1058 end if;
1059 end;
1060 end loop;
1061 end;
1063 -- Generate SPARK cross-reference information
1065 Add_SPARK_Xrefs;
1066 end Collect_SPARK_Xrefs;
1068 -------------------------------------
1069 -- Enclosing_Subprogram_Or_Package --
1070 -------------------------------------
1072 function Enclosing_Subprogram_Or_Library_Package
1073 (N : Node_Id) return Entity_Id
1074 is
1075 Context : Entity_Id;
1077 begin
1078 -- If N is the defining identifier for a subprogram, then return the
1079 -- enclosing subprogram or package, not this subprogram.
1081 if Nkind_In (N, N_Defining_Identifier, N_Defining_Operator_Symbol)
1082 and then (Ekind (N) in Entry_Kind
1083 or else Ekind (N) = E_Subprogram_Body
1084 or else Ekind (N) in Generic_Subprogram_Kind
1085 or else Ekind (N) in Subprogram_Kind)
1086 then
1087 Context := Parent (Unit_Declaration_Node (N));
1089 -- If this was a library-level subprogram then replace Context with
1090 -- its Unit, which points to N_Subprogram_* node.
1092 if Nkind (Context) = N_Compilation_Unit then
1093 Context := Unit (Context);
1094 end if;
1095 else
1096 Context := N;
1097 end if;
1099 while Present (Context) loop
1100 case Nkind (Context) is
1101 when N_Package_Body |
1102 N_Package_Specification =>
1104 -- Only return a library-level package
1106 if Is_Library_Level_Entity (Defining_Entity (Context)) then
1107 Context := Defining_Entity (Context);
1108 exit;
1109 else
1110 Context := Parent (Context);
1111 end if;
1113 when N_Pragma =>
1115 -- The enclosing subprogram for a precondition, postcondition,
1116 -- or contract case should be the declaration preceding the
1117 -- pragma (skipping any other pragmas between this pragma and
1118 -- this declaration.
1120 while Nkind (Context) = N_Pragma
1121 and then Is_List_Member (Context)
1122 and then Present (Prev (Context))
1123 loop
1124 Context := Prev (Context);
1125 end loop;
1127 if Nkind (Context) = N_Pragma then
1128 Context := Parent (Context);
1129 end if;
1131 when N_Entry_Body |
1132 N_Entry_Declaration |
1133 N_Protected_Type_Declaration |
1134 N_Subprogram_Body |
1135 N_Subprogram_Declaration |
1136 N_Subprogram_Specification |
1137 N_Task_Body |
1138 N_Task_Type_Declaration =>
1139 Context := Defining_Entity (Context);
1140 exit;
1142 when others =>
1143 Context := Parent (Context);
1144 end case;
1145 end loop;
1147 if Nkind (Context) = N_Defining_Program_Unit_Name then
1148 Context := Defining_Identifier (Context);
1149 end if;
1151 -- Do not return a scope without a proper location
1153 if Present (Context)
1154 and then Sloc (Context) = No_Location
1155 then
1156 return Empty;
1157 end if;
1159 return Context;
1160 end Enclosing_Subprogram_Or_Library_Package;
1162 -----------------
1163 -- Entity_Hash --
1164 -----------------
1166 function Entity_Hash (E : Entity_Id) return Entity_Hashed_Range is
1167 begin
1168 return
1169 Entity_Hashed_Range (E mod (Entity_Id (Entity_Hashed_Range'Last) + 1));
1170 end Entity_Hash;
1172 --------------------------
1173 -- Generate_Dereference --
1174 --------------------------
1176 procedure Generate_Dereference
1177 (N : Node_Id;
1179 is
1180 procedure Create_Heap;
1181 -- Create and decorate the special entity which denotes the heap
1183 -----------------
1184 -- Create_Heap --
1185 -----------------
1187 procedure Create_Heap is
1188 begin
1189 Name_Len := Name_Of_Heap_Variable'Length;
1190 Name_Buffer (1 .. Name_Len) := Name_Of_Heap_Variable;
1192 Heap := Make_Defining_Identifier (Standard_Location, Name_Enter);
1194 Set_Ekind (Heap, E_Variable);
1195 Set_Is_Internal (Heap, True);
1196 Set_Has_Fully_Qualified_Name (Heap);
1197 end Create_Heap;
1199 -- Local variables
1201 Loc : constant Source_Ptr := Sloc (N);
1203 -- Start of processing for Generate_Dereference
1205 begin
1206 if Loc > No_Location then
1207 Drefs.Increment_Last;
1209 declare
1210 Deref_Entry : Xref_Entry renames Drefs.Table (Drefs.Last);
1211 Deref : Xref_Key renames Deref_Entry.Key;
1213 begin
1214 if No (Heap) then
1215 Create_Heap;
1216 end if;
1218 Deref.Ent := Heap;
1219 Deref.Loc := Loc;
1220 Deref.Typ := Typ;
1222 -- It is as if the special "Heap" was defined in the main unit,
1223 -- in the scope of the entity for the main unit. This single
1224 -- definition point is required to ensure that sorting cross
1225 -- references works for "Heap" references as well.
1227 Deref.Eun := Main_Unit;
1228 Deref.Lun := Get_Top_Level_Code_Unit (Loc);
1230 Deref.Ref_Scope := Enclosing_Subprogram_Or_Library_Package (N);
1231 Deref.Ent_Scope := Cunit_Entity (Main_Unit);
1233 Deref_Entry.Def := No_Location;
1235 Deref_Entry.Ent_Scope_File := Main_Unit;
1236 end;
1237 end if;
1238 end Generate_Dereference;
1240 -------------------------------
1241 -- Traverse_Compilation_Unit --
1242 -------------------------------
1244 procedure Traverse_Compilation_Unit
1245 (CU : Node_Id;
1246 Inside_Stubs : Boolean)
1247 is
1248 procedure Traverse_Block (N : Node_Id);
1249 procedure Traverse_Declaration_Or_Statement (N : Node_Id);
1250 procedure Traverse_Declarations_And_HSS (N : Node_Id);
1251 procedure Traverse_Declarations_Or_Statements (L : List_Id);
1252 procedure Traverse_Handled_Statement_Sequence (N : Node_Id);
1253 procedure Traverse_Package_Body (N : Node_Id);
1254 procedure Traverse_Visible_And_Private_Parts (N : Node_Id);
1255 procedure Traverse_Protected_Body (N : Node_Id);
1256 procedure Traverse_Subprogram_Body (N : Node_Id);
1257 procedure Traverse_Task_Body (N : Node_Id);
1259 -- Traverse corresponding construct, calling Process on all declarations
1261 --------------------
1262 -- Traverse_Block --
1263 --------------------
1265 procedure Traverse_Block (N : Node_Id) renames
1266 Traverse_Declarations_And_HSS;
1268 ---------------------------------------
1269 -- Traverse_Declaration_Or_Statement --
1270 ---------------------------------------
1272 procedure Traverse_Declaration_Or_Statement (N : Node_Id) is
1273 begin
1274 case Nkind (N) is
1275 when N_Package_Declaration =>
1276 Traverse_Visible_And_Private_Parts (Specification (N));
1278 when N_Package_Body =>
1279 if Ekind (Defining_Entity (N)) /= E_Generic_Package then
1280 Traverse_Package_Body (N);
1281 end if;
1283 when N_Package_Body_Stub =>
1284 if Present (Library_Unit (N)) then
1285 declare
1286 Body_N : constant Node_Id := Get_Body_From_Stub (N);
1287 begin
1288 if Inside_Stubs
1289 and then Ekind (Defining_Entity (Body_N)) /=
1290 E_Generic_Package
1291 then
1292 Traverse_Package_Body (Body_N);
1293 end if;
1294 end;
1295 end if;
1297 when N_Subprogram_Body =>
1298 if not Is_Generic_Subprogram (Defining_Entity (N)) then
1299 Traverse_Subprogram_Body (N);
1300 end if;
1302 when N_Entry_Body =>
1303 Traverse_Subprogram_Body (N);
1305 when N_Subprogram_Body_Stub =>
1306 if Present (Library_Unit (N)) then
1307 declare
1308 Body_N : constant Node_Id := Get_Body_From_Stub (N);
1309 begin
1310 if Inside_Stubs
1311 and then
1312 not Is_Generic_Subprogram (Defining_Entity (Body_N))
1313 then
1314 Traverse_Subprogram_Body (Body_N);
1315 end if;
1316 end;
1317 end if;
1319 when N_Protected_Body =>
1320 Traverse_Protected_Body (N);
1322 when N_Protected_Body_Stub =>
1323 if Present (Library_Unit (N)) and then Inside_Stubs then
1324 Traverse_Protected_Body (Get_Body_From_Stub (N));
1325 end if;
1327 when N_Protected_Type_Declaration |
1328 N_Single_Protected_Declaration =>
1329 Traverse_Visible_And_Private_Parts (Protected_Definition (N));
1331 when N_Task_Definition =>
1332 Traverse_Visible_And_Private_Parts (N);
1334 when N_Task_Body =>
1335 Traverse_Task_Body (N);
1337 when N_Task_Body_Stub =>
1338 if Present (Library_Unit (N)) and then Inside_Stubs then
1339 Traverse_Task_Body (Get_Body_From_Stub (N));
1340 end if;
1342 when N_Block_Statement =>
1343 Traverse_Block (N);
1345 when N_If_Statement =>
1347 -- Traverse the statements in the THEN part
1349 Traverse_Declarations_Or_Statements (Then_Statements (N));
1351 -- Loop through ELSIF parts if present
1353 if Present (Elsif_Parts (N)) then
1354 declare
1355 Elif : Node_Id := First (Elsif_Parts (N));
1357 begin
1358 while Present (Elif) loop
1359 Traverse_Declarations_Or_Statements
1360 (Then_Statements (Elif));
1361 Next (Elif);
1362 end loop;
1363 end;
1364 end if;
1366 -- Finally traverse the ELSE statements if present
1368 Traverse_Declarations_Or_Statements (Else_Statements (N));
1370 when N_Case_Statement =>
1372 -- Process case branches
1374 declare
1375 Alt : Node_Id;
1376 begin
1377 Alt := First (Alternatives (N));
1378 while Present (Alt) loop
1379 Traverse_Declarations_Or_Statements (Statements (Alt));
1380 Next (Alt);
1381 end loop;
1382 end;
1384 when N_Extended_Return_Statement =>
1385 Traverse_Handled_Statement_Sequence
1386 (Handled_Statement_Sequence (N));
1388 when N_Loop_Statement =>
1389 Traverse_Declarations_Or_Statements (Statements (N));
1391 -- Generic declarations are ignored
1393 when others =>
1394 null;
1395 end case;
1396 end Traverse_Declaration_Or_Statement;
1398 -----------------------------------
1399 -- Traverse_Declarations_And_HSS --
1400 -----------------------------------
1402 procedure Traverse_Declarations_And_HSS (N : Node_Id) is
1403 begin
1404 Traverse_Declarations_Or_Statements (Declarations (N));
1405 Traverse_Handled_Statement_Sequence (Handled_Statement_Sequence (N));
1406 end Traverse_Declarations_And_HSS;
1408 -----------------------------------------
1409 -- Traverse_Declarations_Or_Statements --
1410 -----------------------------------------
1412 procedure Traverse_Declarations_Or_Statements (L : List_Id) is
1413 N : Node_Id;
1415 begin
1416 -- Loop through statements or declarations
1418 N := First (L);
1419 while Present (N) loop
1421 -- Call Process on all declarations
1423 if Nkind (N) in N_Declaration
1424 or else Nkind (N) in N_Later_Decl_Item
1425 or else Nkind (N) = N_Entry_Body
1426 then
1427 Process (N);
1428 end if;
1430 Traverse_Declaration_Or_Statement (N);
1432 Next (N);
1433 end loop;
1434 end Traverse_Declarations_Or_Statements;
1436 -----------------------------------------
1437 -- Traverse_Handled_Statement_Sequence --
1438 -----------------------------------------
1440 procedure Traverse_Handled_Statement_Sequence (N : Node_Id) is
1441 Handler : Node_Id;
1443 begin
1444 if Present (N) then
1445 Traverse_Declarations_Or_Statements (Statements (N));
1447 if Present (Exception_Handlers (N)) then
1448 Handler := First (Exception_Handlers (N));
1449 while Present (Handler) loop
1450 Traverse_Declarations_Or_Statements (Statements (Handler));
1451 Next (Handler);
1452 end loop;
1453 end if;
1454 end if;
1455 end Traverse_Handled_Statement_Sequence;
1457 ---------------------------
1458 -- Traverse_Package_Body --
1459 ---------------------------
1461 procedure Traverse_Package_Body (N : Node_Id) renames
1462 Traverse_Declarations_And_HSS;
1464 -----------------------------
1465 -- Traverse_Protected_Body --
1466 -----------------------------
1468 procedure Traverse_Protected_Body (N : Node_Id) is
1469 begin
1470 Traverse_Declarations_Or_Statements (Declarations (N));
1471 end Traverse_Protected_Body;
1473 ------------------------------
1474 -- Traverse_Subprogram_Body --
1475 ------------------------------
1477 procedure Traverse_Subprogram_Body (N : Node_Id) renames
1478 Traverse_Declarations_And_HSS;
1480 ------------------------
1481 -- Traverse_Task_Body --
1482 ------------------------
1484 procedure Traverse_Task_Body (N : Node_Id) renames
1485 Traverse_Declarations_And_HSS;
1487 ----------------------------------------
1488 -- Traverse_Visible_And_Private_Parts --
1489 ----------------------------------------
1491 procedure Traverse_Visible_And_Private_Parts (N : Node_Id) is
1492 begin
1493 Traverse_Declarations_Or_Statements (Visible_Declarations (N));
1494 Traverse_Declarations_Or_Statements (Private_Declarations (N));
1495 end Traverse_Visible_And_Private_Parts;
1497 -- Local variables
1499 Lu : Node_Id;
1501 -- Start of processing for Traverse_Compilation_Unit
1503 begin
1504 -- Get Unit (checking case of subunit)
1506 Lu := Unit (CU);
1508 if Nkind (Lu) = N_Subunit then
1509 Lu := Proper_Body (Lu);
1510 end if;
1512 -- Do not add scopes for generic units
1514 if Nkind (Lu) = N_Package_Body
1515 and then Ekind (Corresponding_Spec (Lu)) in Generic_Unit_Kind
1516 then
1517 return;
1518 end if;
1520 -- Call Process on all declarations
1522 if Nkind (Lu) in N_Declaration
1523 or else Nkind (Lu) in N_Later_Decl_Item
1524 then
1525 Process (Lu);
1526 end if;
1528 -- Traverse the unit
1530 Traverse_Declaration_Or_Statement (Lu);
1531 end Traverse_Compilation_Unit;
1533 end SPARK_Specific;