From 7cc7f3aa68b852b217c511e7d841458b0bdd532a Mon Sep 17 00:00:00 2001 From: Pierre-Marie de Rodat Date: Wed, 8 Nov 2017 15:17:43 +0000 Subject: 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 * sem_disp.adb (Is_Inherited_Public_Operation): Extend the functionality of this routine to handle multiple levels of derivations. 2017-11-08 Hristian Kirtchev * einfo.adb: Elist36 is now used as Nested_Scenarios. (Nested_Scenarios): New routine. (Set_Nested_Scenarios): New routine. (Write_Field36_Name): New routine. * einfo.ads: Add new attribute Nested_Scenarios along with occurrences in entities. (Nested_Scenarios): New routine along with pragma Inline. (Set_Nested_Scenarios): New routine along with pragma Inline. * sem_elab.adb (Find_And_Process_Nested_Scenarios): New routine. (Process_Nested_Scenarios): New routine. (Traverse_Body): When a subprogram body is traversed for the first time, find, save, and process all suitable scenarios found within. Subsequent traversals of the same subprogram body utilize the saved scenarios. 2017-11-08 Piotr Trojanek * lib-xref-spark_specific.adb (Add_SPARK_Scope): Remove detection of protected operations. (Add_SPARK_Xrefs): Simplify detection of empty entities. * get_spark_xrefs.ads, get_spark_xrefs.adb, put_spark_xrefs.ads, put_spark_xrefs.adb, spark_xrefs_test.adb: Remove code for writing, reading and testing SPARK cross-references stored in the ALI files. * lib-xref.ads (Output_SPARK_Xrefs): Remove. * lib-writ.adb (Write_ALI): Do not write SPARK cross-references to the ALI file. * spark_xrefs.ads, spark_xrefs.adb (pspark): Remove, together with description of the SPARK xrefs ALI format. * gcc-interface/Make-lang.in (GNAT_ADA_OBJS): Remove get_spark_refs.o and put_spark_refs.o. 2017-11-08 Hristian Kirtchev * exp_ch4.adb (Apply_Accessibility_Check): Do not finalize the object when the associated access type is subject to pragma No_Heap_Finalization. * exp_intr.adb (Expand_Unc_Deallocation): Use the available view of the designated type in case it comes from a limited withed unit. gcc/testsuite/ 2017-11-08 Javier Miranda * gnat.dg/overriding_ops2.adb, gnat.dg/overriding_ops2.ads, gnat.dg/overriding_ops2_pkg.ads, gnat.dg/overriding_ops2_pkg-high.ads: New testcase. From-SVN: r254532 --- gcc/ada/spark_xrefs.ads | 166 ++---------------------------------------------- 1 file changed, 5 insertions(+), 161 deletions(-) (limited to 'gcc/ada/spark_xrefs.ads') 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; -- cgit v1.1