diff options
| author | Pierre-Marie de Rodat <pmderodat@gcc.gnu.org> | 2017-11-08 15:17:43 +0000 |
|---|---|---|
| committer | Pierre-Marie de Rodat <pmderodat@gcc.gnu.org> | 2017-11-08 15:17:43 +0000 |
| commit | 7cc7f3aa68b852b217c511e7d841458b0bdd532a (patch) | |
| tree | 56f546624848f4160ac2976a6355c5bcedf0f61c | |
| parent | daf82dd806519e567ca6420b5e1c04ec5b732615 (diff) | |
| download | gcc-7cc7f3aa68b852b217c511e7d841458b0bdd532a.zip gcc-7cc7f3aa68b852b217c511e7d841458b0bdd532a.tar.gz gcc-7cc7f3aa68b852b217c511e7d841458b0bdd532a.tar.bz2 | |
sem_disp.adb (Is_Inherited_Public_Operation): Extend the functionality of this routine to handle multiple levels of derivations.
gcc/ada/
2017-11-08 Javier Miranda <miranda@adacore.com>
* sem_disp.adb (Is_Inherited_Public_Operation): Extend the
functionality of this routine to handle multiple levels of derivations.
2017-11-08 Hristian Kirtchev <kirtchev@adacore.com>
* 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 <trojanek@adacore.com>
* 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 <kirtchev@adacore.com>
* 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 <miranda@adacore.com>
* 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.
From-SVN: r254532
| -rw-r--r-- | gcc/ada/ChangeLog | 46 | ||||
| -rw-r--r-- | gcc/ada/einfo.adb | 23 | ||||
| -rw-r--r-- | gcc/ada/einfo.ads | 15 | ||||
| -rw-r--r-- | gcc/ada/exp_ch4.adb | 4 | ||||
| -rw-r--r-- | gcc/ada/exp_intr.adb | 3 | ||||
| -rw-r--r-- | gcc/ada/gcc-interface/Make-lang.in | 2 | ||||
| -rw-r--r-- | gcc/ada/get_spark_xrefs.adb | 493 | ||||
| -rw-r--r-- | gcc/ada/get_spark_xrefs.ads | 60 | ||||
| -rw-r--r-- | gcc/ada/lib-writ.adb | 1 | ||||
| -rw-r--r-- | gcc/ada/lib-xref-spark_specific.adb | 21 | ||||
| -rw-r--r-- | gcc/ada/lib-xref.adb | 1 | ||||
| -rw-r--r-- | gcc/ada/lib-xref.ads | 9 | ||||
| -rw-r--r-- | gcc/ada/put_spark_xrefs.adb | 194 | ||||
| -rw-r--r-- | gcc/ada/put_spark_xrefs.ads | 62 | ||||
| -rw-r--r-- | gcc/ada/sem_disp.adb | 12 | ||||
| -rw-r--r-- | gcc/ada/sem_elab.adb | 222 | ||||
| -rw-r--r-- | gcc/ada/spark_xrefs.adb | 55 | ||||
| -rw-r--r-- | gcc/ada/spark_xrefs.ads | 166 | ||||
| -rw-r--r-- | gcc/ada/spark_xrefs_test.adb | 321 | ||||
| -rw-r--r-- | gcc/testsuite/ChangeLog | 6 | ||||
| -rw-r--r-- | gcc/testsuite/gnat.dg/overriding_ops2.adb | 8 | ||||
| -rw-r--r-- | gcc/testsuite/gnat.dg/overriding_ops2.ads | 12 | ||||
| -rw-r--r-- | gcc/testsuite/gnat.dg/overriding_ops2_pkg-high.ads | 5 | ||||
| -rw-r--r-- | gcc/testsuite/gnat.dg/overriding_ops2_pkg.ads | 9 |
24 files changed, 311 insertions, 1439 deletions
diff --git a/gcc/ada/ChangeLog b/gcc/ada/ChangeLog index 10ab49e..8826c77 100644 --- a/gcc/ada/ChangeLog +++ b/gcc/ada/ChangeLog @@ -1,3 +1,49 @@ +2017-11-08 Javier Miranda <miranda@adacore.com> + + * sem_disp.adb (Is_Inherited_Public_Operation): Extend the + functionality of this routine to handle multiple levels of derivations. + +2017-11-08 Hristian Kirtchev <kirtchev@adacore.com> + + * 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 <trojanek@adacore.com> + + * 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 <kirtchev@adacore.com> + + * 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. + 2017-11-08 Hristian Kirtchev <kirtchev@adacore.com> * exp_ch3.adb (Expand_N_Object_Declaration): Save and restore relevant diff --git a/gcc/ada/einfo.adb b/gcc/ada/einfo.adb index 01d64f3..94e3261 100644 --- a/gcc/ada/einfo.adb +++ b/gcc/ada/einfo.adb @@ -273,6 +273,7 @@ package body Einfo is -- Entry_Max_Queue_Lengths_Array Node35 -- Import_Pragma Node35 + -- Nested_Scenarios Elist36 -- Validated_Object Node36 -- Class_Wide_Clone Node38 @@ -2867,6 +2868,14 @@ package body Einfo is return Flag22 (Id); end Needs_No_Actuals; + function Nested_Scenarios (Id : E) return L is + begin + pragma Assert (Ekind_In (Id, E_Function, + E_Procedure, + E_Subprogram_Body)); + return Elist36 (Id); + end Nested_Scenarios; + function Never_Set_In_Source (Id : E) return B is begin return Flag115 (Id); @@ -6071,6 +6080,14 @@ package body Einfo is Set_Flag22 (Id, V); end Set_Needs_No_Actuals; + procedure Set_Nested_Scenarios (Id : E; V : L) is + begin + pragma Assert (Ekind_In (Id, E_Function, + E_Procedure, + E_Subprogram_Body)); + Set_Elist36 (Id, V); + end Set_Nested_Scenarios; + procedure Set_Never_Set_In_Source (Id : E; V : B := True) is begin Set_Flag115 (Id, V); @@ -11118,6 +11135,12 @@ package body Einfo is procedure Write_Field36_Name (Id : Entity_Id) is begin case Ekind (Id) is + when E_Function + | E_Procedure + | E_Subprogram_Body + => + Write_Str ("Nested_Scenarios"); + when E_Variable => Write_Str ("Validated_Object"); diff --git a/gcc/ada/einfo.ads b/gcc/ada/einfo.ads index bfe14fc..7bcf3f9 100644 --- a/gcc/ada/einfo.ads +++ b/gcc/ada/einfo.ads @@ -3531,6 +3531,14 @@ package Einfo is -- interpreted as an indexing of the result of the call. It is also -- used to resolve various cases of entry calls. +-- Nested_Scenarios (Elist36) +-- Present in [stand alone] subprogram bodies. The list contains all +-- nested scenarios (see the terminology in Sem_Elab) which appear within +-- the declarations, statements, and exception handlers of the subprogram +-- body. The list improves the performance of the ABE Processing phase by +-- avoiding a full tree traversal when the same subprogram body is part +-- of several distinct paths in the elaboration graph. + -- Never_Set_In_Source (Flag115) -- Defined in all entities, but can be set only for variables and -- parameters. This flag is set if the object is never assigned a value @@ -6076,6 +6084,7 @@ package Einfo is -- Linker_Section_Pragma (Node33) -- Contract (Node34) -- Import_Pragma (Node35) (non-generic case only) + -- Nested_Scenarios (Elist36) -- Class_Wide_Clone (Node38) -- Protected_Subprogram (Node39) (non-generic case only) -- SPARK_Pragma (Node40) @@ -6398,6 +6407,7 @@ package Einfo is -- Linker_Section_Pragma (Node33) -- Contract (Node34) -- Import_Pragma (Node35) (non-generic case only) + -- Nested_Scenarios (Elist36) -- Class_Wide_Clone (Node38) -- Protected_Subprogram (Node39) (non-generic case only) -- SPARK_Pragma (Node40) @@ -6592,6 +6602,7 @@ package Einfo is -- Extra_Formals (Node28) -- Anonymous_Masters (Elist29) -- Contract (Node34) + -- Nested_Scenarios (Elist36) -- SPARK_Pragma (Node40) -- Contains_Ignored_Ghost_Code (Flag279) -- SPARK_Pragma_Inherited (Flag265) @@ -7308,6 +7319,7 @@ package Einfo is function Must_Have_Preelab_Init (Id : E) return B; function Needs_Debug_Info (Id : E) return B; function Needs_No_Actuals (Id : E) return B; + function Nested_Scenarios (Id : E) return L; function Never_Set_In_Source (Id : E) return B; function Next_Inlined_Subprogram (Id : E) return E; function No_Dynamic_Predicate_On_Actual (Id : E) return B; @@ -8005,6 +8017,7 @@ package Einfo is procedure Set_Must_Have_Preelab_Init (Id : E; V : B := True); procedure Set_Needs_Debug_Info (Id : E; V : B := True); procedure Set_Needs_No_Actuals (Id : E; V : B := True); + procedure Set_Nested_Scenarios (Id : E; V : L); procedure Set_Never_Set_In_Source (Id : E; V : B := True); procedure Set_Next_Inlined_Subprogram (Id : E; V : E); procedure Set_No_Dynamic_Predicate_On_Actual (Id : E; V : B := True); @@ -8857,6 +8870,7 @@ package Einfo is pragma Inline (Must_Have_Preelab_Init); pragma Inline (Needs_Debug_Info); pragma Inline (Needs_No_Actuals); + pragma Inline (Nested_Scenarios); pragma Inline (Never_Set_In_Source); pragma Inline (Next_Index); pragma Inline (Next_Inlined_Subprogram); @@ -9343,6 +9357,7 @@ package Einfo is pragma Inline (Set_Must_Have_Preelab_Init); pragma Inline (Set_Needs_Debug_Info); pragma Inline (Set_Needs_No_Actuals); + pragma Inline (Set_Nested_Scenarios); pragma Inline (Set_Never_Set_In_Source); pragma Inline (Set_Next_Inlined_Subprogram); pragma Inline (Set_No_Dynamic_Predicate_On_Actual); diff --git a/gcc/ada/exp_ch4.adb b/gcc/ada/exp_ch4.adb index abf6d63..0ef9979 100644 --- a/gcc/ada/exp_ch4.adb +++ b/gcc/ada/exp_ch4.adb @@ -630,7 +630,9 @@ package body Exp_Ch4 is -- [Deep_]Finalize (Obj_Ref.all); - if Needs_Finalization (DesigT) then + if Needs_Finalization (DesigT) + and then not No_Heap_Finalization (PtrT) + then Fin_Call := Make_Final_Call (Obj_Ref => diff --git a/gcc/ada/exp_intr.adb b/gcc/ada/exp_intr.adb index 6de8952..bca7301 100644 --- a/gcc/ada/exp_intr.adb +++ b/gcc/ada/exp_intr.adb @@ -924,7 +924,8 @@ package body Exp_Intr is Arg : constant Node_Id := First_Actual (N); Loc : constant Source_Ptr := Sloc (N); Typ : constant Entity_Id := Etype (Arg); - Desig_Typ : constant Entity_Id := Designated_Type (Typ); + Desig_Typ : constant Entity_Id := + Available_View (Designated_Type (Typ)); Needs_Fin : constant Boolean := Needs_Finalization (Desig_Typ); Root_Typ : constant Entity_Id := Underlying_Type (Root_Type (Typ)); Pool : constant Entity_Id := Associated_Storage_Pool (Root_Typ); diff --git a/gcc/ada/gcc-interface/Make-lang.in b/gcc/ada/gcc-interface/Make-lang.in index 9c7b6e1..d51d397 100644 --- a/gcc/ada/gcc-interface/Make-lang.in +++ b/gcc/ada/gcc-interface/Make-lang.in @@ -322,7 +322,6 @@ GNAT_ADA_OBJS = \ ada/libgnat/g-spchge.o \ ada/libgnat/g-speche.o \ ada/libgnat/g-u3spch.o \ - ada/get_spark_xrefs.o \ ada/get_targ.o \ ada/ghost.o \ ada/libgnat/gnat.o \ @@ -352,7 +351,6 @@ GNAT_ADA_OBJS = \ ada/par_sco.o \ ada/prep.o \ ada/prepcomp.o \ - ada/put_spark_xrefs.o \ ada/put_scos.o \ ada/repinfo.o \ ada/restrict.o \ diff --git a/gcc/ada/get_spark_xrefs.adb b/gcc/ada/get_spark_xrefs.adb deleted file mode 100644 index 9b82d5b..0000000 --- a/gcc/ada/get_spark_xrefs.adb +++ /dev/null @@ -1,493 +0,0 @@ ------------------------------------------------------------------------------- --- -- --- GNAT COMPILER COMPONENTS -- --- -- --- G E T _ S P A R K _ X R E F S -- --- -- --- B o d y -- --- -- --- Copyright (C) 2011-2016, Free Software Foundation, Inc. -- --- -- --- GNAT is free software; you can redistribute it and/or modify it under -- --- terms of the GNU General Public License as published by the Free Soft- -- --- ware Foundation; either version 3, or (at your option) any later ver- -- --- sion. GNAT is distributed in the hope that it will be useful, but WITH- -- --- OUT ANY WARRANTY; without even the implied warranty of MERCHANTABILITY -- --- or FITNESS FOR A PARTICULAR PURPOSE. See the GNU General Public License -- --- for more details. You should have received a copy of the GNU General -- --- Public License distributed with GNAT; see file COPYING3. If not, go to -- --- http://www.gnu.org/licenses for a complete copy of the license. -- --- -- --- GNAT was originally developed by the GNAT team at New York University. -- --- Extensive contributions were provided by Ada Core Technologies Inc. -- --- -- ------------------------------------------------------------------------------- - -with SPARK_Xrefs; use SPARK_Xrefs; -with Types; use Types; - -with Ada.IO_Exceptions; use Ada.IO_Exceptions; - -procedure Get_SPARK_Xrefs is - C : Character; - - use ASCII; - -- For CR/LF - - Cur_File : Nat; - -- Dependency number for the current file - - Cur_Scope : Nat; - -- Scope number for the current scope entity - - Cur_File_Idx : File_Index; - -- Index in SPARK_File_Table of the current file - - Cur_Scope_Idx : Scope_Index; - -- Index in SPARK_Scope_Table of the current scope - - Name_Str : String (1 .. 32768); - Name_Len : Natural := 0; - -- Local string used to store name of File/entity scanned as - -- Name_Str (1 .. Name_Len). - - File_Name : String_Ptr; - Unit_File_Name : String_Ptr; - - ----------------------- - -- Local Subprograms -- - ----------------------- - - function At_EOL return Boolean; - -- Skips any spaces, then checks if at the end of a line. If so, returns - -- True (but does not skip the EOL sequence). If not, then returns False. - - procedure Check (C : Character); - -- Checks that file is positioned at given character, and if so skips past - -- it, If not, raises Data_Error. - - function Get_Nat return Nat; - -- On entry the file is positioned to a digit. On return, the file is - -- positioned past the last digit, and the returned result is the decimal - -- value read. Data_Error is raised for overflow (value greater than - -- Int'Last), or if the initial character is not a digit. - - procedure Get_Name; - -- On entry the file is positioned to a name. On return, the file is - -- positioned past the last character, and the name scanned is returned - -- in Name_Str (1 .. Name_Len). - - procedure Skip_EOL; - -- Called with the current character about to be read being LF or CR. Skips - -- past CR/LF characters until either a non-CR/LF character is found, or - -- the end of file is encountered. - - procedure Skip_Spaces; - -- Skips zero or more spaces at the current position, leaving the file - -- positioned at the first non-blank character (or Types.EOF). - - ------------ - -- At_EOL -- - ------------ - - function At_EOL return Boolean is - begin - Skip_Spaces; - return Nextc = CR or else Nextc = LF; - end At_EOL; - - ----------- - -- Check -- - ----------- - - procedure Check (C : Character) is - begin - if Nextc = C then - Skipc; - else - raise Data_Error; - end if; - end Check; - - ------------- - -- Get_Nat -- - ------------- - - function Get_Nat return Nat is - C : Character := Nextc; - Val : Nat := 0; - - begin - if C not in '0' .. '9' then - raise Data_Error; - end if; - - -- Loop to read digits of integer value - - loop - declare - pragma Unsuppress (Overflow_Check); - begin - Val := Val * 10 + (Character'Pos (C) - Character'Pos ('0')); - end; - - Skipc; - C := Nextc; - - exit when C not in '0' .. '9'; - end loop; - - return Val; - - exception - when Constraint_Error => - raise Data_Error; - end Get_Nat; - - -------------- - -- Get_Name -- - -------------- - - procedure Get_Name is - N : Natural := 0; - - begin - while Nextc > ' ' loop - N := N + 1; - Name_Str (N) := Getc; - end loop; - - Name_Len := N; - end Get_Name; - - -------------- - -- Skip_EOL -- - -------------- - - procedure Skip_EOL is - C : Character; - - begin - loop - Skipc; - C := Nextc; - exit when C /= LF and then C /= CR; - - if C = ' ' then - Skip_Spaces; - C := Nextc; - exit when C /= LF and then C /= CR; - end if; - end loop; - end Skip_EOL; - - ----------------- - -- Skip_Spaces -- - ----------------- - - procedure Skip_Spaces is - begin - while Nextc = ' ' loop - Skipc; - end loop; - end Skip_Spaces; - --- Start of processing for Get_SPARK_Xrefs - -begin - Initialize_SPARK_Tables; - - Cur_File := 0; - Cur_Scope := 0; - Cur_File_Idx := 1; - Cur_Scope_Idx := 0; - - -- Loop through lines of SPARK cross-reference information - - while Nextc = 'F' loop - Skipc; - - C := Getc; - - -- Make sure first line is a File line - - if SPARK_File_Table.Last = 0 and then C /= 'D' then - raise Data_Error; - end if; - - -- Otherwise dispatch on type of line - - case C is - - -- Header entry for scope section - - when 'D' => - - -- Complete previous entry if any - - if SPARK_File_Table.Last /= 0 then - SPARK_File_Table.Table (SPARK_File_Table.Last).To_Scope := - SPARK_Scope_Table.Last; - end if; - - -- Scan out dependency number and file name - - Skip_Spaces; - Cur_File := Get_Nat; - Skip_Spaces; - - Get_Name; - File_Name := new String'(Name_Str (1 .. Name_Len)); - Skip_Spaces; - - -- Scan out unit file name when present (for subunits) - - if Nextc = '-' then - Skipc; - Check ('>'); - Skip_Spaces; - Get_Name; - Unit_File_Name := new String'(Name_Str (1 .. Name_Len)); - - else - Unit_File_Name := null; - end if; - - -- Make new File table entry (will fill in To_Scope later) - - SPARK_File_Table.Append ( - (File_Name => File_Name, - Unit_File_Name => Unit_File_Name, - File_Num => Cur_File, - From_Scope => SPARK_Scope_Table.Last + 1, - To_Scope => 0)); - - -- Initialize counter for scopes - - Cur_Scope := 1; - - -- Scope entry - - when 'S' => - declare - Spec_File : Nat; - Spec_Scope : Nat; - Scope : Nat; - Line : Nat; - Col : Nat; - Typ : Character; - - begin - -- Scan out location - - Skip_Spaces; - Check ('.'); - Scope := Get_Nat; - Check (' '); - Line := Get_Nat; - Typ := Getc; - Col := Get_Nat; - - pragma Assert (Scope = Cur_Scope); - - -- Scan out scope entity name - - Skip_Spaces; - Get_Name; - Skip_Spaces; - - if Nextc = '-' then - Skipc; - Check ('>'); - Skip_Spaces; - Spec_File := Get_Nat; - Check ('.'); - Spec_Scope := Get_Nat; - - else - Spec_File := 0; - Spec_Scope := 0; - end if; - - -- Make new scope table entry (will fill in From_Xref and - -- To_Xref later). Initial range (From_Xref .. To_Xref) is - -- empty for scopes without entities. - - SPARK_Scope_Table.Append ( - (Scope_Entity => Empty, - Scope_Name => new String'(Name_Str (1 .. Name_Len)), - File_Num => Cur_File, - Scope_Num => Cur_Scope, - Spec_File_Num => Spec_File, - Spec_Scope_Num => Spec_Scope, - Line => Line, - Stype => Typ, - Col => Col, - From_Xref => 1, - To_Xref => 0)); - end; - - -- Update counter for scopes - - Cur_Scope := Cur_Scope + 1; - - -- Header entry for cross-ref section - - when 'X' => - - -- Scan out dependency number and file name (ignored) - - Skip_Spaces; - Cur_File := Get_Nat; - Skip_Spaces; - Get_Name; - - -- Update component From_Xref of current file if first reference - -- in this file. - - while SPARK_File_Table.Table (Cur_File_Idx).File_Num /= Cur_File - loop - Cur_File_Idx := Cur_File_Idx + 1; - end loop; - - -- Scan out scope entity number and entity name (ignored) - - Skip_Spaces; - Check ('.'); - Cur_Scope := Get_Nat; - Skip_Spaces; - Get_Name; - - -- Update component To_Xref of previous scope - - if Cur_Scope_Idx /= 0 then - SPARK_Scope_Table.Table (Cur_Scope_Idx).To_Xref := - SPARK_Xref_Table.Last; - end if; - - -- Update component From_Xref of current scope - - Cur_Scope_Idx := SPARK_File_Table.Table (Cur_File_Idx).From_Scope; - - while SPARK_Scope_Table.Table (Cur_Scope_Idx).Scope_Num /= - Cur_Scope - loop - Cur_Scope_Idx := Cur_Scope_Idx + 1; - end loop; - - SPARK_Scope_Table.Table (Cur_Scope_Idx).From_Xref := - SPARK_Xref_Table.Last + 1; - - -- Cross reference entry - - when ' ' => - declare - XR_Entity : String_Ptr; - XR_Entity_Line : Nat; - XR_Entity_Col : Nat; - XR_Entity_Typ : Character; - - XR_File : Nat; - -- Keeps track of the current file (changed by nn|) - - XR_Scope : Nat; - -- Keeps track of the current scope (changed by nn:) - - begin - XR_File := Cur_File; - XR_Scope := Cur_Scope; - - XR_Entity_Line := Get_Nat; - XR_Entity_Typ := Getc; - XR_Entity_Col := Get_Nat; - - Skip_Spaces; - Get_Name; - XR_Entity := new String'(Name_Str (1 .. Name_Len)); - - -- Initialize to scan items on one line - - Skip_Spaces; - - -- Loop through cross-references for this entity - - loop - declare - Line : Nat; - Col : Nat; - N : Nat; - Rtype : Character; - - begin - Skip_Spaces; - - if At_EOL then - Skip_EOL; - exit when Nextc /= '.'; - Skipc; - Skip_Spaces; - end if; - - if Nextc = '.' then - Skipc; - XR_Scope := Get_Nat; - Check (':'); - - else - N := Get_Nat; - - if Nextc = '|' then - XR_File := N; - Skipc; - - else - Line := N; - Rtype := Getc; - Col := Get_Nat; - - pragma Assert - (Rtype = 'r' or else - Rtype = 'c' or else - Rtype = 'm' or else - Rtype = 's'); - - SPARK_Xref_Table.Append ( - (Entity_Name => XR_Entity, - Entity_Line => XR_Entity_Line, - Etype => XR_Entity_Typ, - Entity_Col => XR_Entity_Col, - File_Num => XR_File, - Scope_Num => XR_Scope, - Line => Line, - Rtype => Rtype, - Col => Col)); - end if; - end if; - end; - end loop; - end; - - -- No other SPARK lines are possible - - when others => - raise Data_Error; - end case; - - -- For cross reference lines, the EOL character has been skipped already - - if C /= ' ' then - Skip_EOL; - end if; - end loop; - - -- Here with all Xrefs stored, complete last entries in File/Scope tables - - if SPARK_File_Table.Last /= 0 then - SPARK_File_Table.Table (SPARK_File_Table.Last).To_Scope := - SPARK_Scope_Table.Last; - end if; - - if Cur_Scope_Idx /= 0 then - SPARK_Scope_Table.Table (Cur_Scope_Idx).To_Xref := SPARK_Xref_Table.Last; - end if; -end Get_SPARK_Xrefs; diff --git a/gcc/ada/get_spark_xrefs.ads b/gcc/ada/get_spark_xrefs.ads deleted file mode 100644 index 22af7ed..0000000 --- a/gcc/ada/get_spark_xrefs.ads +++ /dev/null @@ -1,60 +0,0 @@ ------------------------------------------------------------------------------- --- -- --- GNAT COMPILER COMPONENTS -- --- -- --- G E T _ S P A R K _ X R E F S -- --- -- --- S p e c -- --- -- --- Copyright (C) 2011-2013, Free Software Foundation, Inc. -- --- -- --- GNAT is free software; you can redistribute it and/or modify it under -- --- terms of the GNU General Public License as published by the Free Soft- -- --- ware Foundation; either version 3, or (at your option) any later ver- -- --- sion. GNAT is distributed in the hope that it will be useful, but WITH- -- --- OUT ANY WARRANTY; without even the implied warranty of MERCHANTABILITY -- --- or FITNESS FOR A PARTICULAR PURPOSE. See the GNU General Public License -- --- for more details. You should have received a copy of the GNU General -- --- Public License distributed with GNAT; see file COPYING3. If not, go to -- --- http://www.gnu.org/licenses for a complete copy of the license. -- --- -- --- GNAT was originally developed by the GNAT team at New York University. -- --- Extensive contributions were provided by Ada Core Technologies Inc. -- --- -- ------------------------------------------------------------------------------- - --- This package contains the function used to read SPARK cross-reference --- information from an ALI file and populate the tables defined in package --- SPARK_Xrefs with the result. - -generic - -- These subprograms provide access to the ALI file. Locating, opening and - -- providing access to the ALI file is the callers' responsibility. - - with function Getc return Character is <>; - -- Get next character, positioning the ALI file ready to read the following - -- character (equivalent to calling Nextc, then Skipc). If the end of file - -- is encountered, the value Types.EOF is returned. - - with function Nextc return Character is <>; - -- Look at the next character, and return it, leaving the position of the - -- file unchanged, so that a subsequent call to Getc or Nextc will return - -- this same character. If the file is positioned at the end of file, then - -- Types.EOF is returned. - - with procedure Skipc is <>; - -- Skip past the current character (which typically was read with Nextc), - -- and position to the next character, which will be returned by the next - -- call to Getc or Nextc. - -procedure Get_SPARK_Xrefs; --- Load SPARK cross-reference information from ALI file text format into --- internal SPARK tables (SPARK_Xrefs.SPARK_Xref_Table, --- SPARK_Xrefs.SPARK_Scope_Table and SPARK_Xrefs.SPARK_File_Table). On entry --- the input file is positioned to the initial 'F' of the first SPARK specific --- line in the ALI file. On return, the file is positioned either to the end --- of file, or to the first character of the line following the SPARK specific --- information (which will never start with an 'F'). --- --- If a format error is detected in the input, then an exception is raised --- (Ada.IO_Exceptions.Data_Error), with the file positioned to the error. diff --git a/gcc/ada/lib-writ.adb b/gcc/ada/lib-writ.adb index 47109b4..19e05d4 100644 --- a/gcc/ada/lib-writ.adb +++ b/gcc/ada/lib-writ.adb @@ -1572,7 +1572,6 @@ package body Lib.Writ is if Opt.Xref_Active and then GNATprove_Mode then SPARK_Specific.Collect_SPARK_Xrefs (Sdep_Table => Sdep_Table, Num_Sdep => Num_Sdep); - SPARK_Specific.Output_SPARK_Xrefs; end if; -- Output final blank line and we are done. This final blank line is diff --git a/gcc/ada/lib-xref-spark_specific.adb b/gcc/ada/lib-xref-spark_specific.adb index 4d22174..c3bad8d 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; diff --git a/gcc/ada/lib-xref.adb b/gcc/ada/lib-xref.adb index eb6ac0a..513d592 100644 --- a/gcc/ada/lib-xref.adb +++ b/gcc/ada/lib-xref.adb @@ -27,6 +27,7 @@ with Atree; use Atree; with Csets; use Csets; with Elists; use Elists; with Errout; use Errout; +with Lib.Util; use Lib.Util; with Nlists; use Nlists; with Opt; use Opt; with Restrict; use Restrict; diff --git a/gcc/ada/lib-xref.ads b/gcc/ada/lib-xref.ads index d421639..f827eb4 100644 --- a/gcc/ada/lib-xref.ads +++ b/gcc/ada/lib-xref.ads @@ -26,9 +26,7 @@ -- This package contains for collecting and outputting cross-reference -- information. -with Einfo; use Einfo; -with Lib.Util; use Lib.Util; -with Put_SPARK_Xrefs; +with Einfo; use Einfo; package Lib.Xref is @@ -647,11 +645,6 @@ package Lib.Xref is -- files and scopes) and from shared cross-references. Fill in the -- tables in library package called SPARK_Xrefs. - procedure Output_SPARK_Xrefs is new Put_SPARK_Xrefs; - -- Output SPARK cross-reference information to the ALI files, based on - -- the information collected in the tables in library package called - -- SPARK_Xrefs, and using routines in Lib.Util. - generic with procedure Process (N : Node_Id) is <>; procedure Traverse_Compilation_Unit diff --git a/gcc/ada/put_spark_xrefs.adb b/gcc/ada/put_spark_xrefs.adb deleted file mode 100644 index a65fa8a..0000000 --- a/gcc/ada/put_spark_xrefs.adb +++ /dev/null @@ -1,194 +0,0 @@ ------------------------------------------------------------------------------- --- -- --- GNAT COMPILER COMPONENTS -- --- -- --- P U T _ S P A R K _ X R E F S -- --- -- --- B o d y -- --- -- --- Copyright (C) 2011-2016, Free Software Foundation, Inc. -- --- -- --- GNAT is free software; you can redistribute it and/or modify it under -- --- terms of the GNU General Public License as published by the Free Soft- -- --- ware Foundation; either version 3, or (at your option) any later ver- -- --- sion. GNAT is distributed in the hope that it will be useful, but WITH- -- --- OUT ANY WARRANTY; without even the implied warranty of MERCHANTABILITY -- --- or FITNESS FOR A PARTICULAR PURPOSE. See the GNU General Public License -- --- for more details. You should have received a copy of the GNU General -- --- Public License distributed with GNAT; see file COPYING3. If not, go to -- --- http://www.gnu.org/licenses for a complete copy of the license. -- --- -- --- GNAT was originally developed by the GNAT team at New York University. -- --- Extensive contributions were provided by Ada Core Technologies Inc. -- --- -- ------------------------------------------------------------------------------- - -with SPARK_Xrefs; use SPARK_Xrefs; - -procedure Put_SPARK_Xrefs is -begin - -- Loop through entries in SPARK_File_Table - - for J in 1 .. SPARK_File_Table.Last loop - declare - F : SPARK_File_Record renames SPARK_File_Table.Table (J); - - begin - Write_Info_Initiate ('F'); - Write_Info_Char ('D'); - Write_Info_Char (' '); - Write_Info_Nat (F.File_Num); - Write_Info_Char (' '); - - Write_Info_Str (F.File_Name.all); - - -- If file is a subunit, print the file name for the unit - - if F.Unit_File_Name /= null then - Write_Info_Str (" -> " & F.Unit_File_Name.all); - end if; - - Write_Info_Terminate; - - -- Loop through scope entries for this file - - for J in F.From_Scope .. F.To_Scope loop - declare - S : SPARK_Scope_Record renames SPARK_Scope_Table.Table (J); - - begin - Write_Info_Initiate ('F'); - Write_Info_Char ('S'); - Write_Info_Char (' '); - Write_Info_Char ('.'); - Write_Info_Nat (S.Scope_Num); - Write_Info_Char (' '); - Write_Info_Nat (S.Line); - Write_Info_Char (S.Stype); - Write_Info_Nat (S.Col); - Write_Info_Char (' '); - - pragma Assert (S.Scope_Name.all /= ""); - - Write_Info_Str (S.Scope_Name.all); - - if S.Spec_File_Num /= 0 then - Write_Info_Str (" -> "); - Write_Info_Nat (S.Spec_File_Num); - Write_Info_Char ('.'); - Write_Info_Nat (S.Spec_Scope_Num); - end if; - - Write_Info_Terminate; - end; - end loop; - end; - end loop; - - -- Loop through entries in SPARK_File_Table - - for J in 1 .. SPARK_File_Table.Last loop - declare - F : SPARK_File_Record renames SPARK_File_Table.Table (J); - File : Nat; - Scope : Nat; - Entity_Line : Nat; - Entity_Col : Nat; - - begin - -- Loop through scope entries for this file - - for K in F.From_Scope .. F.To_Scope loop - Output_One_Scope : declare - S : SPARK_Scope_Record renames SPARK_Scope_Table.Table (K); - - begin - -- Write only non-empty tables - - if S.From_Xref <= S.To_Xref then - - Write_Info_Initiate ('F'); - Write_Info_Char ('X'); - Write_Info_Char (' '); - Write_Info_Nat (F.File_Num); - Write_Info_Char (' '); - - Write_Info_Str (F.File_Name.all); - - Write_Info_Char (' '); - Write_Info_Char ('.'); - Write_Info_Nat (S.Scope_Num); - Write_Info_Char (' '); - - Write_Info_Str (S.Scope_Name.all); - - -- Default value of (0,0) is used for the special __HEAP - -- variable so use another default value. - - Entity_Line := 0; - Entity_Col := 1; - - -- Loop through cross reference entries for this scope - - for X in S.From_Xref .. S.To_Xref loop - - Output_One_Xref : declare - R : SPARK_Xref_Record renames - SPARK_Xref_Table.Table (X); - - begin - if R.Entity_Line /= Entity_Line - or else R.Entity_Col /= Entity_Col - then - Write_Info_Terminate; - - Write_Info_Initiate ('F'); - Write_Info_Char (' '); - Write_Info_Nat (R.Entity_Line); - Write_Info_Char (R.Etype); - Write_Info_Nat (R.Entity_Col); - Write_Info_Char (' '); - - Write_Info_Str (R.Entity_Name.all); - - Entity_Line := R.Entity_Line; - Entity_Col := R.Entity_Col; - File := F.File_Num; - Scope := S.Scope_Num; - end if; - - if Write_Info_Col > 72 then - Write_Info_Terminate; - Write_Info_Initiate ('.'); - end if; - - Write_Info_Char (' '); - - if R.File_Num /= File then - Write_Info_Nat (R.File_Num); - Write_Info_Char ('|'); - File := R.File_Num; - Scope := 0; - end if; - - if R.Scope_Num /= Scope then - Write_Info_Char ('.'); - Write_Info_Nat (R.Scope_Num); - Write_Info_Char (':'); - Scope := R.Scope_Num; - end if; - - Write_Info_Nat (R.Line); - Write_Info_Char (R.Rtype); - Write_Info_Nat (R.Col); - end Output_One_Xref; - - end loop; - - Write_Info_Terminate; - end if; - end Output_One_Scope; - end loop; - end; - end loop; -end Put_SPARK_Xrefs; diff --git a/gcc/ada/put_spark_xrefs.ads b/gcc/ada/put_spark_xrefs.ads deleted file mode 100644 index fa4a4bc..0000000 --- a/gcc/ada/put_spark_xrefs.ads +++ /dev/null @@ -1,62 +0,0 @@ ------------------------------------------------------------------------------- --- -- --- GNAT COMPILER COMPONENTS -- --- -- --- P U T _ S P A R K _ X R E F S -- --- -- --- S p e c -- --- -- --- Copyright (C) 2011-2016, Free Software Foundation, Inc. -- --- -- --- GNAT is free software; you can redistribute it and/or modify it under -- --- terms of the GNU General Public License as published by the Free Soft- -- --- ware Foundation; either version 3, or (at your option) any later ver- -- --- sion. GNAT is distributed in the hope that it will be useful, but WITH- -- --- OUT ANY WARRANTY; without even the implied warranty of MERCHANTABILITY -- --- or FITNESS FOR A PARTICULAR PURPOSE. See the GNU General Public License -- --- for more details. You should have received a copy of the GNU General -- --- Public License distributed with GNAT; see file COPYING3. If not, go to -- --- http://www.gnu.org/licenses for a complete copy of the license. -- --- -- --- GNAT was originally developed by the GNAT team at New York University. -- --- Extensive contributions were provided by Ada Core Technologies Inc. -- --- -- ------------------------------------------------------------------------------- - --- This package contains the function used to read SPARK cross-reference --- information from the internal tables defined in package SPARK_Xrefs, and --- output text information for the ALI file. The interface allows control over --- the destination of the output, so that this routine can also be used for --- debugging purposes. - -with Types; use Types; - -generic - -- The following procedures are used to output text information. The - -- destination of the text information is thus under control of the - -- particular instantiation. In particular, this procedure is used to - -- write output to the ALI file, and also for debugging output. - - with function Write_Info_Col return Positive is <>; - -- Return the column in which the next character will be written - - with procedure Write_Info_Char (C : Character) is <>; - -- Output one character - - with procedure Write_Info_Str (Val : String) is <>; - -- Output string stored in string pointer - - with procedure Write_Info_Initiate (Key : Character) is <>; - -- Initiate write of new line to output file, the parameter is the - -- keyword character for the line. - - with procedure Write_Info_Nat (N : Nat) is <>; - -- Write image of N to output file with no leading or trailing blanks - - with procedure Write_Info_Terminate is <>; - -- Terminate current info line and output lines built in Info_Buffer - -procedure Put_SPARK_Xrefs; --- Read information from SPARK tables (SPARK_Xrefs.SPARK_Xref_Table, --- SPARK_Xrefs.SPARK_Scope_Table and SPARK_Xrefs.SPARK_File_Table) and output --- corresponding information in ALI format using the Write_Info procedures. diff --git a/gcc/ada/sem_disp.adb b/gcc/ada/sem_disp.adb index 974edd3..1e140ee 100644 --- a/gcc/ada/sem_disp.adb +++ b/gcc/ada/sem_disp.adb @@ -2371,11 +2371,19 @@ package body Sem_Disp is ----------------------------------- function Is_Inherited_Public_Operation (Op : Entity_Id) return Boolean is - Prim : constant Entity_Id := Alias (Op); - Scop : constant Entity_Id := Scope (Prim); + Prim : Entity_Id := Op; + Scop : Entity_Id := Prim; Pack_Decl : Node_Id; begin + -- Locate the ultimate non-hidden alias entity + + while Present (Alias (Prim)) and then not Is_Hidden (Alias (Prim)) loop + pragma Assert (Alias (Prim) /= Prim); + Prim := Alias (Prim); + Scop := Scope (Prim); + end loop; + if Comes_From_Source (Prim) and then Ekind (Scop) = E_Package then Pack_Decl := Unit_Declaration_Node (Scop); return Nkind (Pack_Decl) = N_Package_Declaration diff --git a/gcc/ada/sem_elab.adb b/gcc/ada/sem_elab.adb index fb0d825..2fb8289 100644 --- a/gcc/ada/sem_elab.adb +++ b/gcc/ada/sem_elab.adb @@ -26,6 +26,7 @@ with Atree; use Atree; with Debug; use Debug; with Einfo; use Einfo; +with Elists; use Elists; with Errout; use Errout; with Exp_Ch11; use Exp_Ch11; with Exp_Tss; use Exp_Tss; @@ -8502,84 +8503,172 @@ package body Sem_Elab is In_Partial_Fin : Boolean; In_Task_Body : Boolean) is - function Is_Potential_Scenario (Nod : Node_Id) return Traverse_Result; - -- Determine whether arbitrary node Nod denotes a suitable scenario and - -- if so, process it. + procedure Find_And_Process_Nested_Scenarios; + pragma Inline (Find_And_Process_Nested_Scenarios); + -- Examine the declarations and statements of subprogram body N for + -- suitable scenarios. Save each discovered scenario and process it + -- accordingly. + + procedure Process_Nested_Scenarios (Nested : Elist_Id); + pragma Inline (Process_Nested_Scenarios); + -- Invoke Process_Scenario on each individual scenario whith appears in + -- list Nested. + + --------------------------------------- + -- Find_And_Process_Nested_Scenarios -- + --------------------------------------- + + procedure Find_And_Process_Nested_Scenarios is + Body_Id : constant Entity_Id := Defining_Entity (N); + + function Is_Potential_Scenario + (Nod : Node_Id) return Traverse_Result; + -- Determine whether arbitrary node Nod denotes a suitable scenario. + -- If it does, save it in the Nested_Scenarios list of the subprogram + -- body, and process it. + + procedure Save_Scenario (Nod : Node_Id); + pragma Inline (Save_Scenario); + -- Save scenario Nod in the Nested_Scenarios list of the subprogram + -- body. - procedure Traverse_Potential_Scenarios is - new Traverse_Proc (Is_Potential_Scenario); + procedure Traverse_List (List : List_Id); + pragma Inline (Traverse_List); + -- Invoke Traverse_Potential_Scenarios on each node in list List - procedure Traverse_List (List : List_Id); - -- Inspect list List for suitable elaboration scenarios and process them + procedure Traverse_Potential_Scenarios is + new Traverse_Proc (Is_Potential_Scenario); - --------------------------- - -- Is_Potential_Scenario -- - --------------------------- + --------------------------- + -- Is_Potential_Scenario -- + --------------------------- - function Is_Potential_Scenario (Nod : Node_Id) return Traverse_Result is - begin - -- Special cases + function Is_Potential_Scenario + (Nod : Node_Id) return Traverse_Result + is + begin + -- Special cases - -- Skip constructs which do not have elaboration of their own and - -- need to be elaborated by other means such as invocation, task - -- activation, etc. + -- Skip constructs which do not have elaboration of their own and + -- need to be elaborated by other means such as invocation, task + -- activation, etc. - if Is_Non_Library_Level_Encapsulator (Nod) then - return Skip; + if Is_Non_Library_Level_Encapsulator (Nod) then + return Skip; - -- Terminate the traversal of a task body with an accept statement - -- when no entry calls in elaboration are allowed because the task - -- will block at run-time and none of the remaining statements will - -- be executed. + -- Terminate the traversal of a task body with an accept statement + -- when no entry calls in elaboration are allowed because the task + -- will block at run-time and the remaining statements will not be + -- executed. - elsif Nkind_In (Original_Node (Nod), N_Accept_Statement, - N_Selective_Accept) - and then Restriction_Active (No_Entry_Calls_In_Elaboration_Code) - then - return Abandon; + elsif Nkind_In (Original_Node (Nod), N_Accept_Statement, + N_Selective_Accept) + and then Restriction_Active (No_Entry_Calls_In_Elaboration_Code) + then + return Abandon; - -- Certain nodes carry semantic lists which act as repositories until - -- expansion transforms the node and relocates the contents. Examine - -- these lists in case expansion is disabled. + -- Certain nodes carry semantic lists which act as repositories + -- until expansion transforms the node and relocates the contents. + -- Examine these lists in case expansion is disabled. - elsif Nkind_In (Nod, N_And_Then, N_Or_Else) then - Traverse_List (Actions (Nod)); + elsif Nkind_In (Nod, N_And_Then, N_Or_Else) then + Traverse_List (Actions (Nod)); - elsif Nkind_In (Nod, N_Elsif_Part, N_Iteration_Scheme) then - Traverse_List (Condition_Actions (Nod)); + elsif Nkind_In (Nod, N_Elsif_Part, N_Iteration_Scheme) then + Traverse_List (Condition_Actions (Nod)); - elsif Nkind (Nod) = N_If_Expression then - Traverse_List (Then_Actions (Nod)); - Traverse_List (Else_Actions (Nod)); + elsif Nkind (Nod) = N_If_Expression then + Traverse_List (Then_Actions (Nod)); + Traverse_List (Else_Actions (Nod)); - elsif Nkind_In (Nod, N_Component_Association, - N_Iterated_Component_Association) - then - Traverse_List (Loop_Actions (Nod)); + elsif Nkind_In (Nod, N_Component_Association, + N_Iterated_Component_Association) + then + Traverse_List (Loop_Actions (Nod)); - -- General case + -- General case - elsif Is_Suitable_Scenario (Nod) then - Process_Scenario (Nod, In_Partial_Fin, In_Task_Body); - end if; + -- 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 + -- longer need to reexamine the tree. + + elsif Is_Suitable_Scenario (Nod) then + Save_Scenario (Nod); + Process_Scenario (Nod, In_Partial_Fin, In_Task_Body); + end if; - return OK; - end Is_Potential_Scenario; + return OK; + end Is_Potential_Scenario; - ------------------- - -- Traverse_List -- - ------------------- + ------------------- + -- Save_Scenario -- + ------------------- - procedure Traverse_List (List : List_Id) is - Item : Node_Id; + procedure Save_Scenario (Nod : Node_Id) is + Nested : Elist_Id; + + begin + Nested := Nested_Scenarios (Body_Id); + + if No (Nested) then + Nested := New_Elmt_List; + Set_Nested_Scenarios (Body_Id, Nested); + end if; + + Append_Elmt (Nod, Nested); + end Save_Scenario; + + ------------------- + -- Traverse_List -- + ------------------- + + procedure Traverse_List (List : List_Id) is + Item : Node_Id; + + begin + Item := First (List); + while Present (Item) loop + Traverse_Potential_Scenarios (Item); + Next (Item); + end loop; + end Traverse_List; + + -- Start of processing for Find_And_Process_Nested_Scenarios begin - Item := First (List); - while Present (Item) loop - Traverse_Potential_Scenarios (Item); - Next (Item); + -- Examine the declarations for suitable scenarios + + Traverse_List (Declarations (N)); + + -- Examine the handled sequence of statements. This also includes any + -- exceptions handlers. + + Traverse_Potential_Scenarios (Handled_Statement_Sequence (N)); + end Find_And_Process_Nested_Scenarios; + + ------------------------------ + -- Process_Nested_Scenarios -- + ------------------------------ + + procedure Process_Nested_Scenarios (Nested : Elist_Id) is + Nested_Elmt : Elmt_Id; + + begin + Nested_Elmt := First_Elmt (Nested); + while Present (Nested_Elmt) loop + Process_Scenario + (N => Node (Nested_Elmt), + In_Partial_Fin => In_Partial_Fin, + In_Task_Body => In_Task_Body); + + Next_Elmt (Nested_Elmt); end loop; - end Traverse_List; + end Process_Nested_Scenarios; + + -- Local variables + + Nested : Elist_Id; -- Start of processing for Traverse_Body @@ -8605,14 +8694,23 @@ package body Sem_Elab is Visited_Bodies.Set (N, True); end if; - -- Examine the declarations for suitable scenarios + Nested := Nested_Scenarios (Defining_Entity (N)); - Traverse_List (Declarations (N)); + -- The subprogram body was already examined as part of the elaboration + -- 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. - -- Examine the handled sequence of statements. This also includes any - -- exceptions handlers. + if Present (Nested) then + Process_Nested_Scenarios (Nested); - Traverse_Potential_Scenarios (Handled_Statement_Sequence (N)); + -- Otherwise examine the declarations and statements of the subprogram + -- body for suitable scenarios, save and process them accordingly. + + else + Find_And_Process_Nested_Scenarios; + end if; end Traverse_Body; --------------------------------- diff --git a/gcc/ada/spark_xrefs.adb b/gcc/ada/spark_xrefs.adb index 8fab555..ca4e69d 100644 --- a/gcc/ada/spark_xrefs.adb +++ b/gcc/ada/spark_xrefs.adb @@ -6,7 +6,7 @@ -- -- -- B o d y -- -- -- --- Copyright (C) 2011-2016, Free Software Foundation, Inc. -- +-- Copyright (C) 2011-2017, Free Software Foundation, Inc. -- -- -- -- GNAT is free software; you can redistribute it and/or modify it under -- -- terms of the GNU General Public License as published by the Free Soft- -- @@ -23,8 +23,7 @@ -- -- ------------------------------------------------------------------------------ -with Output; use Output; -with Put_SPARK_Xrefs; +with Output; use Output; package body SPARK_Xrefs is @@ -153,54 +152,4 @@ package body SPARK_Xrefs is SPARK_Xref_Table.Init; end Initialize_SPARK_Tables; - ------------ - -- pspark -- - ------------ - - procedure pspark is - - procedure Write_Info_Char (C : Character) renames Write_Char; - -- Write one character - - procedure Write_Info_Str (Val : String) renames Write_Str; - -- Write string - - function Write_Info_Col return Positive; - -- Return next column for writing - - procedure Write_Info_Initiate (Key : Character) renames Write_Char; - -- Start new one and write one character; - - procedure Write_Info_Nat (N : Nat); - -- Write value of N - - procedure Write_Info_Terminate renames Write_Eol; - -- Terminate current line - - -------------------- - -- Write_Info_Col -- - -------------------- - - function Write_Info_Col return Positive is - begin - return Positive (Column); - end Write_Info_Col; - - -------------------- - -- Write_Info_Nat -- - -------------------- - - procedure Write_Info_Nat (N : Nat) is - begin - Write_Int (N); - end Write_Info_Nat; - - procedure Debug_Put_SPARK_Xrefs is new Put_SPARK_Xrefs; - - -- Start of processing for pspark - - begin - Debug_Put_SPARK_Xrefs; - end pspark; - end SPARK_Xrefs; diff --git a/gcc/ada/spark_xrefs.ads b/gcc/ada/spark_xrefs.ads index fd5b76d..7fb2939 100644 --- a/gcc/ada/spark_xrefs.ads +++ b/gcc/ada/spark_xrefs.ads @@ -25,173 +25,21 @@ -- 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 before writing it to the ALI --- file, and by Get_SPARK_Xrefs/Put_SPARK_Xrefs to read/write the textual --- representation that is stored in the ALI file. +-- SPARK-specific cross-reference information. with Table; -with Types; use Types; +with Types; use Types; package SPARK_Xrefs is - -- SPARK cross-reference information can exist in one of two forms. In - -- the ALI file, it is represented using a text format that is described - -- in this specification. Internally it is stored using three tables: - -- SPARK_Xref_Table, SPARK_Scope_Table and SPARK_File_Table, which are - -- also defined in this unit. + -- 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. - -- Get_SPARK_Xrefs reads the text lines in ALI format and populates the - -- internal tables with corresponding information. - - -- Put_SPARK_Xrefs reads the internal tables and generates text lines in - -- the ALI format. - - ---------------------------- - -- SPARK Xrefs ALI Format -- - ---------------------------- - - -- SPARK cross-reference information is generated on a unit-by-unit basis - -- in the ALI file, using lines that start with the identifying character F - -- ("Formal"). These lines are generated if GNATprove_Mode is True. - - -- The SPARK cross-reference information comes after the shared - -- cross-reference information, so it can be ignored by tools like - -- gnatbind, gnatmake, etc. - - -- ------------------- - -- -- Scope Section -- - -- ------------------- - - -- A first section defines the scopes in which entities are defined and - -- referenced. A scope is a package/subprogram/protected_type/task_type - -- declaration/body. Note that a package declaration and body define two - -- different scopes. Similarly, a subprogram, protected type and task type - -- declaration and body, when both present, define two different scopes. - - -- FD dependency-number filename (-> unit-filename)? - - -- This header precedes scope information for the unit identified by - -- dependency number and file name. The dependency number is the index - -- into the generated D lines and is ones-origin (e.g. 2 = reference to - -- second generated D line). - - -- The list of FD lines should match the list of D lines defined in the - -- ALI file, in the same order. - - -- Note that the filename here will reflect the original name if a - -- Source_Reference pragma was encountered (since all line number - -- references will be with respect to the original file). - - -- Note: the filename is redundant in that it could be deduced from the - -- corresponding D line, but it is convenient at least for human - -- reading of the SPARK cross-reference information, and means that - -- the SPARK cross-reference information can stand on its own without - -- needing other parts of the ALI file. - - -- The optional unit filename is given only for subunits. - - -- FS . scope line type col entity (-> spec-file . spec-scope)? - - -- (The ? mark stands for an optional entry in the syntax) - - -- scope is the ones-origin scope number for the current file (e.g. 2 = - -- reference to the second FS line in this FD block). - - -- line is the line number of the scope entity. The name of the entity - -- starts in column col. Columns are numbered from one, and if - -- horizontal tab characters are present, the column number is computed - -- assuming standard 1,9,17,.. tab stops. For example, if the entity is - -- the first token on the line, and is preceded by space-HT-space, then - -- the column would be column 10. - - -- type is a single letter identifying the type of the entity, using - -- the same code as in cross-references: - - -- K = package (k = generic package) - -- V = function (v = generic function) - -- U = procedure (u = generic procedure) - -- Y = entry - - -- col is the column number of the scope entity - - -- entity is the name of the scope entity, with casing in the canonical - -- casing for the source file where it is defined. - - -- spec-file and spec-scope are respectively the file and scope for the - -- spec corresponding to the current body scope, when they differ. - - -- ------------------ - -- -- Xref Section -- - -- ------------------ - - -- A second section defines cross-references useful for computing global - -- variables read/written in each subprogram/package/protected_type/ - -- task_type. - - -- FX dependency-number filename . entity-number entity - - -- dependency-number and filename identify a file in FD lines - - -- entity-number and entity identify a scope in FS lines - -- for the previously identified file. - - -- (filename and entity are just a textual representations of - -- dependency-number and entity-number) - - -- F line typ col entity ref* - - -- line is the line number of the referenced entity - - -- typ is the type of the referenced entity, using a code similar to - -- the one used for cross-references: - - -- > = IN parameter - -- < = OUT parameter - -- = = IN OUT parameter - -- * = all other cases - - -- col is the column number of the referenced entity - - -- entity is the name of the referenced entity as written in the source - -- file where it is defined. - - -- There may be zero or more ref entries on each line - - -- (file |)? ((. scope :)? line type col)* - - -- file is the dependency number of the file with the reference. It and - -- the following vertical bar are omitted if the file is the same as - -- the previous ref, and the refs for the current file are first (and - -- do not need a bar). - - -- scope is the scope number of the scope with the reference. It and - -- the following colon are omitted if the scope is the same as the - -- previous ref, and the refs for the current scope are first (and do - -- not need a colon). - - -- line is the line number of the reference - - -- col is the column number of the reference - - -- type is one of the following, using the same code as in - -- cross-references: - - -- m = modification - -- r = reference - -- c = reference to constant object - -- s = subprogram reference in a static call - - -- Special entries for reads and writes to memory reference a special - -- variable called "__HEAP". These special entries are present in every - -- scope where reads and writes to memory are present. Line and column for - -- this special variable are always 0. - - -- Examples: ??? add examples here - -- ------------------------------- -- -- Generated Globals Section -- -- ------------------------------- @@ -389,8 +237,4 @@ package SPARK_Xrefs is -- Debug routine to dump internal SPARK cross-reference tables. This is a -- raw format dump showing exactly what the tables contain. - procedure pspark; - -- Debugging procedure to output contents of SPARK cross-reference binary - -- tables in the format in which they appear in an ALI file. - end SPARK_Xrefs; diff --git a/gcc/ada/spark_xrefs_test.adb b/gcc/ada/spark_xrefs_test.adb deleted file mode 100644 index 6ad4de2..0000000 --- a/gcc/ada/spark_xrefs_test.adb +++ /dev/null @@ -1,321 +0,0 @@ ------------------------------------------------------------------------------- --- -- --- GNAT SYSTEM UTILITIES -- --- -- --- S P A R K _ X R E F S _ T E S T -- --- -- --- B o d y -- --- -- --- Copyright (C) 2011-2013, Free Software Foundation, Inc. -- --- -- --- GNAT is free software; you can redistribute it and/or modify it under -- --- terms of the GNU General Public License as published by the Free Soft- -- --- ware Foundation; either version 3, or (at your option) any later ver- -- --- sion. GNAT is distributed in the hope that it will be useful, but WITH- -- --- OUT ANY WARRANTY; without even the implied warranty of MERCHANTABILITY -- --- or FITNESS FOR A PARTICULAR PURPOSE. See the GNU General Public License -- --- for more details. You should have received a copy of the GNU General -- --- Public License distributed with GNAT; see file COPYING3. If not, go to -- --- http://www.gnu.org/licenses for a complete copy of the license. -- --- -- --- GNAT was originally developed by the GNAT team at New York University. -- --- Extensive contributions were provided by Ada Core Technologies Inc. -- --- -- ------------------------------------------------------------------------------- - --- This utility program is used to test proper operation of the --- Get_SPARK_Xrefs and Put_SPARK_Xrefs units. To run it, compile any source --- file with switch -gnatd.E or -gnatd.F to get an ALI file file.ALI --- containing SPARK information. Then run this utility using: - --- spark_xrefs_test file.ali - --- This test will read the SPARK cross-reference information from the ALI --- file, and use Get_SPARK_Xrefs to store this in binary form in the internal --- tables in SPARK_Xrefs. Then Put_SPARK_Xrefs is used to write the --- information from these tables back into text form. This output is compared --- with the original SPARK cross-reference information in the ALI file and the --- two should be identical. If not an error message is output. - -with Get_SPARK_Xrefs; -with Put_SPARK_Xrefs; - -with SPARK_Xrefs; use SPARK_Xrefs; -with Types; use Types; - -with Ada.Command_Line; use Ada.Command_Line; -with Ada.Streams; use Ada.Streams; -with Ada.Streams.Stream_IO; use Ada.Streams.Stream_IO; -with Ada.Text_IO; - -with GNAT.OS_Lib; use GNAT.OS_Lib; - -procedure SPARK_Xrefs_Test is - Infile : File_Type; - Name1 : String_Access; - Outfile_1 : File_Type; - Name2 : String_Access; - Outfile_2 : File_Type; - C : Character; - - Stop : exception; - -- Terminate execution - - Diff_Exec : constant String_Access := Locate_Exec_On_Path ("diff"); - Diff_Result : Integer; - - use ASCII; - -begin - if Argument_Count /= 1 then - Ada.Text_IO.Put_Line ("Usage: spark_xrefs_test FILE.ali"); - raise Stop; - end if; - - Name1 := new String'(Argument (1) & ".1"); - Name2 := new String'(Argument (1) & ".2"); - - Open (Infile, In_File, Argument (1)); - Create (Outfile_1, Out_File, Name1.all); - Create (Outfile_2, Out_File, Name2.all); - - -- Read input file till we get to first 'F' line - - Process : declare - Output_Col : Positive := 1; - - function Get_Char (F : File_Type) return Character; - -- Read one character from specified file - - procedure Put_Char (F : File_Type; C : Character); - -- Write one character to specified file - - function Get_Output_Col return Positive; - -- Return current column in output file, where each line starts at - -- column 1 and terminate with LF, and HT is at columns 1, 9, etc. - -- All output is supposed to be carried through Put_Char. - - -------------- - -- Get_Char -- - -------------- - - function Get_Char (F : File_Type) return Character is - Item : Stream_Element_Array (1 .. 1); - Last : Stream_Element_Offset; - - begin - Read (F, Item, Last); - - if Last /= 1 then - return Types.EOF; - else - return Character'Val (Item (1)); - end if; - end Get_Char; - - -------------------- - -- Get_Output_Col -- - -------------------- - - function Get_Output_Col return Positive is - begin - return Output_Col; - end Get_Output_Col; - - -------------- - -- Put_Char -- - -------------- - - procedure Put_Char (F : File_Type; C : Character) is - Item : Stream_Element_Array (1 .. 1); - - begin - if C /= CR and then C /= EOF then - if C = LF then - Output_Col := 1; - elsif C = HT then - Output_Col := ((Output_Col + 6) / 8) * 8 + 1; - else - Output_Col := Output_Col + 1; - end if; - - Item (1) := Character'Pos (C); - Write (F, Item); - end if; - end Put_Char; - - -- Subprograms used by Get_SPARK_Xrefs (these also copy the output to - -- Outfile_1 for later comparison with the output generated by - -- Put_SPARK_Xrefs). - - function Getc return Character; - function Nextc return Character; - procedure Skipc; - - ---------- - -- Getc -- - ---------- - - function Getc return Character is - C : Character; - begin - C := Get_Char (Infile); - Put_Char (Outfile_1, C); - return C; - end Getc; - - ----------- - -- Nextc -- - ----------- - - function Nextc return Character is - C : Character; - - begin - C := Get_Char (Infile); - - if C /= EOF then - Set_Index (Infile, Index (Infile) - 1); - end if; - - return C; - end Nextc; - - ----------- - -- Skipc -- - ----------- - - procedure Skipc is - C : Character; - pragma Unreferenced (C); - begin - C := Getc; - end Skipc; - - -- Subprograms used by Put_SPARK_Xrefs, which write information to - -- Outfile_2. - - function Write_Info_Col return Positive; - procedure Write_Info_Char (C : Character); - procedure Write_Info_Initiate (Key : Character); - procedure Write_Info_Nat (N : Nat); - procedure Write_Info_Terminate; - - -------------------- - -- Write_Info_Col -- - -------------------- - - function Write_Info_Col return Positive is - begin - return Get_Output_Col; - end Write_Info_Col; - - --------------------- - -- Write_Info_Char -- - --------------------- - - procedure Write_Info_Char (C : Character) is - begin - Put_Char (Outfile_2, C); - end Write_Info_Char; - - ------------------------- - -- Write_Info_Initiate -- - ------------------------- - - procedure Write_Info_Initiate (Key : Character) is - begin - Write_Info_Char (Key); - end Write_Info_Initiate; - - -------------------- - -- Write_Info_Nat -- - -------------------- - - procedure Write_Info_Nat (N : Nat) is - begin - if N > 9 then - Write_Info_Nat (N / 10); - end if; - - Write_Info_Char (Character'Val (48 + N mod 10)); - end Write_Info_Nat; - - -------------------------- - -- Write_Info_Terminate -- - -------------------------- - - procedure Write_Info_Terminate is - begin - Write_Info_Char (LF); - end Write_Info_Terminate; - - -- Local instantiations of Put_SPARK_Xrefs and Get_SPARK_Xrefs - - procedure Get_SPARK_Xrefs_Info is new Get_SPARK_Xrefs; - procedure Put_SPARK_Xrefs_Info is new Put_SPARK_Xrefs; - - -- Start of processing for Process - - begin - -- Loop to skip till first 'F' line - - loop - C := Get_Char (Infile); - - if C = EOF then - raise Stop; - - elsif C = LF or else C = CR then - loop - C := Get_Char (Infile); - exit when C /= LF and then C /= CR; - end loop; - - exit when C = 'F'; - end if; - end loop; - - -- Position back to initial 'F' of first 'F' line - - Set_Index (Infile, Index (Infile) - 1); - - -- Read SPARK cross-reference information to internal SPARK tables, also - -- copying SPARK xrefs info to Outfile_1. - - Initialize_SPARK_Tables; - Get_SPARK_Xrefs_Info; - - -- Write SPARK cross-reference information from internal SPARK tables to - -- Outfile_2. - - Put_SPARK_Xrefs_Info; - - -- Junk blank line (see comment at end of Lib.Writ) - - Write_Info_Terminate; - - -- Flush to disk - - Close (Outfile_1); - Close (Outfile_2); - - -- Now Outfile_1 and Outfile_2 should be identical - - Diff_Result := - Spawn (Diff_Exec.all, - Argument_String_To_List - ("-u " & Name1.all & " " & Name2.all).all); - - if Diff_Result /= 0 then - Ada.Text_IO.Put_Line ("diff(1) exit status" & Diff_Result'Img); - end if; - - OS_Exit (Diff_Result); - - end Process; - -exception - when Stop => - null; -end SPARK_Xrefs_Test; diff --git a/gcc/testsuite/ChangeLog b/gcc/testsuite/ChangeLog index a0a32f8..2b42d04 100644 --- a/gcc/testsuite/ChangeLog +++ b/gcc/testsuite/ChangeLog @@ -1,3 +1,9 @@ +2017-11-08 Javier Miranda <miranda@adacore.com> + + * 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. + 2017-11-08 Andreas Schwab <schwab@suse.de> * c-c++-common/torture/aarch64-vect-lane-2.c (search_line_fast): diff --git a/gcc/testsuite/gnat.dg/overriding_ops2.adb b/gcc/testsuite/gnat.dg/overriding_ops2.adb new file mode 100644 index 0000000..9ab2f5c --- /dev/null +++ b/gcc/testsuite/gnat.dg/overriding_ops2.adb @@ -0,0 +1,8 @@ +-- { dg-do compile } + +package body Overriding_Ops2 is + overriding procedure Finalize (Self : in out Consumer) is + begin + null; + end Finalize; +end Overriding_Ops2; diff --git a/gcc/testsuite/gnat.dg/overriding_ops2.ads b/gcc/testsuite/gnat.dg/overriding_ops2.ads new file mode 100644 index 0000000..695cffb --- /dev/null +++ b/gcc/testsuite/gnat.dg/overriding_ops2.ads @@ -0,0 +1,12 @@ +with Overriding_Ops2_Pkg.High; + +package Overriding_Ops2 is + type Consumer is tagged limited private; +private + type Consumer is + limited + new Overriding_Ops2_Pkg.High.High_Level_Session + with null record; + + overriding procedure Finalize (Self : in out Consumer); +end Overriding_Ops2; diff --git a/gcc/testsuite/gnat.dg/overriding_ops2_pkg-high.ads b/gcc/testsuite/gnat.dg/overriding_ops2_pkg-high.ads new file mode 100644 index 0000000..46eb462 --- /dev/null +++ b/gcc/testsuite/gnat.dg/overriding_ops2_pkg-high.ads @@ -0,0 +1,5 @@ +package Overriding_Ops2_Pkg.High is + type High_Level_Session is new Session_Type with private; +private + type High_Level_Session is new Session_Type with null record; +end Overriding_Ops2_Pkg.High; diff --git a/gcc/testsuite/gnat.dg/overriding_ops2_pkg.ads b/gcc/testsuite/gnat.dg/overriding_ops2_pkg.ads new file mode 100644 index 0000000..85c8f0b --- /dev/null +++ b/gcc/testsuite/gnat.dg/overriding_ops2_pkg.ads @@ -0,0 +1,9 @@ +with Ada.Finalization; + +package Overriding_Ops2_Pkg is + type Session_Type is abstract tagged limited private; + procedure Finalize (Session : in out Session_Type); +private + type Session_Type is + abstract new Ada.Finalization.Limited_Controlled with null record; +end Overriding_Ops2_Pkg; |