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

1 files changed, 5 insertions, 161 deletions

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;