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-2013, 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          Start : Scope_Index;
  36          Stop  : Scope_Index;
  37
  38       begin
  39          Start := F.From_Scope;
  40          Stop  := F.To_Scope;
  41
  42          Write_Info_Initiate ('F');
  43          Write_Info_Char ('D');
  44          Write_Info_Char (' ');
  45          Write_Info_Nat (F.File_Num);
  46          Write_Info_Char (' ');
  47
  48          for N in F.File_Name'Range loop
  49             Write_Info_Char (F.File_Name (N));
  50          end loop;
  51
  52          --  If file is a subunit, print the file name for the unit
  53
  54          if F.Unit_File_Name /= null then
  55             Write_Info_Char (' ');
  56             Write_Info_Char ('-');
  57             Write_Info_Char ('>');
  58             Write_Info_Char (' ');
  59
  60             for N in F.Unit_File_Name'Range loop
  61                Write_Info_Char (F.Unit_File_Name (N));
  62             end loop;
  63          end if;
  64
  65          Write_Info_Terminate;
  66
  67          --  Loop through scope entries for this file
  68
  69          loop
  70             exit when Start = Stop + 1;
  71             pragma Assert (Start <= Stop);
  72
  73             declare
  74                S : SPARK_Scope_Record renames SPARK_Scope_Table.Table (Start);
  75
  76             begin
  77                Write_Info_Initiate ('F');
  78                Write_Info_Char ('S');
  79                Write_Info_Char (' ');
  80                Write_Info_Char ('.');
  81                Write_Info_Nat (S.Scope_Num);
  82                Write_Info_Char (' ');
  83                Write_Info_Nat (S.Line);
  84                Write_Info_Char (S.Stype);
  85                Write_Info_Nat (S.Col);
  86                Write_Info_Char (' ');
  87
  88                pragma Assert (S.Scope_Name.all /= "");
  89
  90                for N in S.Scope_Name'Range loop
  91                   Write_Info_Char (S.Scope_Name (N));
  92                end loop;
  93
  94                if S.Spec_File_Num /= 0 then
  95                   Write_Info_Char (' ');
  96                   Write_Info_Char ('-');
  97                   Write_Info_Char ('>');
  98                   Write_Info_Char (' ');
  99                   Write_Info_Nat (S.Spec_File_Num);
 100                   Write_Info_Char ('.');
 101                   Write_Info_Nat (S.Spec_Scope_Num);
 102                end if;
 103
 104                Write_Info_Terminate;
 105             end;
 106
 107             Start := Start + 1;
 108          end loop;
 109       end;
 110    end loop;
 111
 112    --  Loop through entries in SPARK_File_Table
 113
 114    for J in 1 .. SPARK_File_Table.Last loop
 115       declare
 116          F           : SPARK_File_Record renames SPARK_File_Table.Table (J);
 117          Start       : Scope_Index;
 118          Stop        : Scope_Index;
 119          File        : Nat;
 120          Scope       : Nat;
 121          Entity_Line : Nat;
 122          Entity_Col  : Nat;
 123
 124       begin
 125          Start := F.From_Scope;
 126          Stop  := F.To_Scope;
 127
 128          --  Loop through scope entries for this file
 129
 130          loop
 131             exit when Start = Stop + 1;
 132             pragma Assert (Start <= Stop);
 133
 134             Output_One_Scope : declare
 135                S : SPARK_Scope_Record renames SPARK_Scope_Table.Table (Start);
 136
 137                XStart : Xref_Index;
 138                XStop  : Xref_Index;
 139
 140             begin
 141                XStart := S.From_Xref;
 142                XStop  := S.To_Xref;
 143
 144                if XStart > XStop then
 145                   goto Continue;
 146                end if;
 147
 148                Write_Info_Initiate ('F');
 149                Write_Info_Char ('X');
 150                Write_Info_Char (' ');
 151                Write_Info_Nat (F.File_Num);
 152                Write_Info_Char (' ');
 153
 154                for N in F.File_Name'Range loop
 155                   Write_Info_Char (F.File_Name (N));
 156                end loop;
 157
 158                Write_Info_Char (' ');
 159                Write_Info_Char ('.');
 160                Write_Info_Nat (S.Scope_Num);
 161                Write_Info_Char (' ');
 162
 163                for N in S.Scope_Name'Range loop
 164                   Write_Info_Char (S.Scope_Name (N));
 165                end loop;
 166
 167                --  Default value of (0,0) is used for the special __HEAP
 168                --  variable so use another default value.
 169
 170                Entity_Line := 0;
 171                Entity_Col  := 1;
 172
 173                --  Loop through cross reference entries for this scope
 174
 175                loop
 176                   exit when XStart = XStop + 1;
 177                   pragma Assert (XStart <= XStop);
 178
 179                   Output_One_Xref : declare
 180                      R : SPARK_Xref_Record renames
 181                            SPARK_Xref_Table.Table (XStart);
 182
 183                   begin
 184                      if R.Entity_Line /= Entity_Line
 185                        or else R.Entity_Col /= Entity_Col
 186                      then
 187                         Write_Info_Terminate;
 188
 189                         Write_Info_Initiate ('F');
 190                         Write_Info_Char (' ');
 191                         Write_Info_Nat (R.Entity_Line);
 192                         Write_Info_Char (R.Etype);
 193                         Write_Info_Nat (R.Entity_Col);
 194                         Write_Info_Char (' ');
 195
 196                         for N in R.Entity_Name'Range loop
 197                            Write_Info_Char (R.Entity_Name (N));
 198                         end loop;
 199
 200                         Entity_Line := R.Entity_Line;
 201                         Entity_Col  := R.Entity_Col;
 202                         File        := F.File_Num;
 203                         Scope       := S.Scope_Num;
 204                      end if;
 205
 206                      if Write_Info_Col > 72 then
 207                         Write_Info_Terminate;
 208                         Write_Info_Initiate ('.');
 209                      end if;
 210
 211                      Write_Info_Char (' ');
 212
 213                      if R.File_Num /= File then
 214                         Write_Info_Nat (R.File_Num);
 215                         Write_Info_Char ('|');
 216                         File  := R.File_Num;
 217                         Scope := 0;
 218                      end if;
 219
 220                      if R.Scope_Num /= Scope then
 221                         Write_Info_Char ('.');
 222                         Write_Info_Nat (R.Scope_Num);
 223                         Write_Info_Char (':');
 224                         Scope := R.Scope_Num;
 225                      end if;
 226
 227                      Write_Info_Nat (R.Line);
 228                      Write_Info_Char (R.Rtype);
 229                      Write_Info_Nat (R.Col);
 230                   end Output_One_Xref;
 231
 232                   XStart := XStart + 1;
 233                end loop;
 234
 235                Write_Info_Terminate;
 236             end Output_One_Scope;
 237
 238          <<Continue>>
 239             Start := Start + 1;
 240          end loop;
 241       end;
 242    end loop;
 243 end Put_SPARK_Xrefs;