gcc/ada/spark_xrefs.ads

   1 ------------------------------------------------------------------------------
   2 --                                                                          --
   3 --                         GNAT COMPILER COMPONENTS                         --
   4 --                                                                          --
   5 --                           S P A R K _ X R E F S                          --
   6 --                                                                          --
   7 --                                 S p e c                                  --
   8 --                                                                          --
   9 --          Copyright (C) 2011-2017, Free Software Foundation, Inc.         --
  10 --                                                                          --
  11 -- GNAT is free software;  you can  redistribute it  and/or modify it under --
  12 -- terms of the  GNU General Public License as published  by the Free Soft- --
  13 -- ware  Foundation;  either version 3,  or (at your option) any later ver- --
  14 -- sion.  GNAT is distributed in the hope that it will be useful, but WITH- --
  15 -- OUT ANY WARRANTY;  without even the  implied warranty of MERCHANTABILITY --
  16 -- or FITNESS FOR A PARTICULAR PURPOSE.  See the GNU General Public License --
  17 -- for  more details.  You should have  received  a copy of the GNU General --
  18 -- Public License  distributed with GNAT; see file COPYING3.  If not, go to --
  19 -- http://www.gnu.org/licenses for a complete copy of the license.          --
  20 --                                                                          --
  21 -- GNAT was originally developed  by the GNAT team at  New York University. --
  22 -- Extensive contributions were provided by Ada Core Technologies Inc.      --
  23 --                                                                          --
  24 ------------------------------------------------------------------------------
  25
  26 --  This package defines tables used to store information needed for the SPARK
  27 --  mode. It is used by procedures in Lib.Xref.SPARK_Specific to build the
  28 --  SPARK-specific cross-reference information.
  29
  30 with Table;
  31 with Types; use Types;
  32
  33 package SPARK_Xrefs is
  34
  35    --  SPARK cross-reference information is stored internally using three
  36    --  tables: SPARK_Xref_Table, SPARK_Scope_Table and SPARK_File_Table, which
  37    --  are defined in this unit.
  38
  39    --  Lib.Xref.SPARK_Specific is part of the compiler. It extracts SPARK
  40    --  cross-reference information from the complete set of cross-references
  41    --  generated during compilation.
  42
  43    --  -------------------------------
  44    --  -- Generated Globals Section --
  45    --  -------------------------------
  46
  47    --  The Generated Globals section is located at the end of the ALI file
  48
  49    --  All lines with information related to the Generated Globals begin with
  50    --  string "GG". This string should therefore not be used in the beginning
  51    --  of any line not related to Generated Globals.
  52
  53    --  The processing (reading and writing) of this section happens in package
  54    --  Flow_Generated_Globals (from the SPARK 2014 sources), for further
  55    --  information please refer there.
  56
  57    ----------------
  58    -- Xref Table --
  59    ----------------
  60
  61    --  The following table records SPARK cross-references
  62
  63    type Xref_Index is new Nat;
  64    --  Used to index values in this table. Values start at 1 and are assigned
  65    --  sequentially as entries are constructed; value 0 is used temporarily
  66    --  until a proper value is determined.
  67
  68    type SPARK_Xref_Record is record
  69       Entity_Name : String_Ptr;
  70       --  Pointer to entity name in ALI file
  71
  72       Entity_Line : Nat;
  73       --  Line number for the entity referenced
  74
  75       Etype : Character;
  76       --  Indicates type of entity, using code used in ALI file:
  77       --    > = IN parameter
  78       --    < = OUT parameter
  79       --    = = IN OUT parameter
  80       --    * = all other cases
  81
  82       Entity_Col : Nat;
  83       --  Column number for the entity referenced
  84
  85       File_Num : Nat;
  86       --  File dependency number for the cross-reference. Note that if no file
  87       --  entry is present explicitly, this is just a copy of the reference for
  88       --  the current cross-reference section.
  89
  90       Scope_Num : Nat;
  91       --  Scope number for the cross-reference. Note that if no scope entry is
  92       --  present explicitly, this is just a copy of the reference for the
  93       --  current cross-reference section.
  94
  95       Line : Nat;
  96       --  Line number for the reference
  97
  98       Rtype : Character;
  99       --  Indicates type of the reference, using code used in ALI file:
 100       --    r = reference
 101       --    c = reference to constant object
 102       --    m = modification
 103       --    s = call
 104
 105       Col : Nat;
 106       --  Column number for the reference
 107    end record;
 108
 109    package SPARK_Xref_Table is new Table.Table (
 110      Table_Component_Type => SPARK_Xref_Record,
 111      Table_Index_Type     => Xref_Index,
 112      Table_Low_Bound      => 1,
 113      Table_Initial        => 2000,
 114      Table_Increment      => 300,
 115      Table_Name           => "Xref_Table");
 116
 117    -----------------
 118    -- Scope Table --
 119    -----------------
 120
 121    --  This table keeps track of the scopes and the corresponding starting and
 122    --  ending indexes (From, To) in the Xref table.
 123
 124    type Scope_Index is new Nat;
 125    --  Used to index values in this table. Values start at 1 and are assigned
 126    --  sequentially as entries are constructed; value 0 indicates that no
 127    --  entries have been constructed and is also used until a proper value is
 128    --  determined.
 129
 130    type SPARK_Scope_Record is record
 131       Scope_Name : String_Ptr;
 132       --  Pointer to scope name in ALI file
 133
 134       File_Num : Nat;
 135       --  Set to the file dependency number for the scope
 136
 137       Scope_Num : Pos;
 138       --  Set to the scope number for the scope
 139
 140       Spec_File_Num : Nat;
 141       --  Set to the file dependency number for the scope corresponding to the
 142       --  spec of the current scope entity, if different, or else 0.
 143
 144       Spec_Scope_Num : Nat;
 145       --  Set to the scope number for the scope corresponding to the spec of
 146       --  the current scope entity, if different, or else 0.
 147
 148       Line : Nat;
 149       --  Line number for the scope
 150
 151       Stype : Character;
 152       --  Indicates type of scope, using code used in ALI file:
 153       --    K = package
 154       --    T = task
 155       --    U = procedure
 156       --    V = function
 157       --    Y = entry
 158
 159       Col : Nat;
 160       --  Column number for the scope
 161
 162       From_Xref : Xref_Index;
 163       --  Starting index in Xref table for this scope
 164
 165       To_Xref : Xref_Index;
 166       --  Ending index in Xref table for this scope
 167
 168       --  The following component is only used in-memory, not printed out in
 169       --  ALI file.
 170
 171       Scope_Entity : Entity_Id := Empty;
 172       --  Entity (subprogram or package) for the scope
 173    end record;
 174
 175    package SPARK_Scope_Table is new Table.Table (
 176      Table_Component_Type => SPARK_Scope_Record,
 177      Table_Index_Type     => Scope_Index,
 178      Table_Low_Bound      => 1,
 179      Table_Initial        => 200,
 180      Table_Increment      => 300,
 181      Table_Name           => "Scope_Table");
 182
 183    ----------------
 184    -- File Table --
 185    ----------------
 186
 187    --  This table keeps track of the units and the corresponding starting and
 188    --  ending indexes (From, To) in the Scope table.
 189
 190    type File_Index is new Nat;
 191    --  Used to index values in this table. Values start at 1 and are assigned
 192    --  sequentially as entries are constructed; value 0 indicates that no
 193    --  entries have been constructed.
 194
 195    type SPARK_File_Record is record
 196       File_Name : String_Ptr;
 197       --  Pointer to file name in ALI file
 198
 199       Unit_File_Name : String_Ptr;
 200       --  Pointer to file name for unit in ALI file, when File_Name refers to a
 201       --  subunit; otherwise null.
 202
 203       File_Num : Nat;
 204       --  Dependency number in ALI file
 205
 206       From_Scope : Scope_Index;
 207       --  Starting index in Scope table for this unit
 208
 209       To_Scope : Scope_Index;
 210       --  Ending index in Scope table for this unit
 211    end record;
 212
 213    package SPARK_File_Table is new Table.Table (
 214      Table_Component_Type => SPARK_File_Record,
 215      Table_Index_Type     => File_Index,
 216      Table_Low_Bound      => 1,
 217      Table_Initial        => 20,
 218      Table_Increment      => 200,
 219      Table_Name           => "File_Table");
 220
 221    ---------------
 222    -- Constants --
 223    ---------------
 224
 225    Name_Of_Heap_Variable : constant String := "__HEAP";
 226    --  Name of special variable used in effects to denote reads and writes
 227    --  through explicit dereference.
 228
 229    -----------------
 230    -- Subprograms --
 231    -----------------
 232
 233    procedure Initialize_SPARK_Tables;
 234    --  Reset tables for a new compilation
 235
 236    procedure dspark;
 237    --  Debug routine to dump internal SPARK cross-reference tables. This is a
 238    --  raw format dump showing exactly what the tables contain.
 239
 240 end SPARK_Xrefs;