diff options
Diffstat (limited to 'gcc/ada/spark_xrefs.ads')
| -rw-r--r-- | gcc/ada/spark_xrefs.ads | 118 |
1 files changed, 4 insertions, 114 deletions
diff --git a/gcc/ada/spark_xrefs.ads b/gcc/ada/spark_xrefs.ads index df1d8e89..25af902 100644 --- a/gcc/ada/spark_xrefs.ads +++ b/gcc/ada/spark_xrefs.ads @@ -23,48 +23,13 @@ -- -- ------------------------------------------------------------------------------ --- This package defines tables used to store information needed for the SPARK --- mode. It is used by procedures in Lib.Xref.SPARK_Specific to build the --- SPARK-specific cross-reference information. +-- This package defines data structures used to expose frontend +-- cross-references to the SPARK backend. -with Table; with Types; use Types; package SPARK_Xrefs is - -- SPARK cross-reference information is stored internally using three - -- tables: SPARK_Xref_Table, SPARK_Scope_Table and SPARK_File_Table, which - -- are defined in this unit. - - -- Lib.Xref.SPARK_Specific is part of the compiler. It extracts SPARK - -- cross-reference information from the complete set of cross-references - -- generated during compilation. - - -- ------------------------------- - -- -- Generated Globals Section -- - -- ------------------------------- - - -- The Generated Globals section is located at the end of the ALI file - - -- All lines with information related to the Generated Globals begin with - -- string "GG". This string should therefore not be used in the beginning - -- of any line not related to Generated Globals. - - -- The processing (reading and writing) of this section happens in package - -- Flow_Generated_Globals (from the SPARK 2014 sources), for further - -- information please refer there. - - ---------------- - -- Xref Table -- - ---------------- - - -- The following table records SPARK cross-references - - type Xref_Index is new Nat; - -- Used to index values in this table. Values start at 1 and are assigned - -- sequentially as entries are constructed; value 0 is used temporarily - -- until a proper value is determined. - type SPARK_Xref_Record is record Entity : Entity_Id; -- Referenced entity @@ -78,80 +43,8 @@ package SPARK_Xrefs is -- m = modification -- s = call end record; - - package SPARK_Xref_Table is new Table.Table ( - Table_Component_Type => SPARK_Xref_Record, - Table_Index_Type => Xref_Index, - Table_Low_Bound => 1, - Table_Initial => 2000, - Table_Increment => 300, - Table_Name => "Xref_Table"); - - ----------------- - -- Scope Table -- - ----------------- - - -- This table keeps track of the scopes and the corresponding starting and - -- ending indexes (From, To) in the Xref table. - - type Scope_Index is new Nat; - -- Used to index values in this table. Values start at 1 and are assigned - -- sequentially as entries are constructed; value 0 indicates that no - -- entries have been constructed and is also used until a proper value is - -- determined. - - type SPARK_Scope_Record is record - Entity : Entity_Id; - -- Entity that is represented by the scope - - Scope_Num : Pos; - -- Set to the scope number within the enclosing unit - - From_Xref : Xref_Index; - -- Starting index in Xref table for this scope - - To_Xref : Xref_Index; - -- Ending index in Xref table for this scope - end record; - - package SPARK_Scope_Table is new Table.Table ( - Table_Component_Type => SPARK_Scope_Record, - Table_Index_Type => Scope_Index, - Table_Low_Bound => 1, - Table_Initial => 200, - Table_Increment => 300, - Table_Name => "Scope_Table"); - - ---------------- - -- File Table -- - ---------------- - - -- This table keeps track of the units and the corresponding starting and - -- ending indexes (From, To) in the Scope table. - - type File_Index is new Nat; - -- Used to index values in this table. Values start at 1 and are assigned - -- sequentially as entries are constructed; value 0 indicates that no - -- entries have been constructed. - - type SPARK_File_Record is record - File_Num : Nat; - -- Dependency number in ALI file - - From_Scope : Scope_Index; - -- Starting index in Scope table for this unit - - To_Scope : Scope_Index; - -- Ending index in Scope table for this unit - end record; - - package SPARK_File_Table is new Table.Table ( - Table_Component_Type => SPARK_File_Record, - Table_Index_Type => File_Index, - Table_Low_Bound => 1, - Table_Initial => 20, - Table_Increment => 200, - Table_Name => "File_Table"); + -- This type holds a subset of the frontend xref entry that is needed by + -- the SPARK backend. --------------- -- Constants -- @@ -170,9 +63,6 @@ package SPARK_Xrefs is -- Subprograms -- ----------------- - procedure Initialize_SPARK_Tables; - -- Reset tables for a new compilation - procedure dspark; -- Debug routine to dump internal SPARK cross-reference tables. This is a -- raw format dump showing exactly what the tables contain. |