From c23f55b4932192981183ab6a3f914ef22476ec93 Mon Sep 17 00:00:00 2001 From: Pierre-Marie de Rodat Date: Thu, 9 Nov 2017 11:13:49 +0000 Subject: [PATCH] gnat1drv.adb (Adjust_Global_Switches): Suppress warnings in codepeer mode here unless -gnateC is specified. 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. From-SVN: r254568 --- gcc/ada/ChangeLog | 48 ++ gcc/ada/gnat1drv.adb | 8 + gcc/ada/lib-writ.adb | 7 - gcc/ada/lib-xref-spark_specific.adb | 1075 +-------------------------------- gcc/ada/lib-xref.ads | 18 +- gcc/ada/sem_elab.adb | 220 ++++--- gcc/ada/sem_prag.adb | 2 +- gcc/ada/sem_res.adb | 25 +- gcc/ada/sinfo.adb | 22 - gcc/ada/sinfo.ads | 18 - gcc/ada/spark_xrefs.adb | 105 +--- gcc/ada/spark_xrefs.ads | 118 +--- gcc/ada/switch-c.adb | 14 +- gcc/testsuite/ChangeLog | 10 + gcc/testsuite/gnat.dg/controlled2.adb | 3 + gcc/testsuite/gnat.dg/controlled4.adb | 3 + gcc/testsuite/gnat.dg/elab3.adb | 9 + gcc/testsuite/gnat.dg/elab3.ads | 3 + gcc/testsuite/gnat.dg/elab3_pkg.adb | 11 + gcc/testsuite/gnat.dg/elab3_pkg.ads | 7 + gcc/testsuite/gnat.dg/finalized.adb | 3 + 21 files changed, 345 insertions(+), 1384 deletions(-) create mode 100644 gcc/testsuite/gnat.dg/elab3.adb create mode 100644 gcc/testsuite/gnat.dg/elab3.ads create mode 100644 gcc/testsuite/gnat.dg/elab3_pkg.adb create mode 100644 gcc/testsuite/gnat.dg/elab3_pkg.ads diff --git a/gcc/ada/ChangeLog b/gcc/ada/ChangeLog index ed44aba..2f92c29 100644 --- a/gcc/ada/ChangeLog +++ b/gcc/ada/ChangeLog @@ -1,3 +1,51 @@ +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. + 2017-11-09 Jerome Lambourg * sigtramp-qnx.c: Fix obvious typo. diff --git a/gcc/ada/gnat1drv.adb b/gcc/ada/gnat1drv.adb index 90c8cab..fb94d86 100644 --- a/gcc/ada/gnat1drv.adb +++ b/gcc/ada/gnat1drv.adb @@ -383,6 +383,14 @@ procedure Gnat1drv is Relaxed_RM_Semantics := True; + if not Generate_CodePeer_Messages then + -- Suppress compiler warnings by default when generating SCIL for + -- CodePeer, except when combined with -gnateC where we do want + -- to emit GNAT warnings. + + Warning_Mode := Suppress; + end if; + -- Disable all simple value propagation. This is an optimization -- which is valuable for code optimization, and also for generation -- of compiler warnings, but these are being turned off by default, diff --git a/gcc/ada/lib-writ.adb b/gcc/ada/lib-writ.adb index 19e05d4..addc9a0 100644 --- a/gcc/ada/lib-writ.adb +++ b/gcc/ada/lib-writ.adb @@ -1567,13 +1567,6 @@ package body Lib.Writ is SCO_Output; end if; - -- Output SPARK cross-reference information if needed - - if Opt.Xref_Active and then GNATprove_Mode then - SPARK_Specific.Collect_SPARK_Xrefs (Sdep_Table => Sdep_Table, - Num_Sdep => Num_Sdep); - end if; - -- Output final blank line and we are done. This final blank line is -- probably junk, but we don't feel like making an incompatible change. diff --git a/gcc/ada/lib-xref-spark_specific.adb b/gcc/ada/lib-xref-spark_specific.adb index a30cb84..5295832 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; diff --git a/gcc/ada/lib-xref.ads b/gcc/ada/lib-xref.ads index a01e9d3..0baa896 100644 --- a/gcc/ada/lib-xref.ads +++ b/gcc/ada/lib-xref.ads @@ -26,7 +26,8 @@ -- This package contains for collecting and outputting cross-reference -- information. -with Einfo; use Einfo; +with Einfo; use Einfo; +with SPARK_Xrefs; package Lib.Xref is @@ -638,12 +639,15 @@ package Lib.Xref is -- This procedure is called to record a dereference. N is the location -- of the dereference. - procedure Collect_SPARK_Xrefs - (Sdep_Table : Unit_Ref_Table; - Num_Sdep : Nat); - -- Collect SPARK cross-reference information from library units (for - -- files and scopes) and from shared cross-references. Fill in the - -- tables in library package called SPARK_Xrefs. + generic + with procedure Process + (Index : Int; + Xref : SPARK_Xrefs.SPARK_Xref_Record); + procedure Iterate_SPARK_Xrefs; + -- Call Process on cross-references relevant to the SPARK backend with + -- parameter Xref holding the relevant subset of the xref entry and + -- Index holding the position in the original tables with references + -- (if positive) or dereferences (if negative). end SPARK_Specific; diff --git a/gcc/ada/sem_elab.adb b/gcc/ada/sem_elab.adb index bc86558..b3077ad 100644 --- a/gcc/ada/sem_elab.adb +++ b/gcc/ada/sem_elab.adb @@ -68,7 +68,7 @@ package body Sem_Elab is -- * Diagnose at compile-time or install run-time checks to prevent ABE -- access to data and behaviour. -- - -- The high level idea is to accurately diagnose ABE issues within a + -- The high-level idea is to accurately diagnose ABE issues within a -- single unit because the ABE mechanism can inspect the whole unit. -- As soon as the elaboration graph extends to an external unit, the -- diagnostics stop because the body of the unit may not be available. @@ -146,8 +146,8 @@ package body Sem_Elab is -- the library level if it appears in a package library unit, ignoring -- enclosng packages. -- - -- * Non-library level encapsulator - A construct that cannot be elaborated - -- on its own and requires elaboration by a top level scenario. + -- * Non-library-level encapsulator - A construct that cannot be elaborated + -- on its own and requires elaboration by a top-level scenario. -- -- * Scenario - A construct or context which may be elaborated or executed -- by elaboration code. The scenarios recognized by the ABE mechanism are @@ -181,7 +181,7 @@ package body Sem_Elab is -- -- - For task activation, the target is the task body -- - -- * Top level scenario - A scenario which appears in a non-generic main + -- * Top-level scenario - A scenario which appears in a non-generic main -- unit. Depending on the elaboration model is in effect, the following -- addotional restrictions apply: -- @@ -198,7 +198,7 @@ package body Sem_Elab is -- The Recording phase coincides with the analysis/resolution phase of the -- compiler. It has the following objectives: -- - -- * Record all top level scenarios for examination by the Processing + -- * Record all top-level scenarios for examination by the Processing -- phase. -- -- Saving only a certain number of nodes improves the performance of @@ -231,9 +231,9 @@ package body Sem_Elab is -- and/or inlining of bodies, but before the removal of Ghost code. It has -- the following objectives: -- - -- * Examine all top level scenarios saved during the Recording phase + -- * Examine all top-level scenarios saved during the Recording phase -- - -- The top level scenarios act as roots for depth-first traversal of + -- The top-level scenarios act as roots for depth-first traversal of -- the call/instantiation/task activation graph. The traversal stops -- when an outgoing edge leaves the main unit. -- @@ -420,8 +420,7 @@ package body Sem_Elab is -- The following steps describe how to add a new elaboration scenario and -- preserve the existing architecture. -- - -- 1) If necessary, update predicates Is_Check_Emitting_Scenario and - -- Is_Scenario. + -- 1) If necessary, update predicate Is_Scenario -- -- 2) Add predicate Is_Suitable_xxx. Include a call to it in predicate -- Is_Suitable_Scenario. @@ -712,8 +711,28 @@ package body Sem_Elab is Hash => Elaboration_Context_Hash, Equal => "="); + -- The following table stores a status flag for each top-level scenario + -- recorded in table Top_Level_Scenarios. + + Recorded_Top_Level_Scenarios_Max : constant := 503; + + type Recorded_Top_Level_Scenarios_Index is + range 0 .. Recorded_Top_Level_Scenarios_Max - 1; + + function Recorded_Top_Level_Scenarios_Hash + (Key : Node_Id) return Recorded_Top_Level_Scenarios_Index; + -- Obtain the hash value of entity Key + + package Recorded_Top_Level_Scenarios is new Simple_HTable + (Header_Num => Recorded_Top_Level_Scenarios_Index, + Element => Boolean, + No_Element => False, + Key => Node_Id, + Hash => Recorded_Top_Level_Scenarios_Hash, + Equal => "="); + -- The following table stores all active scenarios in a recursive traversal - -- starting from a top level scenario. This table must be maintained in a + -- starting from a top-level scenario. This table must be maintained in a -- FIFO fashion. package Scenario_Stack is new Table.Table @@ -724,7 +743,7 @@ package body Sem_Elab is Table_Increment => 100, Table_Name => "Scenario_Stack"); - -- The following table stores all top level scenario saved during the + -- The following table stores all top-level scenario saved during the -- Recording phase. The contents of this table act as traversal roots -- later in the Processing phase. This table must be maintained in a -- LIFO fashion. @@ -738,7 +757,7 @@ package body Sem_Elab is Table_Name => "Top_Level_Scenarios"); -- The following table stores the bodies of all eligible scenarios visited - -- during a traversal starting from a top level scenario. The contents of + -- during a traversal starting from a top-level scenario. The contents of -- this table must be reset upon each new traversal. Visited_Bodies_Max : constant := 511; @@ -867,7 +886,7 @@ package body Sem_Elab is -- Return the code unit which contains arbitrary node or entity N. This -- is the unit of the file which physically contains the related construct -- denoted by N except when N is within an instantiation. In that case the - -- unit is that of the top level instantiation. + -- unit is that of the top-level instantiation. procedure Find_Elaborated_Units; -- Populate table Elaboration_Context with all units which have prior @@ -1019,11 +1038,6 @@ package body Sem_Elab is pragma Inline (Is_Bodiless_Subprogram); -- Determine whether subprogram Subp_Id will never have a body - function Is_Check_Emitting_Scenario (N : Node_Id) return Boolean; - pragma Inline (Is_Check_Emitting_Scenario); - -- Determine whether arbitrary node N denotes a scenario which may emit a - -- conditional ABE check. - function Is_Controlled_Proc (Subp_Id : Entity_Id; Subp_Nam : Name_Id) return Boolean; @@ -1101,6 +1115,11 @@ package body Sem_Elab is -- Determine whether entity Id denotes the protected or unprotected version -- of a protected subprogram. + function Is_Recorded_Top_Level_Scenario (N : Node_Id) return Boolean; + pragma Inline (Is_Recorded_Top_Level_Scenario); + -- Determine whether arbitrary node is a recorded top-level scenario which + -- appears in table Top_Level_Scenarios. + function Is_Safe_Activation (Call : Node_Id; Task_Decl : Node_Id) return Boolean; @@ -1329,14 +1348,14 @@ package body Sem_Elab is -- routine. procedure Process_Guaranteed_ABE (N : Node_Id); - -- Top level dispatcher for processing of scenarios which result in a + -- Top-level dispatcher for processing of scenarios which result in a -- guaranteed ABE. procedure Process_Instantiation (Exp_Inst : Node_Id; In_Partial_Fin : Boolean; In_Task_Body : Boolean); - -- Top level dispatcher for processing of instantiations. Perform ABE + -- Top-level dispatcher for processing of instantiations. Perform ABE -- checks and diagnostics for expanded instantiation Exp_Inst. Flag -- In_Partial_Fin shoud be set when the processing is initiated by a -- partial finalization routine. Flag In_Task_Body should be set when @@ -1393,14 +1412,14 @@ package body Sem_Elab is (N : Node_Id; In_Partial_Fin : Boolean := False; In_Task_Body : Boolean := False); - -- Top level dispatcher for processing of various elaboration scenarios. + -- Top-level dispatcher for processing of various elaboration scenarios. -- Perform ABE checks and diagnostics for scenario N. Flag In_Partial_Fin -- shoud be set when the processing is initiated by a partial finalization -- routine. Flag In_Task_Body should be set when the processing is started -- from a task body. procedure Process_Variable_Assignment (Asmt : Node_Id); - -- Top level dispatcher for processing of variable assignments. Perform ABE + -- Top-level dispatcher for processing of variable assignments. Perform ABE -- checks and diagnostics for assignment statement Asmt. procedure Process_Variable_Assignment_Ada @@ -1416,7 +1435,7 @@ package body Sem_Elab is -- updates the value of variable Var_Id using the SPARK rules. procedure Process_Variable_Reference (Ref : Node_Id); - -- Top level dispatcher for processing of variable references. Perform ABE + -- Top-level dispatcher for processing of variable references. Perform ABE -- checks and diagnostics for variable reference Ref. procedure Process_Variable_Reference_Read @@ -1432,10 +1451,16 @@ package body Sem_Elab is function Root_Scenario return Node_Id; pragma Inline (Root_Scenario); - -- Return the top level scenario which started a recursive search for other - -- scenarios. It is assumed that there is a valid top level scenario on the + -- Return the top-level scenario which started a recursive search for other + -- scenarios. It is assumed that there is a valid top-level scenario on the -- active scenario stack. + procedure Set_Is_Recorded_Top_Level_Scenario + (N : Node_Id; + Val : Boolean := True); + pragma Inline (Set_Is_Recorded_Top_Level_Scenario); + -- Mark scenario N as being recorded in table Top_Level_Scenarios + function Static_Elaboration_Checks return Boolean; pragma Inline (Static_Elaboration_Checks); -- Determine whether the static model is in effect @@ -1970,12 +1995,12 @@ package body Sem_Elab is Find_Elaborated_Units; - -- Examine each top level scenario saved during the Recording phase and + -- Examine each top-level scenario saved during the Recording phase and -- perform various actions depending on the elaboration model in effect. for Index in Top_Level_Scenarios.First .. Top_Level_Scenarios.Last loop - -- Clear the table of visited scenario bodies for each new top level + -- Clear the table of visited scenario bodies for each new top-level -- scenario. Visited_Bodies.Reset; @@ -2046,7 +2071,7 @@ package body Sem_Elab is Level := Find_Enclosing_Level (Call); - -- Library level calls are always considered because they are part of + -- Library-level calls are always considered because they are part of -- the associated unit's elaboration actions. if Level in Library_Level then @@ -3589,7 +3614,7 @@ package body Sem_Elab is return Declaration_Level; end if; - -- The current construct is a declaration level encapsulator + -- The current construct is a declaration-level encapsulator elsif Nkind_In (Curr, N_Entry_Body, N_Subprogram_Body, @@ -3612,9 +3637,9 @@ package body Sem_Elab is return Declaration_Level; end if; - -- The current construct is a non-library level encapsulator which + -- The current construct is a non-library-level encapsulator which -- indicates that the node cannot possibly appear at any level. - -- Note that this check must come after the declaration level check + -- Note that this check must come after the declaration-level check -- because both predicates share certain nodes. elsif Is_Non_Library_Level_Encapsulator (Curr) then @@ -4103,7 +4128,7 @@ package body Sem_Elab is Nested_OK : Boolean := False) return Boolean is function Find_Enclosing_Context (N : Node_Id) return Node_Id; - -- Return the nearest enclosing non-library level or compilation unit + -- Return the nearest enclosing non-library-level or compilation unit -- node which which encapsulates arbitrary node N. Return Empty is no -- such context is available. @@ -4149,7 +4174,7 @@ package body Sem_Elab is return Par; end if; - -- Reaching a compilation unit node without hitting a non-library + -- Reaching a compilation unit node without hitting a non-library- -- level encapsulator indicates that N is at the library level in -- which case the compilation unit is the context. @@ -4231,7 +4256,7 @@ package body Sem_Elab is procedure Initialize is begin - -- Set the soft link which enables Atree.Rewrite to update a top level + -- Set the soft link which enables Atree.Rewrite to update a top-level -- scenario each time it is transformed into another node. Set_Rewriting_Proc (Update_Elaboration_Scenario'Access); @@ -4837,19 +4862,6 @@ package body Sem_Elab is return False; end Is_Bodiless_Subprogram; - -------------------------------- - -- Is_Check_Emitting_Scenario -- - -------------------------------- - - function Is_Check_Emitting_Scenario (N : Node_Id) return Boolean is - begin - return - Nkind_In (N, N_Call_Marker, - N_Function_Instantiation, - N_Package_Instantiation, - N_Procedure_Instantiation); - end Is_Check_Emitting_Scenario; - ------------------------ -- Is_Controlled_Proc -- ------------------------ @@ -5105,6 +5117,15 @@ package body Sem_Elab is and then Present (Protected_Subprogram (Id)); end Is_Protected_Body_Subp; + ------------------------------------ + -- Is_Recorded_Top_Level_Scenario -- + ------------------------------------ + + function Is_Recorded_Top_Level_Scenario (N : Node_Id) return Boolean is + begin + return Recorded_Top_Level_Scenarios.Get (N); + end Is_Recorded_Top_Level_Scenario; + ------------------------ -- Is_Safe_Activation -- ------------------------ @@ -5568,7 +5589,7 @@ package body Sem_Elab is begin -- The root appears within the declaratons of a block statement, entry -- body, subprogram body, or task body ignoring enclosing packages. The - -- root is always within the main unit. An up level target is a notion + -- root is always within the main unit. An up-level target is a notion -- applicable only to the static model because scenarios are reached by -- means of graph traversal started from a fixed declarative or library -- level. @@ -5578,7 +5599,7 @@ package body Sem_Elab is if Static_Elaboration_Checks and then Find_Enclosing_Level (Root) = Declaration_Level then - -- The target is within the main unit. It acts as an up level target + -- The target is within the main unit. It acts as an up-level target -- when it appears within a context which encloses the root. -- package body Main_Unit is @@ -5594,7 +5615,7 @@ package body Sem_Elab is return not In_Same_Context (Root, Target_Decl, Nested_OK => True); -- Otherwise the target is external to the main unit which makes it - -- an up level target. + -- an up-level target. else return True; @@ -5609,14 +5630,32 @@ package body Sem_Elab is ------------------------------- procedure Kill_Elaboration_Scenario (N : Node_Id) is + package Scenarios renames Top_Level_Scenarios; + begin - -- Eliminate the scenario by suppressing the generation of conditional - -- ABE checks or guaranteed ABE failures. Note that other diagnostics - -- must be carried out ignoring the fact that the scenario is within - -- dead code. + -- Eliminate a recorded top-level scenario when it appears within dead + -- code because it will not be executed at elaboration time. - if Is_Scenario (N) then - Set_Is_Elaboration_Checks_OK_Node (N, False); + if Is_Scenario (N) + and then Is_Recorded_Top_Level_Scenario (N) + then + -- Performance node: list traversal + + for Index in Scenarios.First .. Scenarios.Last loop + if Scenarios.Table (Index) = N then + Scenarios.Table (Index) := Empty; + + -- The top-level scenario is no longer recorded + + Set_Is_Recorded_Top_Level_Scenario (N, False); + return; + end if; + end loop; + + -- A recorded top-level scenario must be in the table of recorded + -- top-level scenarios. + + pragma Assert (False); end if; end Kill_Elaboration_Scenario; @@ -8352,7 +8391,7 @@ package body Sem_Elab is return; end if; - -- Ensure that a library level call does not appear in a preelaborated + -- Ensure that a library-level call does not appear in a preelaborated -- unit. The check must come before ignoring scenarios within external -- units or inside generics because calls in those context must also be -- verified. @@ -8426,23 +8465,23 @@ package body Sem_Elab is Level := Find_Enclosing_Level (N); - -- Declaration level scenario + -- Declaration-level scenario if Declaration_Level_OK and then Level = Declaration_Level then null; - -- Library level scenario + -- Library-level scenario elsif Level in Library_Level then null; - -- Instantiation library level scenario + -- Instantiation library-level scenario elsif Level = Instantiation then null; -- Otherwise the scenario does not appear at the proper level and - -- cannot possibly act as a top level scenario. + -- cannot possibly act as a top-level scenario. else return; @@ -8459,16 +8498,21 @@ package body Sem_Elab is -- later processing by the ABE phase. Top_Level_Scenarios.Append (N); + Set_Is_Recorded_Top_Level_Scenario (N); + end Record_Elaboration_Scenario; - -- Mark a scenario which may produce run-time conditional ABE checks or - -- guaranteed ABE failures as recorded. The flag ensures that scenario - -- rewriting performed by Atree.Rewrite will be properly reflected in - -- all relevant internal data structures. + --------------------------------------- + -- Recorded_Top_Level_Scenarios_Hash -- + --------------------------------------- - if Is_Check_Emitting_Scenario (N) then - Set_Is_Recorded_Scenario (N); - end if; - end Record_Elaboration_Scenario; + function Recorded_Top_Level_Scenarios_Hash + (Key : Node_Id) return Recorded_Top_Level_Scenarios_Index + is + begin + return + Recorded_Top_Level_Scenarios_Index + (Key mod Recorded_Top_Level_Scenarios_Max); + end Recorded_Top_Level_Scenarios_Hash; ------------------- -- Root_Scenario -- @@ -8485,6 +8529,18 @@ package body Sem_Elab is return Stack.Table (Stack.First); end Root_Scenario; + ---------------------------------------- + -- Set_Is_Recorded_Top_Level_Scenario -- + ---------------------------------------- + + procedure Set_Is_Recorded_Top_Level_Scenario + (N : Node_Id; + Val : Boolean := True) + is + begin + Recorded_Top_Level_Scenarios.Set (N, Val); + end Set_Is_Recorded_Top_Level_Scenario; + ------------------------------- -- Static_Elaboration_Checks -- ------------------------------- @@ -8590,7 +8646,7 @@ package body Sem_Elab is -- Save a suitable scenario in the Nested_Scenarios list of the -- subprogram body. As a result any subsequent traversals of the - -- subprogram body started from a different top level scenario no + -- subprogram body started from a different top-level scenario no -- longer need to reexamine the tree. elsif Is_Suitable_Scenario (Nod) then @@ -8683,7 +8739,7 @@ package body Sem_Elab is end if; -- Nothing to do if the body was already traversed during the processing - -- of the same top level scenario. + -- of the same top-level scenario. if Visited_Bodies.Get (N) then return; @@ -8697,7 +8753,7 @@ package body Sem_Elab is Nested := Nested_Scenarios (Defining_Entity (N)); -- The subprogram body was already examined as part of the elaboration - -- graph starting from a different top level scenario. There is no need + -- graph starting from a different top-level scenario. There is no need -- to traverse the declarations and statements again because this will -- yield the exact same scenarios. Use the nested scenarios collected -- during the first inspection of the body. @@ -8721,14 +8777,18 @@ package body Sem_Elab is package Scenarios renames Top_Level_Scenarios; begin + -- Nothing to do when the old and new scenarios are one and the same + + if Old_N = New_N then + return; + -- A scenario is being transformed by Atree.Rewrite. Update all relevant -- internal data structures to reflect this change. This ensures that a -- potential run-time conditional ABE check or a guaranteed ABE failure -- is inserted at the proper place in the tree. - if Is_Check_Emitting_Scenario (Old_N) - and then Is_Recorded_Scenario (Old_N) - and then Old_N /= New_N + elsif Is_Scenario (Old_N) + and then Is_Recorded_Top_Level_Scenario (Old_N) then -- Performance note: list traversal @@ -8736,13 +8796,17 @@ package body Sem_Elab is if Scenarios.Table (Index) = Old_N then Scenarios.Table (Index) := New_N; - Set_Is_Recorded_Scenario (Old_N, False); - Set_Is_Recorded_Scenario (New_N); + -- The old top-level scenario is no longer recorded, but the + -- new one is. + + Set_Is_Recorded_Top_Level_Scenario (Old_N, False); + Set_Is_Recorded_Top_Level_Scenario (New_N); return; end if; end loop; - -- A recorded scenario must be in the table of recorded scenarios + -- A recorded top-level scenario must be in the table of recorded + -- top-level scenarios. pragma Assert (False); end if; diff --git a/gcc/ada/sem_prag.adb b/gcc/ada/sem_prag.adb index e70ae54..0f6223e 100644 --- a/gcc/ada/sem_prag.adb +++ b/gcc/ada/sem_prag.adb @@ -3327,7 +3327,7 @@ package body Sem_Prag is elsif Placement = Private_State_Space then if Scope (Encap_Id) /= Pack_Id then SPARK_Msg_NE - ("indicator Part_Of must designate an abstract state of " + ("indicator Part_Of must denote an abstract state of " & "package & (SPARK RM 7.2.6(2))", Indic, Pack_Id); Error_Msg_Name_1 := Chars (Pack_Id); SPARK_Msg_NE diff --git a/gcc/ada/sem_res.adb b/gcc/ada/sem_res.adb index 85621fd..3faeb55 100644 --- a/gcc/ada/sem_res.adb +++ b/gcc/ada/sem_res.adb @@ -5161,11 +5161,11 @@ package body Sem_Res is (Parent (Associated_Node_For_Itype (Typ)))) then Error_Msg_N - ("info: coextension will not be finalized when its " + ("??coextension will not be finalized when its " & "associated owner is finalized", N); else Error_Msg_N - ("info: coextension will not be finalized when its " + ("??coextension will not be finalized when its " & "associated owner is deallocated", N); end if; else @@ -5174,12 +5174,12 @@ package body Sem_Res is (Parent (Associated_Node_For_Itype (Typ)))) then Error_Msg_N - ("info: coextension will not be deallocated when its " - & "associated owner is finalized", N); + ("??coextension will not be deallocated when " + & "its associated owner is finalized", N); else Error_Msg_N - ("info: coextension will not be deallocated when its " - & "associated owner is deallocated", N); + ("??coextension will not be deallocated when " + & "its associated owner is deallocated", N); end if; end if; end if; @@ -5189,6 +5189,19 @@ package body Sem_Res is else Set_Is_Dynamic_Coextension (N, False); Set_Is_Static_Coextension (N, False); + + -- ??? It seems we also do not properly finalize anonymous + -- access-to-controlled objects within their declared scope and + -- instead finalize them with their associated unit. Warn the + -- user about it here. + + if Ekind (Typ) = E_Anonymous_Access_Type + and then Is_Controlled_Active (Desig_T) + then + Error_Msg_N ("??anonymous access-to-controlled object will " + & "be finalized when its enclosing unit goes out " + & "of scope", N); + end if; end if; end if; diff --git a/gcc/ada/sinfo.adb b/gcc/ada/sinfo.adb index 5514291..20ff3b2 100644 --- a/gcc/ada/sinfo.adb +++ b/gcc/ada/sinfo.adb @@ -2098,17 +2098,6 @@ package body Sinfo is return Flag1 (N); end Is_Read; - function Is_Recorded_Scenario - (N : Node_Id) return Boolean is - begin - pragma Assert (False - or else NT (N).Nkind = N_Call_Marker - or else NT (N).Nkind = N_Function_Instantiation - or else NT (N).Nkind = N_Package_Instantiation - or else NT (N).Nkind = N_Procedure_Instantiation); - return Flag6 (N); - end Is_Recorded_Scenario; - function Is_Source_Call (N : Node_Id) return Boolean is begin @@ -5537,17 +5526,6 @@ package body Sinfo is Set_Flag1 (N, Val); end Set_Is_Read; - procedure Set_Is_Recorded_Scenario - (N : Node_Id; Val : Boolean := True) is - begin - pragma Assert (False - or else NT (N).Nkind = N_Call_Marker - or else NT (N).Nkind = N_Function_Instantiation - or else NT (N).Nkind = N_Package_Instantiation - or else NT (N).Nkind = N_Procedure_Instantiation); - Set_Flag6 (N, Val); - end Set_Is_Recorded_Scenario; - procedure Set_Is_Source_Call (N : Node_Id; Val : Boolean := True) is begin diff --git a/gcc/ada/sinfo.ads b/gcc/ada/sinfo.ads index 21e7bb9..3c3c9fb 100644 --- a/gcc/ada/sinfo.ads +++ b/gcc/ada/sinfo.ads @@ -1867,12 +1867,6 @@ package Sinfo is -- Present in variable reference markers. Set when the original variable -- reference constitues a read of the variable. - -- Is_Recorded_Scenario (Flag6-Sem) - -- Present in call marker and instantiation nodes. Set when the scenario - -- was saved by the ABE Recording phase. This flag aids the ABE machinery - -- to keep its internal data up-to-date in case the node is transformed - -- by Atree.Rewrite. - -- Is_Source_Call (Flag4-Sem) -- Present in call marker nodes. Set when the related call came from -- source. @@ -7045,7 +7039,6 @@ package Sinfo is -- Is_Elaboration_Checks_OK_Node (Flag1-Sem) -- Is_SPARK_Mode_On_Node (Flag2-Sem) -- Is_Declaration_Level_Node (Flag5-Sem) - -- Is_Recorded_Scenario (Flag6-Sem) -- Is_Known_Guaranteed_ABE (Flag18-Sem) -- N_Procedure_Instantiation @@ -7059,7 +7052,6 @@ package Sinfo is -- Is_Elaboration_Checks_OK_Node (Flag1-Sem) -- Is_SPARK_Mode_On_Node (Flag2-Sem) -- Is_Declaration_Level_Node (Flag5-Sem) - -- Is_Recorded_Scenario (Flag6-Sem) -- Must_Override (Flag14) set if overriding indicator present -- Must_Not_Override (Flag15) set if not_overriding indicator present -- Is_Known_Guaranteed_ABE (Flag18-Sem) @@ -7075,7 +7067,6 @@ package Sinfo is -- Is_Elaboration_Checks_OK_Node (Flag1-Sem) -- Is_SPARK_Mode_On_Node (Flag2-Sem) -- Is_Declaration_Level_Node (Flag5-Sem) - -- Is_Recorded_Scenario (Flag6-Sem) -- Must_Override (Flag14) set if overriding indicator present -- Must_Not_Override (Flag15) set if not_overriding indicator present -- Is_Known_Guaranteed_ABE (Flag18-Sem) @@ -7833,7 +7824,6 @@ package Sinfo is -- Is_Dispatching_Call (Flag3-Sem) -- Is_Source_Call (Flag4-Sem) -- Is_Declaration_Level_Node (Flag5-Sem) - -- Is_Recorded_Scenario (Flag6-Sem) -- Is_Known_Guaranteed_ABE (Flag18-Sem) ------------------------ @@ -9777,9 +9767,6 @@ package Sinfo is function Is_Read (N : Node_Id) return Boolean; -- Flag1 - function Is_Recorded_Scenario - (N : Node_Id) return Boolean; -- Flag6 - function Is_Source_Call (N : Node_Id) return Boolean; -- Flag4 @@ -10872,9 +10859,6 @@ package Sinfo is procedure Set_Is_Read (N : Node_Id; Val : Boolean := True); -- Flag1 - procedure Set_Is_Recorded_Scenario - (N : Node_Id; Val : Boolean := True); -- Flag6 - procedure Set_Is_Source_Call (N : Node_Id; Val : Boolean := True); -- Flag4 @@ -13337,7 +13321,6 @@ package Sinfo is pragma Inline (Is_Protected_Subprogram_Body); pragma Inline (Is_Qualified_Universal_Literal); pragma Inline (Is_Read); - pragma Inline (Is_Recorded_Scenario); pragma Inline (Is_Source_Call); pragma Inline (Is_SPARK_Mode_On_Node); pragma Inline (Is_Static_Coextension); @@ -13697,7 +13680,6 @@ package Sinfo is pragma Inline (Set_Is_Protected_Subprogram_Body); pragma Inline (Set_Is_Qualified_Universal_Literal); pragma Inline (Set_Is_Read); - pragma Inline (Set_Is_Recorded_Scenario); pragma Inline (Set_Is_Source_Call); pragma Inline (Set_Is_SPARK_Mode_On_Node); pragma Inline (Set_Is_Static_Coextension); diff --git a/gcc/ada/spark_xrefs.adb b/gcc/ada/spark_xrefs.adb index cea28a6..e59114d 100644 --- a/gcc/ada/spark_xrefs.adb +++ b/gcc/ada/spark_xrefs.adb @@ -23,6 +23,7 @@ -- -- ------------------------------------------------------------------------------ +with Lib.Xref; with Output; use Output; with Sem_Util; use Sem_Util; @@ -33,92 +34,48 @@ package body SPARK_Xrefs is ------------ procedure dspark is - begin - -- Dump SPARK cross-reference file table - - Write_Line ("SPARK Xrefs File Table"); - Write_Line ("----------------------"); - - for Index in SPARK_File_Table.First .. SPARK_File_Table.Last loop - declare - AFR : SPARK_File_Record renames SPARK_File_Table.Table (Index); - - begin - Write_Str (" "); - Write_Int (Int (Index)); - Write_Str (". File_Num = "); - Write_Int (Int (AFR.File_Num)); - Write_Str (" From = "); - Write_Int (Int (AFR.From_Scope)); - Write_Str (" To = "); - Write_Int (Int (AFR.To_Scope)); - Write_Eol; - end; - end loop; - - -- Dump SPARK cross-reference scope table - Write_Eol; - Write_Line ("SPARK Xrefs Scope Table"); - Write_Line ("-----------------------"); + procedure Dump (Index : Nat; AXR : SPARK_Xref_Record); + + procedure Dump_SPARK_Xrefs is new + Lib.Xref.SPARK_Specific.Iterate_SPARK_Xrefs (Dump); + + ---------- + -- Dump -- + ---------- + + procedure Dump (Index : Nat; AXR : SPARK_Xref_Record) is + begin + Write_Str (" "); + Write_Int (Index); + Write_Char ('.'); + + Write_Str (" Entity = " & Unique_Name (AXR.Entity)); + Write_Str (" ("); + Write_Int (Nat (AXR.Entity)); + Write_Str (")"); - for Index in SPARK_Scope_Table.First .. SPARK_Scope_Table.Last loop - declare - ASR : SPARK_Scope_Record renames SPARK_Scope_Table.Table (Index); + Write_Str (" Scope = " & Unique_Name (AXR.Ref_Scope)); + Write_Str (" ("); + Write_Int (Nat (AXR.Ref_Scope)); + Write_Str (")"); - begin - Write_Str (" "); - Write_Int (Int (Index)); - Write_Str (" Scope_Name = """); + Write_Str (" Ref_Type = '" & AXR.Rtype & "'"); - Write_Str (Unique_Name (ASR.Entity)); + Write_Eol; + end Dump; - Write_Char ('"'); - Write_Str (" From = "); - Write_Int (Int (ASR.From_Xref)); - Write_Str (" To = "); - Write_Int (Int (ASR.To_Xref)); - Write_Eol; - end; - end loop; + -- Start of processing for dspark + begin -- Dump SPARK cross-reference table Write_Eol; Write_Line ("SPARK Xref Table"); Write_Line ("----------------"); - for Index in SPARK_Xref_Table.First .. SPARK_Xref_Table.Last loop - declare - AXR : SPARK_Xref_Record renames SPARK_Xref_Table.Table (Index); - - begin - Write_Str (" "); - Write_Int (Int (Index)); - Write_Str (". Entity_Name = """); - - Write_Str (Unique_Name (AXR.Entity)); - - Write_Char ('"'); - Write_Str (" Reference_Scope = "); - Write_Str (Unique_Name (AXR.Ref_Scope)); - Write_Char ('"'); - Write_Str (" Type = "); - Write_Char (AXR.Rtype); - Write_Eol; - end; - end loop; - end dspark; - - ---------------- - -- Initialize -- - ---------------- + Dump_SPARK_Xrefs; - procedure Initialize_SPARK_Tables is - begin - SPARK_File_Table.Init; - SPARK_Scope_Table.Init; - SPARK_Xref_Table.Init; - end Initialize_SPARK_Tables; + end dspark; end SPARK_Xrefs; diff --git a/gcc/ada/spark_xrefs.ads b/gcc/ada/spark_xrefs.ads index df1d8e8..25af902 100644 --- a/gcc/ada/spark_xrefs.ads +++ b/gcc/ada/spark_xrefs.ads @@ -23,48 +23,13 @@ -- -- ------------------------------------------------------------------------------ --- This package defines tables used to store information needed for the SPARK --- mode. It is used by procedures in Lib.Xref.SPARK_Specific to build the --- SPARK-specific cross-reference information. +-- This package defines data structures used to expose frontend +-- cross-references to the SPARK backend. -with Table; with Types; use Types; package SPARK_Xrefs is - -- SPARK cross-reference information is stored internally using three - -- tables: SPARK_Xref_Table, SPARK_Scope_Table and SPARK_File_Table, which - -- are defined in this unit. - - -- Lib.Xref.SPARK_Specific is part of the compiler. It extracts SPARK - -- cross-reference information from the complete set of cross-references - -- generated during compilation. - - -- ------------------------------- - -- -- Generated Globals Section -- - -- ------------------------------- - - -- The Generated Globals section is located at the end of the ALI file - - -- All lines with information related to the Generated Globals begin with - -- string "GG". This string should therefore not be used in the beginning - -- of any line not related to Generated Globals. - - -- The processing (reading and writing) of this section happens in package - -- Flow_Generated_Globals (from the SPARK 2014 sources), for further - -- information please refer there. - - ---------------- - -- Xref Table -- - ---------------- - - -- The following table records SPARK cross-references - - type Xref_Index is new Nat; - -- Used to index values in this table. Values start at 1 and are assigned - -- sequentially as entries are constructed; value 0 is used temporarily - -- until a proper value is determined. - type SPARK_Xref_Record is record Entity : Entity_Id; -- Referenced entity @@ -78,80 +43,8 @@ package SPARK_Xrefs is -- m = modification -- s = call end record; - - package SPARK_Xref_Table is new Table.Table ( - Table_Component_Type => SPARK_Xref_Record, - Table_Index_Type => Xref_Index, - Table_Low_Bound => 1, - Table_Initial => 2000, - Table_Increment => 300, - Table_Name => "Xref_Table"); - - ----------------- - -- Scope Table -- - ----------------- - - -- This table keeps track of the scopes and the corresponding starting and - -- ending indexes (From, To) in the Xref table. - - type Scope_Index is new Nat; - -- Used to index values in this table. Values start at 1 and are assigned - -- sequentially as entries are constructed; value 0 indicates that no - -- entries have been constructed and is also used until a proper value is - -- determined. - - type SPARK_Scope_Record is record - Entity : Entity_Id; - -- Entity that is represented by the scope - - Scope_Num : Pos; - -- Set to the scope number within the enclosing unit - - From_Xref : Xref_Index; - -- Starting index in Xref table for this scope - - To_Xref : Xref_Index; - -- Ending index in Xref table for this scope - end record; - - package SPARK_Scope_Table is new Table.Table ( - Table_Component_Type => SPARK_Scope_Record, - Table_Index_Type => Scope_Index, - Table_Low_Bound => 1, - Table_Initial => 200, - Table_Increment => 300, - Table_Name => "Scope_Table"); - - ---------------- - -- File Table -- - ---------------- - - -- This table keeps track of the units and the corresponding starting and - -- ending indexes (From, To) in the Scope table. - - type File_Index is new Nat; - -- Used to index values in this table. Values start at 1 and are assigned - -- sequentially as entries are constructed; value 0 indicates that no - -- entries have been constructed. - - type SPARK_File_Record is record - File_Num : Nat; - -- Dependency number in ALI file - - From_Scope : Scope_Index; - -- Starting index in Scope table for this unit - - To_Scope : Scope_Index; - -- Ending index in Scope table for this unit - end record; - - package SPARK_File_Table is new Table.Table ( - Table_Component_Type => SPARK_File_Record, - Table_Index_Type => File_Index, - Table_Low_Bound => 1, - Table_Initial => 20, - Table_Increment => 200, - Table_Name => "File_Table"); + -- This type holds a subset of the frontend xref entry that is needed by + -- the SPARK backend. --------------- -- Constants -- @@ -170,9 +63,6 @@ package SPARK_Xrefs is -- Subprograms -- ----------------- - procedure Initialize_SPARK_Tables; - -- Reset tables for a new compilation - procedure dspark; -- Debug routine to dump internal SPARK cross-reference tables. This is a -- raw format dump showing exactly what the tables contain. diff --git a/gcc/ada/switch-c.adb b/gcc/ada/switch-c.adb index 5ad10e3..c1ff88d 100644 --- a/gcc/ada/switch-c.adb +++ b/gcc/ada/switch-c.adb @@ -337,19 +337,7 @@ package body Switch.C is when 'C' => Ptr := Ptr + 1; - - if not CodePeer_Mode then - CodePeer_Mode := True; - - -- Suppress compiler warnings by default, since what we are - -- interested in here is what CodePeer can find out. Note - -- that if -gnatwxxx is specified after -gnatC on the - -- command line, we do not want to override this setting in - -- Adjust_Global_Switches, and assume that the user wants to - -- get both warnings from GNAT and CodePeer messages. - - Warning_Mode := Suppress; - end if; + CodePeer_Mode := True; -- -gnatd (compiler debug options) diff --git a/gcc/testsuite/ChangeLog b/gcc/testsuite/ChangeLog index cb577bf..f3dbf60 100644 --- a/gcc/testsuite/ChangeLog +++ b/gcc/testsuite/ChangeLog @@ -1,3 +1,13 @@ +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. + 2017-11-09 Jakub Jelinek PR debug/82837 diff --git a/gcc/testsuite/gnat.dg/controlled2.adb b/gcc/testsuite/gnat.dg/controlled2.adb index 4fa61af..5b7eedd 100644 --- a/gcc/testsuite/gnat.dg/controlled2.adb +++ b/gcc/testsuite/gnat.dg/controlled2.adb @@ -1,5 +1,8 @@ -- { dg-do compile } +pragma Warnings + (Off, "anonymous access-to-controlled object will be finalized when its enclosing unit goes out of scope"); + with controlled1; use controlled1; package body controlled2 is procedure Test_Suite is diff --git a/gcc/testsuite/gnat.dg/controlled4.adb b/gcc/testsuite/gnat.dg/controlled4.adb index b823cc9..9809dc6 100644 --- a/gcc/testsuite/gnat.dg/controlled4.adb +++ b/gcc/testsuite/gnat.dg/controlled4.adb @@ -1,5 +1,8 @@ -- { dg-do compile } +pragma Warnings + (Off, "anonymous access-to-controlled object will be finalized when its enclosing unit goes out of scope"); + package body controlled4 is procedure Test_Suite is begin diff --git a/gcc/testsuite/gnat.dg/elab3.adb b/gcc/testsuite/gnat.dg/elab3.adb new file mode 100644 index 0000000..2c0a4b2 --- /dev/null +++ b/gcc/testsuite/gnat.dg/elab3.adb @@ -0,0 +1,9 @@ +-- { dg-do compile } + +with Elab3_Pkg; + +package body Elab3 is + package Inst is new Elab3_Pkg (False, ABE); + + procedure ABE is begin null; end ABE; +end Elab3; diff --git a/gcc/testsuite/gnat.dg/elab3.ads b/gcc/testsuite/gnat.dg/elab3.ads new file mode 100644 index 0000000..92fd4c3 --- /dev/null +++ b/gcc/testsuite/gnat.dg/elab3.ads @@ -0,0 +1,3 @@ +package Elab3 is + procedure ABE; +end Elab3; diff --git a/gcc/testsuite/gnat.dg/elab3_pkg.adb b/gcc/testsuite/gnat.dg/elab3_pkg.adb new file mode 100644 index 0000000..76616d0 --- /dev/null +++ b/gcc/testsuite/gnat.dg/elab3_pkg.adb @@ -0,0 +1,11 @@ +package body Elab3_Pkg is + procedure Elaborator is + begin + Proc; + end Elaborator; + +begin + if Elaborate then + Elaborator; + end if; +end Elab3_Pkg; diff --git a/gcc/testsuite/gnat.dg/elab3_pkg.ads b/gcc/testsuite/gnat.dg/elab3_pkg.ads new file mode 100644 index 0000000..b4abf3a --- /dev/null +++ b/gcc/testsuite/gnat.dg/elab3_pkg.ads @@ -0,0 +1,7 @@ +generic + Elaborate : Boolean := True; + with procedure Proc; + +package Elab3_Pkg is + procedure Elaborator; +end Elab3_Pkg; diff --git a/gcc/testsuite/gnat.dg/finalized.adb b/gcc/testsuite/gnat.dg/finalized.adb index 36400d5..ebbe474 100644 --- a/gcc/testsuite/gnat.dg/finalized.adb +++ b/gcc/testsuite/gnat.dg/finalized.adb @@ -1,5 +1,8 @@ -- { dg-do compile } +pragma Warnings + (Off, "anonymous access-to-controlled object will be finalized when its enclosing unit goes out of scope"); + with Ada.Finalization; use Ada.Finalization; procedure finalized is type Rec is new Controlled with null record; -- 2.7.4