gcc/ada/put_spark_xrefs.adb

   1 ------------------------------------------------------------------------------
   2 --                                                                          --
   3 --                         GNAT COMPILER COMPONENTS                         --
   4 --                                                                          --
   5 --                       P U T _ S P A R K _ X R E F S                      --
   6 --                                                                          --
   7 --                                 B o d y                                  --
   8 --                                                                          --
   9 --          Copyright (C) 2011-2016, 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 with SPARK_Xrefs; use SPARK_Xrefs;
  27
  28 procedure Put_SPARK_Xrefs is
  29 begin
  30    --  Loop through entries in SPARK_File_Table
  31
  32    for J in 1 .. SPARK_File_Table.Last loop
  33       declare
  34          F : SPARK_File_Record renames SPARK_File_Table.Table (J);
  35
  36       begin
  37          Write_Info_Initiate ('F');
  38          Write_Info_Char ('D');
  39          Write_Info_Char (' ');
  40          Write_Info_Nat (F.File_Num);
  41          Write_Info_Char (' ');
  42
  43          Write_Info_Str (F.File_Name.all);
  44
  45          --  If file is a subunit, print the file name for the unit
  46
  47          if F.Unit_File_Name /= null then
  48             Write_Info_Str (" -> " & F.Unit_File_Name.all);
  49          end if;
  50
  51          Write_Info_Terminate;
  52
  53          --  Loop through scope entries for this file
  54
  55          for J in F.From_Scope .. F.To_Scope loop
  56             declare
  57                S : SPARK_Scope_Record renames SPARK_Scope_Table.Table (J);
  58
  59             begin
  60                Write_Info_Initiate ('F');
  61                Write_Info_Char ('S');
  62                Write_Info_Char (' ');
  63                Write_Info_Char ('.');
  64                Write_Info_Nat (S.Scope_Num);
  65                Write_Info_Char (' ');
  66                Write_Info_Nat (S.Line);
  67                Write_Info_Char (S.Stype);
  68                Write_Info_Nat (S.Col);
  69                Write_Info_Char (' ');
  70
  71                pragma Assert (S.Scope_Name.all /= "");
  72
  73                Write_Info_Str (S.Scope_Name.all);
  74
  75                if S.Spec_File_Num /= 0 then
  76                   Write_Info_Str (" -> ");
  77                   Write_Info_Nat (S.Spec_File_Num);
  78                   Write_Info_Char ('.');
  79                   Write_Info_Nat (S.Spec_Scope_Num);
  80                end if;
  81
  82                Write_Info_Terminate;
  83             end;
  84          end loop;
  85       end;
  86    end loop;
  87
  88    --  Loop through entries in SPARK_File_Table
  89
  90    for J in 1 .. SPARK_File_Table.Last loop
  91       declare
  92          F           : SPARK_File_Record renames SPARK_File_Table.Table (J);
  93          File        : Nat;
  94          Scope       : Nat;
  95          Entity_Line : Nat;
  96          Entity_Col  : Nat;
  97
  98       begin
  99          --  Loop through scope entries for this file
 100
 101          for K in F.From_Scope .. F.To_Scope loop
 102             Output_One_Scope : declare
 103                S : SPARK_Scope_Record renames SPARK_Scope_Table.Table (K);
 104
 105             begin
 106                --  Write only non-empty tables
 107
 108                if S.From_Xref <= S.To_Xref then
 109
 110                   Write_Info_Initiate ('F');
 111                   Write_Info_Char ('X');
 112                   Write_Info_Char (' ');
 113                   Write_Info_Nat (F.File_Num);
 114                   Write_Info_Char (' ');
 115
 116                   Write_Info_Str (F.File_Name.all);
 117
 118                   Write_Info_Char (' ');
 119                   Write_Info_Char ('.');
 120                   Write_Info_Nat (S.Scope_Num);
 121                   Write_Info_Char (' ');
 122
 123                   Write_Info_Str (S.Scope_Name.all);
 124
 125                   --  Default value of (0,0) is used for the special __HEAP
 126                   --  variable so use another default value.
 127
 128                   Entity_Line := 0;
 129                   Entity_Col  := 1;
 130
 131                   --  Loop through cross reference entries for this scope
 132
 133                   for X in S.From_Xref .. S.To_Xref loop
 134
 135                      Output_One_Xref : declare
 136                         R : SPARK_Xref_Record renames
 137                               SPARK_Xref_Table.Table (X);
 138
 139                      begin
 140                         if R.Entity_Line /= Entity_Line
 141                           or else R.Entity_Col /= Entity_Col
 142                         then
 143                            Write_Info_Terminate;
 144
 145                            Write_Info_Initiate ('F');
 146                            Write_Info_Char (' ');
 147                            Write_Info_Nat (R.Entity_Line);
 148                            Write_Info_Char (R.Etype);
 149                            Write_Info_Nat (R.Entity_Col);
 150                            Write_Info_Char (' ');
 151
 152                            Write_Info_Str (R.Entity_Name.all);
 153
 154                            Entity_Line := R.Entity_Line;
 155                            Entity_Col  := R.Entity_Col;
 156                            File        := F.File_Num;
 157                            Scope       := S.Scope_Num;
 158                         end if;
 159
 160                         if Write_Info_Col > 72 then
 161                            Write_Info_Terminate;
 162                            Write_Info_Initiate ('.');
 163                         end if;
 164
 165                         Write_Info_Char (' ');
 166
 167                         if R.File_Num /= File then
 168                            Write_Info_Nat (R.File_Num);
 169                            Write_Info_Char ('|');
 170                            File  := R.File_Num;
 171                            Scope := 0;
 172                         end if;
 173
 174                         if R.Scope_Num /= Scope then
 175                            Write_Info_Char ('.');
 176                            Write_Info_Nat (R.Scope_Num);
 177                            Write_Info_Char (':');
 178                            Scope := R.Scope_Num;
 179                         end if;
 180
 181                         Write_Info_Nat (R.Line);
 182                         Write_Info_Char (R.Rtype);
 183                         Write_Info_Nat (R.Col);
 184                      end Output_One_Xref;
 185
 186                   end loop;
 187
 188                   Write_Info_Terminate;
 189                end if;
 190             end Output_One_Scope;
 191          end loop;
 192       end;
 193    end loop;
 194 end Put_SPARK_Xrefs;