| ------------------------------------------------------------------------------ |
| -- -- |
| -- GNAT COMPILER COMPONENTS -- |
| -- -- |
| -- 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 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. |
| |
| with Types; use Types; |
| with GNAT.Table; |
| |
| 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. |
| |
| -- 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 -- |
| -- ------------------------------- |
| |
| -- 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_Name : String_Ptr; |
| -- Pointer to entity name in ALI file |
| |
| Entity_Line : Nat; |
| -- Line number for the entity referenced |
| |
| Etype : Character; |
| -- Indicates type of entity, using code used in ALI file: |
| -- > = IN parameter |
| -- < = OUT parameter |
| -- = = IN OUT parameter |
| -- * = all other cases |
| |
| Entity_Col : Nat; |
| -- Column number for the entity referenced |
| |
| File_Num : Nat; |
| -- File dependency number for the cross-reference. Note that if no file |
| -- entry is present explicitly, this is just a copy of the reference for |
| -- the current cross-reference section. |
| |
| Scope_Num : Nat; |
| -- Scope number for the cross-reference. Note that if no scope entry is |
| -- present explicitly, this is just a copy of the reference for the |
| -- current cross-reference section. |
| |
| Line : Nat; |
| -- Line number for the reference |
| |
| Rtype : Character; |
| -- Indicates type of the reference, using code used in ALI file: |
| -- r = reference |
| -- c = reference to constant object |
| -- m = modification |
| -- s = call |
| |
| Col : Nat; |
| -- Column number for the reference |
| end record; |
| |
| package SPARK_Xref_Table is new GNAT.Table ( |
| Table_Component_Type => SPARK_Xref_Record, |
| Table_Index_Type => Xref_Index, |
| Table_Low_Bound => 1, |
| Table_Initial => 2000, |
| Table_Increment => 300); |
| |
| ----------------- |
| -- 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 |
| Scope_Name : String_Ptr; |
| -- Pointer to scope name in ALI file |
| |
| File_Num : Nat; |
| -- Set to the file dependency number for the scope |
| |
| Scope_Num : Pos; |
| -- Set to the scope number for the scope |
| |
| Spec_File_Num : Nat; |
| -- Set to the file dependency number for the scope corresponding to the |
| -- spec of the current scope entity, if different, or else 0. |
| |
| Spec_Scope_Num : Nat; |
| -- Set to the scope number for the scope corresponding to the spec of |
| -- the current scope entity, if different, or else 0. |
| |
| Line : Nat; |
| -- Line number for the scope |
| |
| Stype : Character; |
| -- Indicates type of scope, using code used in ALI file: |
| -- K = package |
| -- T = task |
| -- U = procedure |
| -- V = function |
| -- Y = entry |
| |
| Col : Nat; |
| -- Column number for the scope |
| |
| From_Xref : Xref_Index; |
| -- Starting index in Xref table for this scope |
| |
| To_Xref : Xref_Index; |
| -- Ending index in Xref table for this scope |
| |
| -- The following component is only used in-memory, not printed out in |
| -- ALI file. |
| |
| Scope_Entity : Entity_Id := Empty; |
| -- Entity (subprogram or package) for the scope |
| end record; |
| |
| package SPARK_Scope_Table is new GNAT.Table ( |
| Table_Component_Type => SPARK_Scope_Record, |
| Table_Index_Type => Scope_Index, |
| Table_Low_Bound => 1, |
| Table_Initial => 200, |
| Table_Increment => 300); |
| |
| ---------------- |
| -- 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_Name : String_Ptr; |
| -- Pointer to file name in ALI file |
| |
| Unit_File_Name : String_Ptr; |
| -- Pointer to file name for unit in ALI file, when File_Name refers to a |
| -- subunit; otherwise null. |
| |
| 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 GNAT.Table ( |
| Table_Component_Type => SPARK_File_Record, |
| Table_Index_Type => File_Index, |
| Table_Low_Bound => 1, |
| Table_Initial => 20, |
| Table_Increment => 200); |
| |
| --------------- |
| -- Constants -- |
| --------------- |
| |
| Name_Of_Heap_Variable : constant String := "__HEAP"; |
| -- Name of special variable used in effects to denote reads and writes |
| -- through explicit dereference. |
| |
| ----------------- |
| -- 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. |
| |
| 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; |
