CbC/CbC_gcc: gcc/ada/spark_xrefs.ads comparison

comparison gcc/ada/spark_xrefs.ads @ 111:04ced10e8804

gcc 7

author	kono
date	Fri, 27 Oct 2017 22:46:09 +0900
parents
children	84e7813d76e9

comparison

equal deleted inserted replaced

-:561a7518be6b
+:04ced10e8804
+------------------------------------------------------------------------------
+--                                                                          --
+--                         GNAT COMPILER COMPONENTS                         --
+--                                                                          --
+--                           S P A R K _ X R E F S                          --
+--                                                                          --
+--                                 S p e c                                  --
+--                                                                          --
+--          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- --
+-- 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 Table;
+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.
+--  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 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
+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 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_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 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");
+---------------
+-- 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;

Mercurial > hg > CbC > CbC_gcc

comparison gcc/ada/spark_xrefs.ads @ 111:04ced10e8804