Skip to content

R
riscv-gcc-1
Commit 7cc7f3aa by Pierre-Marie de Rodat
Options

sem_disp.adb (Is_Inherited_Public_Operation): Extend the functionality of this… 

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
parent daf82dd8
Showing with 311 additions and 946 deletions
gcc/ada/ChangeLog
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
......
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");
......
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);
......
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 =>
......
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);
......
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 \
......
gcc/ada/get_spark_xrefs.ads deleted 100644 → 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.
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
......
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;
......
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;
......
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
......
gcc/ada/put_spark_xrefs.adb deleted 100644 → 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;
gcc/ada/put_spark_xrefs.ads deleted 100644 → 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.
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
......
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;
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;
gcc/ada/spark_xrefs_test.adb deleted 100644 → 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;
gcc/testsuite/ChangeLog
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):
......
gcc/testsuite/gnat.dg/overriding_ops2.adb 0 → 100644
-- { dg-do compile }
package body Overriding_Ops2 is
overriding procedure Finalize (Self : in out Consumer) is
begin
null;
end Finalize;
end Overriding_Ops2;
gcc/testsuite/gnat.dg/overriding_ops2.ads 0 → 100644
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;
gcc/testsuite/gnat.dg/overriding_ops2_pkg-high.ads 0 → 100644
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;
gcc/testsuite/gnat.dg/overriding_ops2_pkg.ads 0 → 100644
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;
Markdown is supported
0% or
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment