From cfd0a3db624f0dcc1461d256c78e532ee5e01b83 Mon Sep 17 00:00:00 2001 From: pmderodat Date: Wed, 8 Nov 2017 15:17:43 +0000 Subject: gcc/ada/ 2017-11-08 Javier Miranda * sem_disp.adb (Is_Inherited_Public_Operation): Extend the functionality of this routine to handle multiple levels of derivations. 2017-11-08 Hristian Kirtchev * einfo.adb: Elist36 is now used as Nested_Scenarios. (Nested_Scenarios): New routine. (Set_Nested_Scenarios): New routine. (Write_Field36_Name): New routine. * einfo.ads: Add new attribute Nested_Scenarios along with occurrences in entities. (Nested_Scenarios): New routine along with pragma Inline. (Set_Nested_Scenarios): New routine along with pragma Inline. * sem_elab.adb (Find_And_Process_Nested_Scenarios): New routine. (Process_Nested_Scenarios): New routine. (Traverse_Body): When a subprogram body is traversed for the first time, find, save, and process all suitable scenarios found within. Subsequent traversals of the same subprogram body utilize the saved scenarios. 2017-11-08 Piotr Trojanek * lib-xref-spark_specific.adb (Add_SPARK_Scope): Remove detection of protected operations. (Add_SPARK_Xrefs): Simplify detection of empty entities. * get_spark_xrefs.ads, get_spark_xrefs.adb, put_spark_xrefs.ads, put_spark_xrefs.adb, spark_xrefs_test.adb: Remove code for writing, reading and testing SPARK cross-references stored in the ALI files. * lib-xref.ads (Output_SPARK_Xrefs): Remove. * lib-writ.adb (Write_ALI): Do not write SPARK cross-references to the ALI file. * spark_xrefs.ads, spark_xrefs.adb (pspark): Remove, together with description of the SPARK xrefs ALI format. * gcc-interface/Make-lang.in (GNAT_ADA_OBJS): Remove get_spark_refs.o and put_spark_refs.o. 2017-11-08 Hristian Kirtchev * exp_ch4.adb (Apply_Accessibility_Check): Do not finalize the object when the associated access type is subject to pragma No_Heap_Finalization. * exp_intr.adb (Expand_Unc_Deallocation): Use the available view of the designated type in case it comes from a limited withed unit. gcc/testsuite/ 2017-11-08 Javier Miranda * gnat.dg/overriding_ops2.adb, gnat.dg/overriding_ops2.ads, gnat.dg/overriding_ops2_pkg.ads, gnat.dg/overriding_ops2_pkg-high.ads: New testcase. git-svn-id: svn+ssh://gcc.gnu.org/svn/gcc/trunk@254532 138bc75d-0d04-0410-961f-82ee72b054a4 --- gcc/ada/lib-xref-spark_specific.adb | 21 +++------------------ 1 file changed, 3 insertions(+), 18 deletions(-) (limited to 'gcc/ada/lib-xref-spark_specific.adb') diff --git a/gcc/ada/lib-xref-spark_specific.adb b/gcc/ada/lib-xref-spark_specific.adb index 4d221749907..c3bad8d784d 100644 --- a/gcc/ada/lib-xref-spark_specific.adb +++ b/gcc/ada/lib-xref-spark_specific.adb @@ -139,30 +139,17 @@ package body SPARK_Specific is case Ekind (E) is when E_Entry | E_Entry_Family + | E_Function | E_Generic_Function | E_Generic_Package | E_Generic_Procedure | E_Package + | E_Procedure | E_Protected_Type | E_Task_Type => Typ := Xref_Entity_Letters (Ekind (E)); - when E_Function - | E_Procedure - => - -- In SPARK we need to distinguish protected functions and - -- procedures from ordinary subprograms, but there are no - -- special Xref letters for them. Since this distiction is - -- only needed to detect protected calls, we pretend that - -- such calls are entry calls. - - if Ekind (Scope (E)) = E_Protected_Type then - Typ := Xref_Entity_Letters (E_Entry); - else - Typ := Xref_Entity_Letters (Ekind (E)); - end if; - when E_Package_Body | E_Protected_Body | E_Subprogram_Body @@ -670,7 +657,6 @@ package body SPARK_Specific is Prev_Loc : Source_Ptr; Prev_Typ : Character; Ref_Count : Nat; - Ref_Id : Entity_Id; Ref_Name : String_Ptr; Scope_Id : Scope_Index; @@ -795,7 +781,6 @@ package body SPARK_Specific is return; end if; - Ref_Id := Empty; Scope_Id := 1; From_Index := 1; @@ -833,7 +818,7 @@ package body SPARK_Specific is pragma Assert (Scope_Id <= SPARK_Scope_Table.Last); end loop; - if Ref.Ent /= Ref_Id then + if Present (Ref.Ent) then Ref_Name := new String'(Unique_Name (Ref.Ent)); end if; -- cgit v1.2.1 From 3e3c72d45fd4d57d18e084100b5177c537a92adb Mon Sep 17 00:00:00 2001 From: pmderodat Date: Wed, 8 Nov 2017 15:38:51 +0000 Subject: 2017-11-08 Piotr Trojanek * lib-xref-spark_specific.adb (Add_SPARK_Xrefs): Remove dead check for empty entities. git-svn-id: svn+ssh://gcc.gnu.org/svn/gcc/trunk@254535 138bc75d-0d04-0410-961f-82ee72b054a4 --- gcc/ada/lib-xref-spark_specific.adb | 7 +------ 1 file changed, 1 insertion(+), 6 deletions(-) (limited to 'gcc/ada/lib-xref-spark_specific.adb') diff --git a/gcc/ada/lib-xref-spark_specific.adb b/gcc/ada/lib-xref-spark_specific.adb index c3bad8d784d..48377185ebf 100644 --- a/gcc/ada/lib-xref-spark_specific.adb +++ b/gcc/ada/lib-xref-spark_specific.adb @@ -657,7 +657,6 @@ package body SPARK_Specific is Prev_Loc : Source_Ptr; Prev_Typ : Character; Ref_Count : Nat; - Ref_Name : String_Ptr; Scope_Id : Scope_Index; -- Start of processing for Add_SPARK_Xrefs @@ -818,10 +817,6 @@ package body SPARK_Specific is pragma Assert (Scope_Id <= SPARK_Scope_Table.Last); end loop; - if Present (Ref.Ent) then - Ref_Name := new String'(Unique_Name (Ref.Ent)); - end if; - if Ref.Ent = Heap then Line := 0; Col := 0; @@ -845,7 +840,7 @@ package body SPARK_Specific is end if; SPARK_Xref_Table.Append ( - (Entity_Name => Ref_Name, + (Entity_Name => new String'(Unique_Name (Ref.Ent)), Entity_Line => Line, Etype => Get_Entity_Type (Ref.Ent), Entity_Col => Col, -- cgit v1.2.1 From e81f4fdaca5b523b4cd35e00a023dfbbf98f539c Mon Sep 17 00:00:00 2001 From: pmderodat Date: Wed, 8 Nov 2017 15:48:46 +0000 Subject: 2017-11-08 Piotr Trojanek * spark_xrefs.ads (SPARK_Xref_Record): Remove inessential components. (SPARK_Scope_Record): Remove inessential components. * spark_xrefs.adb (dspark): Remove pretty-printing of removed record components. * lib-xref-spark_specific.adb (Add_SPARK_Scope): Remove setting of removed record components. (Add_SPARK_Xrefs): Remove setting of removed record components. git-svn-id: svn+ssh://gcc.gnu.org/svn/gcc/trunk@254538 138bc75d-0d04-0410-961f-82ee72b054a4 --- gcc/ada/lib-xref-spark_specific.adb | 57 ++++--------------------------------- 1 file changed, 6 insertions(+), 51 deletions(-) (limited to 'gcc/ada/lib-xref-spark_specific.adb') diff --git a/gcc/ada/lib-xref-spark_specific.adb b/gcc/ada/lib-xref-spark_specific.adb index 48377185ebf..395071976a0 100644 --- a/gcc/ada/lib-xref-spark_specific.adb +++ b/gcc/ada/lib-xref-spark_specific.adb @@ -120,14 +120,7 @@ package body SPARK_Specific is --------------------- procedure Add_SPARK_Scope (N : Node_Id) is - E : constant Entity_Id := Defining_Entity (N); - Loc : constant Source_Ptr := Sloc (E); - - -- The character describing the kind of scope is chosen to be the - -- same as the one describing the corresponding entity in cross - -- references, see Xref_Entity_Letters in lib-xrefs.ads - - Typ : Character; + E : constant Entity_Id := Defining_Entity (N); begin -- Ignore scopes without a proper location @@ -144,18 +137,15 @@ package body SPARK_Specific is | E_Generic_Package | E_Generic_Procedure | E_Package + | E_Package_Body | E_Procedure + | E_Protected_Body | E_Protected_Type + | E_Task_Body | E_Task_Type - => - Typ := Xref_Entity_Letters (Ekind (E)); - - when E_Package_Body - | E_Protected_Body | E_Subprogram_Body - | E_Task_Body => - Typ := Xref_Entity_Letters (Ekind (Unique_Entity (E))); + null; when E_Void => @@ -179,9 +169,6 @@ package body SPARK_Specific is Scope_Num => Scope_Id, Spec_File_Num => 0, Spec_Scope_Num => 0, - Line => Nat (Get_Logical_Line_Number (Loc)), - Stype => Typ, - Col => Nat (Get_Column_Number (Loc)), From_Xref => 1, To_Xref => 0, Scope_Entity => E)); @@ -290,9 +277,6 @@ package body SPARK_Specific is function Entity_Of_Scope (S : Scope_Index) return Entity_Id; -- Return the entity which maps to the input scope index - function Get_Entity_Type (E : Entity_Id) return Character; - -- Return a character representing the type of entity - function Get_Scope_Num (E : Entity_Id) return Nat; -- Return the scope number associated with the entity E @@ -370,20 +354,6 @@ package body SPARK_Specific is return SPARK_Scope_Table.Table (S).Scope_Entity; end Entity_Of_Scope; - --------------------- - -- Get_Entity_Type -- - --------------------- - - function Get_Entity_Type (E : Entity_Id) return Character is - begin - case Ekind (E) is - when E_Out_Parameter => return '<'; - when E_In_Out_Parameter => return '='; - when E_In_Parameter => return '>'; - when others => return '*'; - end case; - end Get_Entity_Type; - ------------------- -- Get_Scope_Num -- ------------------- @@ -651,9 +621,7 @@ package body SPARK_Specific is -- Local variables - Col : Nat; From_Index : Xref_Index; - Line : Nat; Prev_Loc : Source_Ptr; Prev_Typ : Character; Ref_Count : Nat; @@ -817,14 +785,6 @@ package body SPARK_Specific is pragma Assert (Scope_Id <= SPARK_Scope_Table.Last); end loop; - if Ref.Ent = Heap then - Line := 0; - Col := 0; - else - Line := Nat (Get_Logical_Line_Number (Ref_Entry.Def)); - Col := Nat (Get_Column_Number (Ref_Entry.Def)); - end if; - -- References to constant objects without variable inputs (see -- SPARK RM 3.3.1) are considered specially in SPARK section, -- because these will be translated as constants in the @@ -841,14 +801,9 @@ package body SPARK_Specific is SPARK_Xref_Table.Append ( (Entity_Name => new String'(Unique_Name (Ref.Ent)), - Entity_Line => Line, - Etype => Get_Entity_Type (Ref.Ent), - Entity_Col => Col, File_Num => Dependency_Num (Ref.Lun), Scope_Num => Get_Scope_Num (Ref.Ref_Scope), - Line => Nat (Get_Logical_Line_Number (Ref.Loc)), - Rtype => Typ, - Col => Nat (Get_Column_Number (Ref.Loc)))); + Rtype => Typ)); end; end loop; -- cgit v1.2.1 From 93230fa5507de91ec3b193fe04d789a9cb493a91 Mon Sep 17 00:00:00 2001 From: pmderodat Date: Wed, 8 Nov 2017 16:04:35 +0000 Subject: 2017-11-08 Piotr Trojanek * spark_xrefs.ads (SPARK_Xref_Record): Referenced object is now represented by Entity_Id. (SPARK_Scope_Record): Referenced scope (e.g. subprogram) is now represented by Entity_Id; this information is not repeated as Scope_Entity. (Heap): Moved from lib-xref-spark_specific.adb, to reside next to Name_Of_Heap_Variable. * spark_xrefs.adb (dspark): Adapt debug routine to above changes in data types. * lib-xref-spark_specific.adb: Adapt routines for populating SPARK scope and xrefs tables to above changes in data types. 2017-11-08 Justin Squirek * sem_ch8.adb (Mark_Use_Clauses): Add condition to always mark the primitives of generic actuals. (Mark_Use_Type): Add recursive call to properly mark class-wide type's base type clauses as per ARM 8.4 (8.2/3). 2017-11-08 Ed Schonberg * sem_ch6.adb (Analyze_Generic_Subprobram_Body): Validate categorization dependency of the body, as is done for non-generic units. (New_Overloaded_Entity, Visible_Part_Type): Remove linear search through declarations (Simple optimization, no behavior change). git-svn-id: svn+ssh://gcc.gnu.org/svn/gcc/trunk@254539 138bc75d-0d04-0410-961f-82ee72b054a4 --- gcc/ada/lib-xref-spark_specific.adb | 30 +++++++++++++----------------- 1 file changed, 13 insertions(+), 17 deletions(-) (limited to 'gcc/ada/lib-xref-spark_specific.adb') diff --git a/gcc/ada/lib-xref-spark_specific.adb b/gcc/ada/lib-xref-spark_specific.adb index 395071976a0..1b31c6acd11 100644 --- a/gcc/ada/lib-xref-spark_specific.adb +++ b/gcc/ada/lib-xref-spark_specific.adb @@ -66,9 +66,6 @@ package body SPARK_Specific is -- Local Variables -- --------------------- - Heap : Entity_Id := Empty; - -- A special entity which denotes the heap object - package Drefs is new Table.Table ( Table_Component_Type => Xref_Entry, Table_Index_Type => Xref_Entry_Number, @@ -164,14 +161,13 @@ package body SPARK_Specific is -- range. SPARK_Scope_Table.Append - ((Scope_Name => new String'(Unique_Name (E)), + ((Scope_Id => E, File_Num => Dspec, Scope_Num => Scope_Id, Spec_File_Num => 0, Spec_Scope_Num => 0, From_Xref => 1, - To_Xref => 0, - Scope_Entity => E)); + To_Xref => 0)); Scope_Id := Scope_Id + 1; end Add_SPARK_Scope; @@ -351,7 +347,7 @@ package body SPARK_Specific is function Entity_Of_Scope (S : Scope_Index) return Entity_Id is begin - return SPARK_Scope_Table.Table (S).Scope_Entity; + return SPARK_Scope_Table.Table (S).Scope_Id; end Entity_Of_Scope; ------------------- @@ -423,7 +419,7 @@ package body SPARK_Specific is function Is_Past_Scope_Entity return Boolean is begin for Index in SPARK_Scope_Table.First .. S - 1 loop - if SPARK_Scope_Table.Table (Index).Scope_Entity = E then + if SPARK_Scope_Table.Table (Index).Scope_Id = E then return True; end if; end loop; @@ -435,7 +431,7 @@ package body SPARK_Specific is begin for Index in S .. SPARK_Scope_Table.Last loop - if SPARK_Scope_Table.Table (Index).Scope_Entity = E then + if SPARK_Scope_Table.Table (Index).Scope_Id = E then return True; end if; end loop; @@ -634,7 +630,7 @@ package body SPARK_Specific is declare S : SPARK_Scope_Record renames SPARK_Scope_Table.Table (Index); begin - Set_Scope_Num (S.Scope_Entity, S.Scope_Num); + Set_Scope_Num (S.Scope_Id, S.Scope_Num); end; end loop; @@ -800,10 +796,10 @@ package body SPARK_Specific is end if; SPARK_Xref_Table.Append ( - (Entity_Name => new String'(Unique_Name (Ref.Ent)), - File_Num => Dependency_Num (Ref.Lun), - Scope_Num => Get_Scope_Num (Ref.Ref_Scope), - Rtype => Typ)); + (Entity => Unique_Entity (Ref.Ent), + File_Num => Dependency_Num (Ref.Lun), + Scope_Num => Get_Scope_Num (Ref.Ref_Scope), + Rtype => Typ)); end; end loop; @@ -948,7 +944,7 @@ package body SPARK_Specific is declare Srec : SPARK_Scope_Record renames SPARK_Scope_Table.Table (S); begin - Entity_Hash_Table.Set (Srec.Scope_Entity, S); + Entity_Hash_Table.Set (Srec.Scope_Id, S); end; end loop; @@ -959,14 +955,14 @@ package body SPARK_Specific is Srec : SPARK_Scope_Record renames SPARK_Scope_Table.Table (S); Spec_Entity : constant Entity_Id := - Unique_Entity (Srec.Scope_Entity); + Unique_Entity (Srec.Scope_Id); Spec_Scope : constant Scope_Index := Entity_Hash_Table.Get (Spec_Entity); begin -- Generic spec may be missing in which case Spec_Scope is zero - if Spec_Entity /= Srec.Scope_Entity + if Spec_Entity /= Srec.Scope_Id and then Spec_Scope /= 0 then Srec.Spec_File_Num := -- cgit v1.2.1 From 0d6ffbcc2866af9d148b206fd26b885bfe471759 Mon Sep 17 00:00:00 2001 From: pmderodat Date: Wed, 8 Nov 2017 16:16:04 +0000 Subject: 2017-11-08 Piotr Trojanek * lib-xref.ads, lib-xref-spark_specific.adb (Traverse_Declarations): Remove Inside_Stubs parameter. git-svn-id: svn+ssh://gcc.gnu.org/svn/gcc/trunk@254540 138bc75d-0d04-0410-961f-82ee72b054a4 --- gcc/ada/lib-xref-spark_specific.adb | 11 ++++------- 1 file changed, 4 insertions(+), 7 deletions(-) (limited to 'gcc/ada/lib-xref-spark_specific.adb') diff --git a/gcc/ada/lib-xref-spark_specific.adb b/gcc/ada/lib-xref-spark_specific.adb index 1b31c6acd11..c43cbb15ced 100644 --- a/gcc/ada/lib-xref-spark_specific.adb +++ b/gcc/ada/lib-xref-spark_specific.adb @@ -230,14 +230,14 @@ package body SPARK_Specific is return; end if; - Traverse_Scopes (CU => Cunit (Uspec), Inside_Stubs => True); + Traverse_Scopes (CU => Cunit (Uspec)); -- When two units are present for the same compilation unit, as it -- happens for library-level instantiations of generics, then add all -- scopes to the same SPARK file. if Ubody /= No_Unit then - Traverse_Scopes (CU => Cunit (Ubody), Inside_Stubs => True); + Traverse_Scopes (CU => Cunit (Ubody)); end if; -- Make entry for new file in file table @@ -1156,10 +1156,7 @@ package body SPARK_Specific is -- Traverse_Compilation_Unit -- ------------------------------- - procedure Traverse_Compilation_Unit - (CU : Node_Id; - Inside_Stubs : Boolean) - is + procedure Traverse_Compilation_Unit (CU : Node_Id) is procedure Traverse_Block (N : Node_Id); procedure Traverse_Declaration_Or_Statement (N : Node_Id); procedure Traverse_Declarations_And_HSS (N : Node_Id); @@ -1195,7 +1192,7 @@ package body SPARK_Specific is N_Subprogram_Body_Stub, N_Task_Body_Stub)); - return Inside_Stubs and then Present (Library_Unit (N)); + return Present (Library_Unit (N)); end Traverse_Stub; -- Start of processing for Traverse_Declaration_Or_Statement -- cgit v1.2.1 From bf5009ccd3026429391afce9e153cf58f2da2d4d Mon Sep 17 00:00:00 2001 From: pmderodat Date: Wed, 8 Nov 2017 16:22:37 +0000 Subject: 2017-11-08 Piotr Trojanek * spark_xrefs.ads (SPARK_File_Record): Remove string components. * spark_xrefs.adb (dspark): Remove pretty-printing of removed SPARK_File_Record components. * lib-xref-spark_specific.adb (Add_SPARK_File): Do not store string representation of files/units. git-svn-id: svn+ssh://gcc.gnu.org/svn/gcc/trunk@254541 138bc75d-0d04-0410-961f-82ee72b054a4 --- gcc/ada/lib-xref-spark_specific.adb | 30 +++--------------------------- 1 file changed, 3 insertions(+), 27 deletions(-) (limited to 'gcc/ada/lib-xref-spark_specific.adb') diff --git a/gcc/ada/lib-xref-spark_specific.adb b/gcc/ada/lib-xref-spark_specific.adb index c43cbb15ced..300706a35c8 100644 --- a/gcc/ada/lib-xref-spark_specific.adb +++ b/gcc/ada/lib-xref-spark_specific.adb @@ -208,11 +208,6 @@ package body SPARK_Specific is procedure Traverse_Scopes is new Traverse_Compilation_Unit (Detect_And_Add_SPARK_Scope); - -- Local variables - - File_Name : String_Ptr; - Unit_File_Name : String_Ptr; - -- Start of processing for Add_SPARK_File begin @@ -240,29 +235,10 @@ package body SPARK_Specific is Traverse_Scopes (CU => Cunit (Ubody)); end if; - -- Make entry for new file in file table - - Get_Name_String (Reference_Name (File)); - File_Name := new String'(Name_Buffer (1 .. Name_Len)); - - -- For subunits, also retrieve the file name of the unit. Only do so if - -- unit has an associated compilation unit. - - if Present (Cunit (Unit (File))) - and then Nkind (Unit (Cunit (Unit (File)))) = N_Subunit - then - Get_Name_String (Reference_Name (Main_Source_File)); - Unit_File_Name := new String'(Name_Buffer (1 .. Name_Len)); - else - Unit_File_Name := null; - end if; - SPARK_File_Table.Append ( - (File_Name => File_Name, - Unit_File_Name => Unit_File_Name, - File_Num => Dspec, - From_Scope => From, - To_Scope => SPARK_Scope_Table.Last)); + (File_Num => Dspec, + From_Scope => From, + To_Scope => SPARK_Scope_Table.Last)); end Add_SPARK_File; --------------------- -- cgit v1.2.1 From 68f5ac985f71ec51105ab4fc334298d716e0c365 Mon Sep 17 00:00:00 2001 From: pmderodat Date: Wed, 8 Nov 2017 16:25:03 +0000 Subject: 2017-11-08 Piotr Trojanek * spark_xrefs.ads (SPARK_Scope_Record): Rename Scope_Id component to Entity. * lib-xref-spark_specific.adb, spark_xrefs.adb: Propagate renaming of the Scope_Id record component. git-svn-id: svn+ssh://gcc.gnu.org/svn/gcc/trunk@254542 138bc75d-0d04-0410-961f-82ee72b054a4 --- gcc/ada/lib-xref-spark_specific.adb | 16 ++++++++-------- 1 file changed, 8 insertions(+), 8 deletions(-) (limited to 'gcc/ada/lib-xref-spark_specific.adb') diff --git a/gcc/ada/lib-xref-spark_specific.adb b/gcc/ada/lib-xref-spark_specific.adb index 300706a35c8..929de9a8f21 100644 --- a/gcc/ada/lib-xref-spark_specific.adb +++ b/gcc/ada/lib-xref-spark_specific.adb @@ -161,7 +161,7 @@ package body SPARK_Specific is -- range. SPARK_Scope_Table.Append - ((Scope_Id => E, + ((Entity => E, File_Num => Dspec, Scope_Num => Scope_Id, Spec_File_Num => 0, @@ -323,7 +323,7 @@ package body SPARK_Specific is function Entity_Of_Scope (S : Scope_Index) return Entity_Id is begin - return SPARK_Scope_Table.Table (S).Scope_Id; + return SPARK_Scope_Table.Table (S).Entity; end Entity_Of_Scope; ------------------- @@ -395,7 +395,7 @@ package body SPARK_Specific is function Is_Past_Scope_Entity return Boolean is begin for Index in SPARK_Scope_Table.First .. S - 1 loop - if SPARK_Scope_Table.Table (Index).Scope_Id = E then + if SPARK_Scope_Table.Table (Index).Entity = E then return True; end if; end loop; @@ -407,7 +407,7 @@ package body SPARK_Specific is begin for Index in S .. SPARK_Scope_Table.Last loop - if SPARK_Scope_Table.Table (Index).Scope_Id = E then + if SPARK_Scope_Table.Table (Index).Entity = E then return True; end if; end loop; @@ -606,7 +606,7 @@ package body SPARK_Specific is declare S : SPARK_Scope_Record renames SPARK_Scope_Table.Table (Index); begin - Set_Scope_Num (S.Scope_Id, S.Scope_Num); + Set_Scope_Num (S.Entity, S.Scope_Num); end; end loop; @@ -920,7 +920,7 @@ package body SPARK_Specific is declare Srec : SPARK_Scope_Record renames SPARK_Scope_Table.Table (S); begin - Entity_Hash_Table.Set (Srec.Scope_Id, S); + Entity_Hash_Table.Set (Srec.Entity, S); end; end loop; @@ -931,14 +931,14 @@ package body SPARK_Specific is Srec : SPARK_Scope_Record renames SPARK_Scope_Table.Table (S); Spec_Entity : constant Entity_Id := - Unique_Entity (Srec.Scope_Id); + Unique_Entity (Srec.Entity); Spec_Scope : constant Scope_Index := Entity_Hash_Table.Get (Spec_Entity); begin -- Generic spec may be missing in which case Spec_Scope is zero - if Spec_Entity /= Srec.Scope_Id + if Spec_Entity /= Srec.Entity and then Spec_Scope /= 0 then Srec.Spec_File_Num := -- cgit v1.2.1 From 372381400ad158e11c0239df83c7c5411bf491c8 Mon Sep 17 00:00:00 2001 From: pmderodat Date: Wed, 8 Nov 2017 16:31:39 +0000 Subject: 2017-11-08 Piotr Trojanek * spark_xrefs.ads (SPARK_Xref_Record): Replace file and scope indices with Entity_Id of the reference. * spark_xrefs.adb (dspark): Adapt pretty-printing routine. * lib-xref-spark_specific.adb (Add_SPARK_Xrefs): Store Entity_Id of the reference, not the file and scope indices. 2017-11-08 Arnaud Charlet * errout.ads (Current_Node): New. * errout.adb (Error_Msg): Use Current_Node. * par-ch6.adb, par-ch7.adb, par-ch9.adb, par-util.adb: Set Current_Node when relevant. * style.adb: Call Error_Msg_N when possible. git-svn-id: svn+ssh://gcc.gnu.org/svn/gcc/trunk@254543 138bc75d-0d04-0410-961f-82ee72b054a4 --- gcc/ada/lib-xref-spark_specific.adb | 3 +-- 1 file changed, 1 insertion(+), 2 deletions(-) (limited to 'gcc/ada/lib-xref-spark_specific.adb') diff --git a/gcc/ada/lib-xref-spark_specific.adb b/gcc/ada/lib-xref-spark_specific.adb index 929de9a8f21..8cc2e7299fd 100644 --- a/gcc/ada/lib-xref-spark_specific.adb +++ b/gcc/ada/lib-xref-spark_specific.adb @@ -773,8 +773,7 @@ package body SPARK_Specific is SPARK_Xref_Table.Append ( (Entity => Unique_Entity (Ref.Ent), - File_Num => Dependency_Num (Ref.Lun), - Scope_Num => Get_Scope_Num (Ref.Ref_Scope), + Ref_Scope => Ref.Ref_Scope, Rtype => Typ)); end; end loop; -- cgit v1.2.1 From 64421398fba84a3096de346ae777198b413ad397 Mon Sep 17 00:00:00 2001 From: pmderodat Date: Wed, 8 Nov 2017 16:45:55 +0000 Subject: gcc/ada/ 2017-11-08 Piotr Trojanek * lib-xref-spark_specific.adb (Add_SPARK_Xrefs): Remove special-case for constants (with variable input). (Is_Constant_Object_Without_Variable_Input): Remove. 2017-11-08 Hristian Kirtchev * exp_ch9.adb, sem_disp.adb, sem_util.adb: Minor reformatting. 2017-11-08 Piotr Trojanek * spark_xrefs.ads (Rtype): Remove special-casing of constants for SPARK cross-references. (dspark): Remove hardcoded table bound. 2017-11-08 Ed Schonberg * sem_ch4.adb (Analyze_Aggregate): For Ada2020 delta aggregates, use the type of the base of the construct to determine the type (or candidate interpretations) of the delta aggregate. This allows the construct to appear in a context that expects a private extension. * sem_res.adb (Resolve): Handle properly a delta aggregate with an overloaded base. gcc/testsuite/ 2017-11-08 Ed Schonberg * gnat.dg/delta_aggr.adb: New testcase. git-svn-id: svn+ssh://gcc.gnu.org/svn/gcc/trunk@254544 138bc75d-0d04-0410-961f-82ee72b054a4 --- gcc/ada/lib-xref-spark_specific.adb | 66 +------------------------------------ 1 file changed, 1 insertion(+), 65 deletions(-) (limited to 'gcc/ada/lib-xref-spark_specific.adb') diff --git a/gcc/ada/lib-xref-spark_specific.adb b/gcc/ada/lib-xref-spark_specific.adb index 8cc2e7299fd..37349faf2f0 100644 --- a/gcc/ada/lib-xref-spark_specific.adb +++ b/gcc/ada/lib-xref-spark_specific.adb @@ -252,11 +252,6 @@ package body SPARK_Specific is function Get_Scope_Num (E : Entity_Id) return Nat; -- Return the scope number associated with the entity E - function Is_Constant_Object_Without_Variable_Input - (E : Entity_Id) return Boolean; - -- Return True if E is known to have no variable input, as defined in - -- SPARK RM. - function Is_Future_Scope_Entity (E : Entity_Id; S : Scope_Index) return Boolean; @@ -332,50 +327,6 @@ package body SPARK_Specific is function Get_Scope_Num (E : Entity_Id) return Nat renames Scopes.Get; - ----------------------------------------------- - -- Is_Constant_Object_Without_Variable_Input -- - ----------------------------------------------- - - function Is_Constant_Object_Without_Variable_Input - (E : Entity_Id) return Boolean - is - begin - case Ekind (E) is - - -- A constant is known to have no variable input if its - -- initializing expression is static (a value which is - -- compile-time-known is not guaranteed to have no variable input - -- as defined in the SPARK RM). Otherwise, the constant may or not - -- have variable input. - - when E_Constant => - declare - Decl : Node_Id; - begin - if Present (Full_View (E)) then - Decl := Parent (Full_View (E)); - else - Decl := Parent (E); - end if; - - if Is_Imported (E) then - return False; - else - pragma Assert (Present (Expression (Decl))); - return Is_Static_Expression (Expression (Decl)); - end if; - end; - - when E_In_Parameter - | E_Loop_Parameter - => - return True; - - when others => - return False; - end case; - end Is_Constant_Object_Without_Variable_Input; - ---------------------------- -- Is_Future_Scope_Entity -- ---------------------------- @@ -729,7 +680,6 @@ package body SPARK_Specific is declare Ref_Entry : Xref_Entry renames Xrefs.Table (Rnums (Refno)); Ref : Xref_Key renames Ref_Entry.Key; - Typ : Character; begin -- If this assertion fails, the scope which we are looking for is @@ -757,24 +707,10 @@ package body SPARK_Specific is pragma Assert (Scope_Id <= SPARK_Scope_Table.Last); end loop; - -- References to constant objects without variable inputs (see - -- SPARK RM 3.3.1) are considered specially in SPARK section, - -- because these will be translated as constants in the - -- intermediate language for formal verification, and should - -- therefore never appear in frame conditions. Other constants may - -- later be treated the same, up to GNATprove to decide based on - -- its flow analysis. - - if Is_Constant_Object_Without_Variable_Input (Ref.Ent) then - Typ := 'c'; - else - Typ := Ref.Typ; - end if; - SPARK_Xref_Table.Append ( (Entity => Unique_Entity (Ref.Ent), Ref_Scope => Ref.Ref_Scope, - Rtype => Typ)); + Rtype => Ref.Typ)); end; end loop; -- cgit v1.2.1 From 484268ccfaf0a59fd12001dbcda9656c3c62258a Mon Sep 17 00:00:00 2001 From: pmderodat Date: Wed, 8 Nov 2017 16:52:32 +0000 Subject: 2017-11-08 Piotr Trojanek * spark_xrefs.ads (SPARK_Scope_Record): Remove Spec_File_Num and Spec_Scope_Num components. * spark_xrefs.adb (dspark): Skip pretty-printing to removed components. * lib-xref-spark_specific.adb (Add_SPARK_Scope): Skip initialization of removed components. (Collect_SPARK_Xrefs): Skip setting proper values of removed components. 2017-11-08 Gary Dismukes * exp_ch4.adb (Expand_N_Type_Conversion): Add test that the selector name is a discriminant in check for unconditional accessibility violation within instances. git-svn-id: svn+ssh://gcc.gnu.org/svn/gcc/trunk@254545 138bc75d-0d04-0410-961f-82ee72b054a4 --- gcc/ada/lib-xref-spark_specific.adb | 51 ------------------------------------- 1 file changed, 51 deletions(-) (limited to 'gcc/ada/lib-xref-spark_specific.adb') diff --git a/gcc/ada/lib-xref-spark_specific.adb b/gcc/ada/lib-xref-spark_specific.adb index 37349faf2f0..56bcf5de919 100644 --- a/gcc/ada/lib-xref-spark_specific.adb +++ b/gcc/ada/lib-xref-spark_specific.adb @@ -164,8 +164,6 @@ package body SPARK_Specific is ((Entity => E, File_Num => Dspec, Scope_Num => Scope_Id, - Spec_File_Num => 0, - Spec_Scope_Num => 0, From_Xref => 1, To_Xref => 0)); @@ -836,55 +834,6 @@ package body SPARK_Specific is Sdep := Sdep_Next; end loop; - -- Fill in the spec information when relevant - - declare - package Entity_Hash_Table is new - GNAT.HTable.Simple_HTable - (Header_Num => Entity_Hashed_Range, - Element => Scope_Index, - No_Element => 0, - Key => Entity_Id, - Hash => Entity_Hash, - Equal => "="); - - begin - -- Fill in the hash-table - - for S in SPARK_Scope_Table.First .. SPARK_Scope_Table.Last loop - declare - Srec : SPARK_Scope_Record renames SPARK_Scope_Table.Table (S); - begin - Entity_Hash_Table.Set (Srec.Entity, S); - end; - end loop; - - -- Use the hash-table to locate spec entities - - for S in SPARK_Scope_Table.First .. SPARK_Scope_Table.Last loop - declare - Srec : SPARK_Scope_Record renames SPARK_Scope_Table.Table (S); - - Spec_Entity : constant Entity_Id := - Unique_Entity (Srec.Entity); - Spec_Scope : constant Scope_Index := - Entity_Hash_Table.Get (Spec_Entity); - - begin - -- Generic spec may be missing in which case Spec_Scope is zero - - if Spec_Entity /= Srec.Entity - and then Spec_Scope /= 0 - then - Srec.Spec_File_Num := - SPARK_Scope_Table.Table (Spec_Scope).File_Num; - Srec.Spec_Scope_Num := - SPARK_Scope_Table.Table (Spec_Scope).Scope_Num; - end if; - end; - end loop; - end; - -- Generate SPARK cross-reference information Add_SPARK_Xrefs; -- cgit v1.2.1 From 0486c1119eeee7ec12ceabb3e69195d9f8019b84 Mon Sep 17 00:00:00 2001 From: pmderodat Date: Wed, 8 Nov 2017 17:10:05 +0000 Subject: 2017-11-08 Piotr Trojanek * spark_xrefs.ads (SPARK_Scope_Record): Remove File_Num component. * lib-xref-spark_specific.adb (Add_SPARK_Scope): Skip initialization of removed component. 2017-11-08 Gary Dismukes * sem_ch4.adb: Minor typo fix. git-svn-id: svn+ssh://gcc.gnu.org/svn/gcc/trunk@254546 138bc75d-0d04-0410-961f-82ee72b054a4 --- gcc/ada/lib-xref-spark_specific.adb | 9 ++++----- 1 file changed, 4 insertions(+), 5 deletions(-) (limited to 'gcc/ada/lib-xref-spark_specific.adb') diff --git a/gcc/ada/lib-xref-spark_specific.adb b/gcc/ada/lib-xref-spark_specific.adb index 56bcf5de919..df0c5bbe188 100644 --- a/gcc/ada/lib-xref-spark_specific.adb +++ b/gcc/ada/lib-xref-spark_specific.adb @@ -161,11 +161,10 @@ package body SPARK_Specific is -- range. SPARK_Scope_Table.Append - ((Entity => E, - File_Num => Dspec, - Scope_Num => Scope_Id, - From_Xref => 1, - To_Xref => 0)); + ((Entity => E, + Scope_Num => Scope_Id, + From_Xref => 1, + To_Xref => 0)); Scope_Id := Scope_Id + 1; end Add_SPARK_Scope; -- cgit v1.2.1 From d07035daf0a5fa5bb14bab9bd5199d713e7b525b Mon Sep 17 00:00:00 2001 From: pmderodat Date: Wed, 8 Nov 2017 17:32:18 +0000 Subject: 2017-11-08 Piotr Trojanek * lib-xref.ads, lib-xref-spark_specific.adb (Traverse_Compilation_Unit): Move declaration to package body. 2017-11-08 Hristian Kirtchev * exp_spark.adb (Expand_SPARK_N_Object_Renaming_Declaration): Obtain the type of the renaming from its defining entity, rather then the subtype mark as there may not be a subtype mark. 2017-11-08 Jerome Lambourg * adaint.c, s-oscons-tmplt.c, init.c, libgnat/system-qnx-aarch64.ads, libgnarl/a-intnam__qnx.ads, libgnarl/s-intman__qnx.adb, libgnarl/s-osinte__qnx.ads, libgnarl/s-qnx.ads, libgnarl/s-taprop__qnx.adb, s-oscons-tmplt.c, sigtramp-qnx.c, terminals.c: Initial port of GNAT for aarch64-qnx 2017-11-08 Elisa Barboni * exp_util.adb (Find_DIC_Type): Move... * sem_util.ads, sem_util.adb (Find_DIC_Type): ... here. 2017-11-08 Justin Squirek * sem_res.adb (Resolve_Allocator): Add info messages corresponding to the owner and corresponding coextension. 2017-11-08 Ed Schonberg * sem_aggr.adb (Resolve_Delta_Aggregate): Divide into the following separate procedures. (Resolve_Delta_Array_Aggregate): Previous code form Resolve_Delta_Aggregate. (Resolve_Delta_Record_Aggregate): Extend previous code to cover latest ARG decisions on the legality rules for delta aggregates for records: in the case of a variant record, components from different variants cannot be specified in the delta aggregate, and this must be checked statically. git-svn-id: svn+ssh://gcc.gnu.org/svn/gcc/trunk@254547 138bc75d-0d04-0410-961f-82ee72b054a4 --- gcc/ada/lib-xref-spark_specific.adb | 6 ++++++ 1 file changed, 6 insertions(+) (limited to 'gcc/ada/lib-xref-spark_specific.adb') diff --git a/gcc/ada/lib-xref-spark_specific.adb b/gcc/ada/lib-xref-spark_specific.adb index df0c5bbe188..48bb91da3db 100644 --- a/gcc/ada/lib-xref-spark_specific.adb +++ b/gcc/ada/lib-xref-spark_specific.adb @@ -96,6 +96,12 @@ package body SPARK_Specific is function Entity_Hash (E : Entity_Id) return Entity_Hashed_Range; -- Hash function for hash table + generic + with procedure Process (N : Node_Id) is <>; + procedure Traverse_Compilation_Unit (CU : Node_Id); + -- Call Process on all declarations within compilation unit CU. Bodies + -- of stubs are also traversed, but generic declarations are ignored. + -------------------- -- Add_SPARK_File -- -------------------- -- cgit v1.2.1 From 8a56eb985602f6282d38e5adc1f02067b1a84377 Mon Sep 17 00:00:00 2001 From: pmderodat Date: Thu, 9 Nov 2017 09:47:31 +0000 Subject: 2017-11-09 Piotr Trojanek * lib-xref-spark_specific.adb (Add_SPARK_Xrefs): Ignore loop parameters in expression funtions that are expanded into variables. 2017-11-09 Piotr Trojanek * sem_util.adb: Minor whitespace cleanup. 2017-11-09 Jerome Lambourg * libgnarl/s-taprop__qnx.adb: Refine aarch64-qnx. Use the POSIX s-taprop version rather than a custom one. * sigtramp-qnx.c (aarch64-qnx): Implement the signal trampoline. git-svn-id: svn+ssh://gcc.gnu.org/svn/gcc/trunk@254563 138bc75d-0d04-0410-961f-82ee72b054a4 --- gcc/ada/lib-xref-spark_specific.adb | 4 +++- 1 file changed, 3 insertions(+), 1 deletion(-) (limited to 'gcc/ada/lib-xref-spark_specific.adb') diff --git a/gcc/ada/lib-xref-spark_specific.adb b/gcc/ada/lib-xref-spark_specific.adb index 48bb91da3db..a30cb84b30f 100644 --- a/gcc/ada/lib-xref-spark_specific.adb +++ b/gcc/ada/lib-xref-spark_specific.adb @@ -608,9 +608,11 @@ package body SPARK_Specific is -- the analysis of the expanded body. We don't lose any globals -- by discarding them, because such loop parameters can only be -- accessed locally from within the expression function body. + -- Note: some loop parameters are expanded into variables; they + -- also must be ignored. and then not - (Ekind (Ref.Ent) = E_Loop_Parameter + (Ekind_In (Ref.Ent, E_Loop_Parameter, E_Variable) and then Scope_Within (Ref.Ent, Unique_Entity (Ref.Ref_Scope)) and then Is_Expression_Function (Ref.Ref_Scope)) -- cgit v1.2.1 From 54a4cafdfd9ca8df94c3a49c87f77e466f8c2823 Mon Sep 17 00:00:00 2001 From: pmderodat Date: Thu, 9 Nov 2017 11:13:49 +0000 Subject: gcc/ada/ 2017-11-09 Arnaud Charlet * gnat1drv.adb (Adjust_Global_Switches): Suppress warnings in codepeer mode here unless -gnateC is specified. * switch-c.adb (Scan_Front_End_Switches): Do not suppress warnings with -gnatC here. 2017-11-09 Piotr Trojanek * lib-writ.adb (Write_ALI): Remove processing of the frontend xrefs as part of the ALI writing; they are now processed directly from memory when requested by the backend. * lib-xref.ads (Collect_SPARK_Xrefs): Remove. (Iterate_SPARK_Xrefs): New routine for iterating over frontend xrefs. * lib-xref-spark_specific.adb (Traverse_Compilation_Unit): Remove. (Add_SPARK_File): Remove. (Add_SPARK_Xref): Refactored from removed code; filters xref entries that are trivially uninteresting to the SPARK backend. * spark_xrefs.ads: Remove code that is no longer needed. * spark_xrefs.adb (dspark): Adapt to use Iterate_SPARK_Xrefs. 2017-11-09 Hristian Kirtchev * sem_elab.adb: Update the documentation on adding a new elaboration schenario. Add new hash table Recorded_Top_Level_Scenarios. (Is_Check_Emitting_Scenario): Removed. (Is_Recorded_Top_Level_Scenario): New routine. (Kill_Elaboration_Scenario): Reimplemented. (Record_Elaboration_Scenario): Mark the scenario as recorded. (Set_Is_Recorded_Top_Level_Scenario): New routine. (Update_Elaboration_Scenario): Reimplemented. * sinfo.adb (Is_Recorded_Scenario): Removed. (Set_Is_Recorded_Scenario): Removed. * sinfo.ads: Remove attribute Is_Recorded_Scenario along with occurrences in nodes. (Is_Recorded_Scenario): Removed along with pragma Inline. (Set_Is_Recorded_Scenario): Removed along with pragma Inline. 2017-11-09 Piotr Trojanek * sem_prag.adb (Analyze_Part_Of): Change "designate" to "denote" in error message. 2017-11-09 Justin Squirek * sem_res.adb (Resolve_Allocator): Add warning messages corresponding to the allocation of an anonymous access-to-controlled object. gcc/testsuite/ 2017-11-09 Hristian Kirtchev * gnat.dg/elab3.adb, gnat.dg/elab3.ads, gnat.dg/elab3_pkg.adb, gnat.dg/elab3_pkg.ads: New testcase. 2017-11-09 Pierre-Marie de Rodat * gnat.dg/controlled2.adb, gnat.dg/controlled4.adb, gnat.dg/finalized.adb: Disable the new warning from GNAT. git-svn-id: svn+ssh://gcc.gnu.org/svn/gcc/trunk@254568 138bc75d-0d04-0410-961f-82ee72b054a4 --- gcc/ada/lib-xref-spark_specific.adb | 1075 +---------------------------------- 1 file changed, 31 insertions(+), 1044 deletions(-) (limited to 'gcc/ada/lib-xref-spark_specific.adb') diff --git a/gcc/ada/lib-xref-spark_specific.adb b/gcc/ada/lib-xref-spark_specific.adb index a30cb84b30f..52958328b1e 100644 --- a/gcc/ada/lib-xref-spark_specific.adb +++ b/gcc/ada/lib-xref-spark_specific.adb @@ -27,8 +27,6 @@ with Einfo; use Einfo; with Nmake; use Nmake; with SPARK_Xrefs; use SPARK_Xrefs; -with GNAT.HTable; - separate (Lib.Xref) package body SPARK_Specific is @@ -59,9 +57,6 @@ package body SPARK_Specific is 's' => True, others => False); - type Entity_Hashed_Range is range 0 .. 255; - -- Size of hash table headers - --------------------- -- Local Variables -- --------------------- @@ -78,187 +73,13 @@ package body SPARK_Specific is -- "Heap". These references are added to the regular references when -- computing SPARK cross-references. - ----------------------- - -- Local Subprograms -- - ----------------------- - - procedure Add_SPARK_File (Uspec, Ubody : Unit_Number_Type; Dspec : Nat); - -- Add file and corresponding scopes for unit to the tables - -- SPARK_File_Table and SPARK_Scope_Table. When two units are present - -- for the same compilation unit, as it happens for library-level - -- instantiations of generics, then Ubody is the number of the body - -- unit; otherwise it is No_Unit. - - procedure Add_SPARK_Xrefs; - -- Filter table Xrefs to add all references used in SPARK to the table - -- SPARK_Xref_Table. - - function Entity_Hash (E : Entity_Id) return Entity_Hashed_Range; - -- Hash function for hash table - - generic - with procedure Process (N : Node_Id) is <>; - procedure Traverse_Compilation_Unit (CU : Node_Id); - -- Call Process on all declarations within compilation unit CU. Bodies - -- of stubs are also traversed, but generic declarations are ignored. - - -------------------- - -- Add_SPARK_File -- - -------------------- - - procedure Add_SPARK_File (Uspec, Ubody : Unit_Number_Type; Dspec : Nat) is - File : constant Source_File_Index := Source_Index (Uspec); - From : constant Scope_Index := SPARK_Scope_Table.Last + 1; - - Scope_Id : Pos := 1; - - procedure Add_SPARK_Scope (N : Node_Id); - -- Add scope N to the table SPARK_Scope_Table - - procedure Detect_And_Add_SPARK_Scope (N : Node_Id); - -- Call Add_SPARK_Scope on scopes - - --------------------- - -- Add_SPARK_Scope -- - --------------------- - - procedure Add_SPARK_Scope (N : Node_Id) is - E : constant Entity_Id := Defining_Entity (N); - - begin - -- Ignore scopes without a proper location - - if Sloc (N) = No_Location then - return; - end if; - - case Ekind (E) is - when E_Entry - | E_Entry_Family - | E_Function - | E_Generic_Function - | E_Generic_Package - | E_Generic_Procedure - | E_Package - | E_Package_Body - | E_Procedure - | E_Protected_Body - | E_Protected_Type - | E_Task_Body - | E_Task_Type - | E_Subprogram_Body - => - null; - - when E_Void => - - -- Compilation of prj-attr.adb with -gnatn creates a node with - -- entity E_Void for the package defined at a-charac.ads16:13. - -- ??? TBD - - return; - - when others => - raise Program_Error; - end case; - - -- File_Num and Scope_Num are filled later. From_Xref and To_Xref - -- are filled even later, but are initialized to represent an empty - -- range. - - SPARK_Scope_Table.Append - ((Entity => E, - Scope_Num => Scope_Id, - From_Xref => 1, - To_Xref => 0)); - - Scope_Id := Scope_Id + 1; - end Add_SPARK_Scope; - - -------------------------------- - -- Detect_And_Add_SPARK_Scope -- - -------------------------------- - - procedure Detect_And_Add_SPARK_Scope (N : Node_Id) is - begin - -- Entries - - if Nkind_In (N, N_Entry_Body, N_Entry_Declaration) - - -- Packages - - or else Nkind_In (N, N_Package_Body, - N_Package_Declaration) - -- Protected units - - or else Nkind_In (N, N_Protected_Body, - N_Protected_Type_Declaration) - - -- Subprograms - - or else Nkind_In (N, N_Subprogram_Body, - N_Subprogram_Declaration) - - -- Task units - - or else Nkind_In (N, N_Task_Body, - N_Task_Type_Declaration) - then - Add_SPARK_Scope (N); - end if; - end Detect_And_Add_SPARK_Scope; - - procedure Traverse_Scopes is new - Traverse_Compilation_Unit (Detect_And_Add_SPARK_Scope); - - -- Start of processing for Add_SPARK_File - - begin - -- Source file could be inexistant as a result of an error, if option - -- gnatQ is used. - - if File <= No_Source_File then - return; - end if; - - -- Subunits are traversed as part of the top-level unit to which they - -- belong. - - if Nkind (Unit (Cunit (Uspec))) = N_Subunit then - return; - end if; - - Traverse_Scopes (CU => Cunit (Uspec)); - - -- When two units are present for the same compilation unit, as it - -- happens for library-level instantiations of generics, then add all - -- scopes to the same SPARK file. - - if Ubody /= No_Unit then - Traverse_Scopes (CU => Cunit (Ubody)); - end if; - - SPARK_File_Table.Append ( - (File_Num => Dspec, - From_Scope => From, - To_Scope => SPARK_Scope_Table.Last)); - end Add_SPARK_File; - - --------------------- - -- Add_SPARK_Xrefs -- - --------------------- - - procedure Add_SPARK_Xrefs is - function Entity_Of_Scope (S : Scope_Index) return Entity_Id; - -- Return the entity which maps to the input scope index + ------------------------- + -- Iterate_SPARK_Xrefs -- + ------------------------- - function Get_Scope_Num (E : Entity_Id) return Nat; - -- Return the scope number associated with the entity E + procedure Iterate_SPARK_Xrefs is - function Is_Future_Scope_Entity - (E : Entity_Id; - S : Scope_Index) return Boolean; - -- Check whether entity E is in SPARK_Scope_Table at index S or higher + procedure Add_SPARK_Xref (Index : Int; Xref : Xref_Entry); function Is_SPARK_Reference (E : Entity_Id; @@ -270,110 +91,29 @@ package body SPARK_Specific is -- Return whether the entity or reference scope meets requirements for -- being a SPARK scope. - function Lt (Op1 : Natural; Op2 : Natural) return Boolean; - -- Comparison function for Sort call - - procedure Move (From : Natural; To : Natural); - -- Move procedure for Sort call - - procedure Set_Scope_Num (E : Entity_Id; Num : Nat); - -- Associate entity E with the scope number Num - - procedure Update_Scope_Range - (S : Scope_Index; - From : Xref_Index; - To : Xref_Index); - -- Update the scope which maps to S with the new range From .. To - - package Sorting is new GNAT.Heap_Sort_G (Move, Lt); - - No_Scope : constant Nat := 0; - -- Initial scope counter - - package Scopes is new GNAT.HTable.Simple_HTable - (Header_Num => Entity_Hashed_Range, - Element => Nat, - No_Element => No_Scope, - Key => Entity_Id, - Hash => Entity_Hash, - Equal => "="); - -- Package used to build a correspondence between entities and scope - -- numbers used in SPARK cross references. - - Nrefs : Nat := Xrefs.Last; - -- Number of references in table. This value may get reset (reduced) - -- when we eliminate duplicate reference entries as well as references - -- not suitable for local cross-references. - - Nrefs_Add : constant Nat := Drefs.Last; - -- Number of additional references which correspond to dereferences in - -- the source code. - - Rnums : array (0 .. Nrefs + Nrefs_Add) of Nat; - -- This array contains numbers of references in the Xrefs table. This - -- list is sorted in output order. The extra 0'th entry is convenient - -- for the call to sort. When we sort the table, we move the indices in - -- Rnums around, but we do not move the original table entries. - - --------------------- - -- Entity_Of_Scope -- - --------------------- - - function Entity_Of_Scope (S : Scope_Index) return Entity_Id is - begin - return SPARK_Scope_Table.Table (S).Entity; - end Entity_Of_Scope; - - ------------------- - -- Get_Scope_Num -- - ------------------- - - function Get_Scope_Num (E : Entity_Id) return Nat renames Scopes.Get; - - ---------------------------- - -- Is_Future_Scope_Entity -- - ---------------------------- - - function Is_Future_Scope_Entity - (E : Entity_Id; - S : Scope_Index) return Boolean - is - function Is_Past_Scope_Entity return Boolean; - -- Check whether entity E is in SPARK_Scope_Table at index strictly - -- lower than S. - - -------------------------- - -- Is_Past_Scope_Entity -- - -------------------------- - - function Is_Past_Scope_Entity return Boolean is - begin - for Index in SPARK_Scope_Table.First .. S - 1 loop - if SPARK_Scope_Table.Table (Index).Entity = E then - return True; - end if; - end loop; - - return False; - end Is_Past_Scope_Entity; - - -- Start of processing for Is_Future_Scope_Entity + -------------------- + -- Add_SPARK_Xref -- + -------------------- + procedure Add_SPARK_Xref (Index : Int; Xref : Xref_Entry) is + Ref : Xref_Key renames Xref.Key; begin - for Index in S .. SPARK_Scope_Table.Last loop - if SPARK_Scope_Table.Table (Index).Entity = E then - return True; - end if; - end loop; + -- Eliminate entries not appropriate for SPARK - -- If this assertion fails, this means that the scope which we are - -- looking for has been treated already, which reveals a problem in - -- the order of cross-references. - - pragma Assert (not Is_Past_Scope_Entity); + if SPARK_Entities (Ekind (Ref.Ent)) + and then SPARK_References (Ref.Typ) + and then Is_SPARK_Scope (Ref.Ent_Scope) + and then Is_SPARK_Scope (Ref.Ref_Scope) + and then Is_SPARK_Reference (Ref.Ent, Ref.Typ) + then + Process + (Index, + (Entity => Ref.Ent, + Ref_Scope => Ref.Ref_Scope, + Rtype => Ref.Typ)); + end if; - return False; - end Is_Future_Scope_Entity; + end Add_SPARK_Xref; ------------------------ -- Is_SPARK_Reference -- @@ -411,440 +151,22 @@ package body SPARK_Specific is begin return Present (E) and then not Is_Generic_Unit (E) - and then (not Can_Be_Renamed or else No (Renamed_Entity (E))) - and then Get_Scope_Num (E) /= No_Scope; + and then (not Can_Be_Renamed or else No (Renamed_Entity (E))); end Is_SPARK_Scope; - -------- - -- Lt -- - -------- - - function Lt (Op1 : Natural; Op2 : Natural) return Boolean is - T1 : constant Xref_Entry := Xrefs.Table (Rnums (Nat (Op1))); - T2 : constant Xref_Entry := Xrefs.Table (Rnums (Nat (Op2))); - - begin - -- First test: if entity is in different unit, sort by unit. Note: - -- that we use Ent_Scope_File rather than Eun, as Eun may refer to - -- the file where the generic scope is defined, which may differ from - -- the file where the enclosing scope is defined. It is the latter - -- which matters for a correct order here. - - if T1.Ent_Scope_File /= T2.Ent_Scope_File then - return Dependency_Num (T1.Ent_Scope_File) < - Dependency_Num (T2.Ent_Scope_File); - - -- Second test: within same unit, sort by location of the scope of - -- the entity definition. - - elsif Get_Scope_Num (T1.Key.Ent_Scope) /= - Get_Scope_Num (T2.Key.Ent_Scope) - then - return Get_Scope_Num (T1.Key.Ent_Scope) < - Get_Scope_Num (T2.Key.Ent_Scope); - - -- Third test: within same unit and scope, sort by location of - -- entity definition. - - elsif T1.Def /= T2.Def then - return T1.Def < T2.Def; - - else - -- Both entities must be equal at this point - - pragma Assert (T1.Key.Ent = T2.Key.Ent); - pragma Assert (T1.Key.Ent_Scope = T2.Key.Ent_Scope); - pragma Assert (T1.Ent_Scope_File = T2.Ent_Scope_File); - - -- Fourth test: if reference is in same unit as entity definition, - -- sort first. - - if T1.Key.Lun /= T2.Key.Lun - and then T1.Ent_Scope_File = T1.Key.Lun - then - return True; - - elsif T1.Key.Lun /= T2.Key.Lun - and then T2.Ent_Scope_File = T2.Key.Lun - then - return False; - - -- Fifth test: if reference is in same unit and same scope as - -- entity definition, sort first. - - elsif T1.Ent_Scope_File = T1.Key.Lun - and then T1.Key.Ref_Scope /= T2.Key.Ref_Scope - and then T1.Key.Ent_Scope = T1.Key.Ref_Scope - then - return True; - - elsif T2.Ent_Scope_File = T2.Key.Lun - and then T1.Key.Ref_Scope /= T2.Key.Ref_Scope - and then T2.Key.Ent_Scope = T2.Key.Ref_Scope - then - return False; - - -- Sixth test: for same entity, sort by reference location unit - - elsif T1.Key.Lun /= T2.Key.Lun then - return Dependency_Num (T1.Key.Lun) < - Dependency_Num (T2.Key.Lun); - - -- Seventh test: for same entity, sort by reference location scope - - elsif Get_Scope_Num (T1.Key.Ref_Scope) /= - Get_Scope_Num (T2.Key.Ref_Scope) - then - return Get_Scope_Num (T1.Key.Ref_Scope) < - Get_Scope_Num (T2.Key.Ref_Scope); - - -- Eighth test: order of location within referencing unit - - elsif T1.Key.Loc /= T2.Key.Loc then - return T1.Key.Loc < T2.Key.Loc; - - -- Finally, for two locations at the same address prefer the one - -- that does NOT have the type 'r', so that a modification or - -- extension takes preference, when there are more than one - -- reference at the same location. As a result, in the case of - -- entities that are in-out actuals, the read reference follows - -- the modify reference. - - else - return T2.Key.Typ = 'r'; - end if; - end if; - end Lt; - - ---------- - -- Move -- - ---------- - - procedure Move (From : Natural; To : Natural) is - begin - Rnums (Nat (To)) := Rnums (Nat (From)); - end Move; - - ------------------- - -- Set_Scope_Num -- - ------------------- - - procedure Set_Scope_Num (E : Entity_Id; Num : Nat) renames Scopes.Set; - - ------------------------ - -- Update_Scope_Range -- - ------------------------ - - procedure Update_Scope_Range - (S : Scope_Index; - From : Xref_Index; - To : Xref_Index) - is - begin - SPARK_Scope_Table.Table (S).From_Xref := From; - SPARK_Scope_Table.Table (S).To_Xref := To; - end Update_Scope_Range; - - -- Local variables - - From_Index : Xref_Index; - Prev_Loc : Source_Ptr; - Prev_Typ : Character; - Ref_Count : Nat; - Scope_Id : Scope_Index; - -- Start of processing for Add_SPARK_Xrefs begin - for Index in SPARK_Scope_Table.First .. SPARK_Scope_Table.Last loop - declare - S : SPARK_Scope_Record renames SPARK_Scope_Table.Table (Index); - begin - Set_Scope_Num (S.Entity, S.Scope_Num); - end; - end loop; - - declare - Drefs_Table : Drefs.Table_Type - renames Drefs.Table (Drefs.First .. Drefs.Last); - begin - Xrefs.Append_All (Xrefs.Table_Type (Drefs_Table)); - Nrefs := Nrefs + Drefs_Table'Length; - end; - - -- Capture the definition Sloc values. As in the case of normal cross - -- references, we have to wait until now to get the correct value. - - for Index in 1 .. Nrefs loop - Xrefs.Table (Index).Def := Sloc (Xrefs.Table (Index).Key.Ent); - end loop; - - -- Eliminate entries not appropriate for SPARK. Done prior to sorting - -- cross-references, as it discards useless references which do not have - -- a proper format for the comparison function (like no location). - - Ref_Count := Nrefs; - Nrefs := 0; - - for Index in 1 .. Ref_Count loop - declare - Ref : Xref_Key renames Xrefs.Table (Index).Key; - - begin - if SPARK_Entities (Ekind (Ref.Ent)) - and then SPARK_References (Ref.Typ) - and then Is_SPARK_Scope (Ref.Ent_Scope) - and then Is_SPARK_Scope (Ref.Ref_Scope) - and then Is_SPARK_Reference (Ref.Ent, Ref.Typ) - - -- Discard references from unknown scopes, e.g. generic scopes - - and then Get_Scope_Num (Ref.Ent_Scope) /= No_Scope - and then Get_Scope_Num (Ref.Ref_Scope) /= No_Scope - - -- Discard references to loop parameters introduced within - -- expression functions, as they give two references: one from - -- the analysis of the expression function itself and one from - -- the analysis of the expanded body. We don't lose any globals - -- by discarding them, because such loop parameters can only be - -- accessed locally from within the expression function body. - -- Note: some loop parameters are expanded into variables; they - -- also must be ignored. - - and then not - (Ekind_In (Ref.Ent, E_Loop_Parameter, E_Variable) - and then Scope_Within - (Ref.Ent, Unique_Entity (Ref.Ref_Scope)) - and then Is_Expression_Function (Ref.Ref_Scope)) - then - Nrefs := Nrefs + 1; - Rnums (Nrefs) := Index; - end if; - end; - end loop; - - -- Sort the references - - Sorting.Sort (Integer (Nrefs)); - - -- Eliminate duplicate entries - - -- We need this test for Ref_Count because if we force ALI file - -- generation in case of errors detected, it may be the case that - -- Nrefs is 0, so we should not reset it here. - - if Nrefs >= 2 then - Ref_Count := Nrefs; - Nrefs := 1; - - for Index in 2 .. Ref_Count loop - if Xrefs.Table (Rnums (Index)) /= Xrefs.Table (Rnums (Nrefs)) then - Nrefs := Nrefs + 1; - Rnums (Nrefs) := Rnums (Index); - end if; - end loop; - end if; - - -- Eliminate the reference if it is at the same location as the previous - -- one, unless it is a read-reference indicating that the entity is an - -- in-out actual in a call. - - Ref_Count := Nrefs; - Nrefs := 0; - Prev_Loc := No_Location; - Prev_Typ := 'm'; - - for Index in 1 .. Ref_Count loop - declare - Ref : Xref_Key renames Xrefs.Table (Rnums (Index)).Key; - - begin - if Ref.Loc /= Prev_Loc - or else (Prev_Typ = 'm' and then Ref.Typ = 'r') - then - Prev_Loc := Ref.Loc; - Prev_Typ := Ref.Typ; - Nrefs := Nrefs + 1; - Rnums (Nrefs) := Rnums (Index); - end if; - end; - end loop; - - -- The two steps have eliminated all references, nothing to do - - if SPARK_Scope_Table.Last = 0 then - return; - end if; - - Scope_Id := 1; - From_Index := 1; - - -- Loop to output references + -- Expose cross-references from private frontend tables to the backend - for Refno in 1 .. Nrefs loop - declare - Ref_Entry : Xref_Entry renames Xrefs.Table (Rnums (Refno)); - Ref : Xref_Key renames Ref_Entry.Key; - - begin - -- If this assertion fails, the scope which we are looking for is - -- not in SPARK scope table, which reveals either a problem in the - -- construction of the scope table, or an erroneous scope for the - -- current cross-reference. - - pragma Assert (Is_Future_Scope_Entity (Ref.Ent_Scope, Scope_Id)); - - -- Update the range of cross references to which the current scope - -- refers to. This may be the empty range only for the first scope - -- considered. - - if Ref.Ent_Scope /= Entity_Of_Scope (Scope_Id) then - Update_Scope_Range - (S => Scope_Id, - From => From_Index, - To => SPARK_Xref_Table.Last); - - From_Index := SPARK_Xref_Table.Last + 1; - end if; - - while Ref.Ent_Scope /= Entity_Of_Scope (Scope_Id) loop - Scope_Id := Scope_Id + 1; - pragma Assert (Scope_Id <= SPARK_Scope_Table.Last); - end loop; - - SPARK_Xref_Table.Append ( - (Entity => Unique_Entity (Ref.Ent), - Ref_Scope => Ref.Ref_Scope, - Rtype => Ref.Typ)); - end; + for Index in Drefs.First .. Drefs.Last loop + Add_SPARK_Xref (Index, Drefs.Table (Index)); end loop; - -- Update the range of cross references to which the scope refers to - - Update_Scope_Range - (S => Scope_Id, - From => From_Index, - To => SPARK_Xref_Table.Last); - end Add_SPARK_Xrefs; - - ------------------------- - -- Collect_SPARK_Xrefs -- - ------------------------- - - procedure Collect_SPARK_Xrefs - (Sdep_Table : Unit_Ref_Table; - Num_Sdep : Nat) - is - Sdep : Pos; - Sdep_Next : Pos; - -- Index of the current and next source dependency - - Sdep_File : Pos; - -- Index of the file to which the scopes need to be assigned; for - -- library-level instances of generic units this points to the unit - -- of the body, because this is where references are assigned to. - - Ubody : Unit_Number_Type; - Uspec : Unit_Number_Type; - -- Unit numbers for the dependency spec and possibly its body (only in - -- the case of library-level instance of a generic package). - - begin - -- Cross-references should have been computed first - - pragma Assert (Xrefs.Last /= 0); - - Initialize_SPARK_Tables; - - -- Generate file and scope SPARK cross-reference information - - Sdep := 1; - while Sdep <= Num_Sdep loop - - -- Skip dependencies with no entity node, e.g. configuration files - -- with pragmas (.adc) or target description (.atp), since they - -- present no interest for SPARK cross references. - - if No (Cunit_Entity (Sdep_Table (Sdep))) then - Sdep_Next := Sdep + 1; - - -- For library-level instantiation of a generic, two consecutive - -- units refer to the same compilation unit node and entity (one to - -- body, one to spec). In that case, treat them as a single unit for - -- the sake of SPARK cross references by passing to Add_SPARK_File. - - else - if Sdep < Num_Sdep - and then Cunit_Entity (Sdep_Table (Sdep)) = - Cunit_Entity (Sdep_Table (Sdep + 1)) - then - declare - Cunit1 : Node_Id renames Cunit (Sdep_Table (Sdep)); - Cunit2 : Node_Id renames Cunit (Sdep_Table (Sdep + 1)); - - begin - -- Both Cunits point to compilation unit nodes - - pragma Assert - (Nkind (Cunit1) = N_Compilation_Unit - and then Nkind (Cunit2) = N_Compilation_Unit); - - -- Do not depend on the sorting order, which is based on - -- Unit_Name, and for library-level instances of nested - -- generic packages they are equal. - - -- If declaration comes before the body - - if Nkind (Unit (Cunit1)) = N_Package_Declaration - and then Nkind (Unit (Cunit2)) = N_Package_Body - then - Uspec := Sdep_Table (Sdep); - Ubody := Sdep_Table (Sdep + 1); - - Sdep_File := Sdep + 1; - - -- If body comes before declaration - - elsif Nkind (Unit (Cunit1)) = N_Package_Body - and then Nkind (Unit (Cunit2)) = N_Package_Declaration - then - Uspec := Sdep_Table (Sdep + 1); - Ubody := Sdep_Table (Sdep); - - Sdep_File := Sdep; - - -- Otherwise it is an error - - else - raise Program_Error; - end if; - - Sdep_Next := Sdep + 2; - end; - - -- ??? otherwise? - - else - Uspec := Sdep_Table (Sdep); - Ubody := No_Unit; - - Sdep_File := Sdep; - Sdep_Next := Sdep + 1; - end if; - - Add_SPARK_File - (Uspec => Uspec, - Ubody => Ubody, - Dspec => Sdep_File); - end if; - - Sdep := Sdep_Next; + for Index in Xrefs.First .. Xrefs.Last loop + Add_SPARK_Xref (-Index, Xrefs.Table (Index)); end loop; - - -- Generate SPARK cross-reference information - - Add_SPARK_Xrefs; - end Collect_SPARK_Xrefs; + end Iterate_SPARK_Xrefs; ------------------------------------- -- Enclosing_Subprogram_Or_Package -- @@ -941,16 +263,6 @@ package body SPARK_Specific is return Context; end Enclosing_Subprogram_Or_Library_Package; - ----------------- - -- Entity_Hash -- - ----------------- - - function Entity_Hash (E : Entity_Id) return Entity_Hashed_Range is - begin - return - Entity_Hashed_Range (E mod (Entity_Id (Entity_Hashed_Range'Last) + 1)); - end Entity_Hash; - -------------------------- -- Generate_Dereference -- -------------------------- @@ -1019,329 +331,4 @@ package body SPARK_Specific is end if; end Generate_Dereference; - ------------------------------- - -- Traverse_Compilation_Unit -- - ------------------------------- - - procedure Traverse_Compilation_Unit (CU : Node_Id) is - procedure Traverse_Block (N : Node_Id); - procedure Traverse_Declaration_Or_Statement (N : Node_Id); - procedure Traverse_Declarations_And_HSS (N : Node_Id); - procedure Traverse_Declarations_Or_Statements (L : List_Id); - procedure Traverse_Handled_Statement_Sequence (N : Node_Id); - procedure Traverse_Package_Body (N : Node_Id); - procedure Traverse_Visible_And_Private_Parts (N : Node_Id); - procedure Traverse_Protected_Body (N : Node_Id); - procedure Traverse_Subprogram_Body (N : Node_Id); - procedure Traverse_Task_Body (N : Node_Id); - - -- Traverse corresponding construct, calling Process on all declarations - - -------------------- - -- Traverse_Block -- - -------------------- - - procedure Traverse_Block (N : Node_Id) renames - Traverse_Declarations_And_HSS; - - --------------------------------------- - -- Traverse_Declaration_Or_Statement -- - --------------------------------------- - - procedure Traverse_Declaration_Or_Statement (N : Node_Id) is - function Traverse_Stub (N : Node_Id) return Boolean; - -- Returns True iff stub N should be traversed - - function Traverse_Stub (N : Node_Id) return Boolean is - begin - pragma Assert (Nkind_In (N, N_Package_Body_Stub, - N_Protected_Body_Stub, - N_Subprogram_Body_Stub, - N_Task_Body_Stub)); - - return Present (Library_Unit (N)); - end Traverse_Stub; - - -- Start of processing for Traverse_Declaration_Or_Statement - - begin - case Nkind (N) is - when N_Package_Declaration => - Traverse_Visible_And_Private_Parts (Specification (N)); - - when N_Package_Body => - Traverse_Package_Body (N); - - when N_Package_Body_Stub => - if Traverse_Stub (N) then - Traverse_Package_Body (Get_Body_From_Stub (N)); - end if; - - when N_Subprogram_Body => - Traverse_Subprogram_Body (N); - - when N_Entry_Body => - Traverse_Subprogram_Body (N); - - when N_Subprogram_Body_Stub => - if Traverse_Stub (N) then - Traverse_Subprogram_Body (Get_Body_From_Stub (N)); - end if; - - when N_Protected_Body => - Traverse_Protected_Body (N); - - when N_Protected_Body_Stub => - if Traverse_Stub (N) then - Traverse_Protected_Body (Get_Body_From_Stub (N)); - end if; - - when N_Protected_Type_Declaration => - Traverse_Visible_And_Private_Parts (Protected_Definition (N)); - - when N_Task_Type_Declaration => - - -- Task type definition is optional (unlike protected type - -- definition, which is mandatory). - - declare - Task_Def : constant Node_Id := Task_Definition (N); - begin - if Present (Task_Def) then - Traverse_Visible_And_Private_Parts (Task_Def); - end if; - end; - - when N_Task_Body => - Traverse_Task_Body (N); - - when N_Task_Body_Stub => - if Traverse_Stub (N) then - Traverse_Task_Body (Get_Body_From_Stub (N)); - end if; - - when N_Block_Statement => - Traverse_Block (N); - - when N_If_Statement => - - -- Traverse the statements in the THEN part - - Traverse_Declarations_Or_Statements (Then_Statements (N)); - - -- Loop through ELSIF parts if present - - if Present (Elsif_Parts (N)) then - declare - Elif : Node_Id := First (Elsif_Parts (N)); - - begin - while Present (Elif) loop - Traverse_Declarations_Or_Statements - (Then_Statements (Elif)); - Next (Elif); - end loop; - end; - end if; - - -- Finally traverse the ELSE statements if present - - Traverse_Declarations_Or_Statements (Else_Statements (N)); - - when N_Case_Statement => - - -- Process case branches - - declare - Alt : Node_Id := First (Alternatives (N)); - begin - loop - Traverse_Declarations_Or_Statements (Statements (Alt)); - Next (Alt); - exit when No (Alt); - end loop; - end; - - when N_Extended_Return_Statement => - Traverse_Handled_Statement_Sequence - (Handled_Statement_Sequence (N)); - - when N_Loop_Statement => - Traverse_Declarations_Or_Statements (Statements (N)); - - -- Generic declarations are ignored - - when others => - null; - end case; - end Traverse_Declaration_Or_Statement; - - ----------------------------------- - -- Traverse_Declarations_And_HSS -- - ----------------------------------- - - procedure Traverse_Declarations_And_HSS (N : Node_Id) is - begin - Traverse_Declarations_Or_Statements (Declarations (N)); - Traverse_Handled_Statement_Sequence (Handled_Statement_Sequence (N)); - end Traverse_Declarations_And_HSS; - - ----------------------------------------- - -- Traverse_Declarations_Or_Statements -- - ----------------------------------------- - - procedure Traverse_Declarations_Or_Statements (L : List_Id) is - N : Node_Id; - - begin - -- Loop through statements or declarations - - N := First (L); - while Present (N) loop - - -- Call Process on all declarations - - if Nkind (N) in N_Declaration - or else Nkind (N) in N_Later_Decl_Item - or else Nkind (N) = N_Entry_Body - then - if Nkind (N) in N_Body_Stub then - Process (Get_Body_From_Stub (N)); - else - Process (N); - end if; - end if; - - Traverse_Declaration_Or_Statement (N); - - Next (N); - end loop; - end Traverse_Declarations_Or_Statements; - - ----------------------------------------- - -- Traverse_Handled_Statement_Sequence -- - ----------------------------------------- - - procedure Traverse_Handled_Statement_Sequence (N : Node_Id) is - Handler : Node_Id; - - begin - if Present (N) then - Traverse_Declarations_Or_Statements (Statements (N)); - - if Present (Exception_Handlers (N)) then - Handler := First (Exception_Handlers (N)); - while Present (Handler) loop - Traverse_Declarations_Or_Statements (Statements (Handler)); - Next (Handler); - end loop; - end if; - end if; - end Traverse_Handled_Statement_Sequence; - - --------------------------- - -- Traverse_Package_Body -- - --------------------------- - - procedure Traverse_Package_Body (N : Node_Id) is - Spec_E : constant Entity_Id := Unique_Defining_Entity (N); - - begin - case Ekind (Spec_E) is - when E_Package => - Traverse_Declarations_And_HSS (N); - - when E_Generic_Package => - null; - - when others => - raise Program_Error; - end case; - end Traverse_Package_Body; - - ----------------------------- - -- Traverse_Protected_Body -- - ----------------------------- - - procedure Traverse_Protected_Body (N : Node_Id) is - begin - Traverse_Declarations_Or_Statements (Declarations (N)); - end Traverse_Protected_Body; - - ------------------------------ - -- Traverse_Subprogram_Body -- - ------------------------------ - - procedure Traverse_Subprogram_Body (N : Node_Id) is - Spec_E : constant Entity_Id := Unique_Defining_Entity (N); - - begin - case Ekind (Spec_E) is - when Entry_Kind - | E_Function - | E_Procedure - => - Traverse_Declarations_And_HSS (N); - - when Generic_Subprogram_Kind => - null; - - when others => - raise Program_Error; - end case; - end Traverse_Subprogram_Body; - - ------------------------ - -- Traverse_Task_Body -- - ------------------------ - - procedure Traverse_Task_Body (N : Node_Id) renames - Traverse_Declarations_And_HSS; - - ---------------------------------------- - -- Traverse_Visible_And_Private_Parts -- - ---------------------------------------- - - procedure Traverse_Visible_And_Private_Parts (N : Node_Id) is - begin - Traverse_Declarations_Or_Statements (Visible_Declarations (N)); - Traverse_Declarations_Or_Statements (Private_Declarations (N)); - end Traverse_Visible_And_Private_Parts; - - -- Local variables - - Lu : Node_Id; - - -- Start of processing for Traverse_Compilation_Unit - - begin - -- Get Unit (checking case of subunit) - - Lu := Unit (CU); - - if Nkind (Lu) = N_Subunit then - Lu := Proper_Body (Lu); - end if; - - -- Do not add scopes for generic units - - if Nkind (Lu) = N_Package_Body - and then Ekind (Corresponding_Spec (Lu)) in Generic_Unit_Kind - then - return; - end if; - - -- Call Process on all declarations - - if Nkind (Lu) in N_Declaration - or else Nkind (Lu) in N_Later_Decl_Item - then - Process (Lu); - end if; - - -- Traverse the unit - - Traverse_Declaration_Or_Statement (Lu); - end Traverse_Compilation_Unit; - end SPARK_Specific; -- cgit v1.2.1