gcc/ada/get_spark_xrefs.adb

   1 ------------------------------------------------------------------------------
   2 --                                                                          --
   3 --                         GNAT COMPILER COMPONENTS                         --
   4 --                                                                          --
   5 --                       G E 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 with Types;       use Types;
  28
  29 with Ada.IO_Exceptions; use Ada.IO_Exceptions;
  30
  31 procedure Get_SPARK_Xrefs is
  32    C : Character;
  33
  34    use ASCII;
  35    --  For CR/LF
  36
  37    Cur_File : Nat;
  38    --  Dependency number for the current file
  39
  40    Cur_Scope : Nat;
  41    --  Scope number for the current scope entity
  42
  43    Cur_File_Idx : File_Index;
  44    --  Index in SPARK_File_Table of the current file
  45
  46    Cur_Scope_Idx : Scope_Index;
  47    --  Index in SPARK_Scope_Table of the current scope
  48
  49    Name_Str : String (1 .. 32768);
  50    Name_Len : Natural := 0;
  51    --  Local string used to store name of File/entity scanned as
  52    --  Name_Str (1 .. Name_Len).
  53
  54    File_Name : String_Ptr;
  55    Unit_File_Name : String_Ptr;
  56
  57    -----------------------
  58    -- Local Subprograms --
  59    -----------------------
  60
  61    function At_EOL return Boolean;
  62    --  Skips any spaces, then checks if at the end of a line. If so, returns
  63    --  True (but does not skip the EOL sequence). If not, then returns False.
  64
  65    procedure Check (C : Character);
  66    --  Checks that file is positioned at given character, and if so skips past
  67    --  it, If not, raises Data_Error.
  68
  69    function Get_Nat return Nat;
  70    --  On entry the file is positioned to a digit. On return, the file is
  71    --  positioned past the last digit, and the returned result is the decimal
  72    --  value read. Data_Error is raised for overflow (value greater than
  73    --  Int'Last), or if the initial character is not a digit.
  74
  75    procedure Get_Name;
  76    --  On entry the file is positioned to a name. On return, the file is
  77    --  positioned past the last character, and the name scanned is returned
  78    --  in Name_Str (1 .. Name_Len).
  79
  80    procedure Skip_EOL;
  81    --  Called with the current character about to be read being LF or CR. Skips
  82    --  past CR/LF characters until either a non-CR/LF character is found, or
  83    --  the end of file is encountered.
  84
  85    procedure Skip_Spaces;
  86    --  Skips zero or more spaces at the current position, leaving the file
  87    --  positioned at the first non-blank character (or Types.EOF).
  88
  89    ------------
  90    -- At_EOL --
  91    ------------
  92
  93    function At_EOL return Boolean is
  94    begin
  95       Skip_Spaces;
  96       return Nextc = CR or else Nextc = LF;
  97    end At_EOL;
  98
  99    -----------
 100    -- Check --
 101    -----------
 102
 103    procedure Check (C : Character) is
 104    begin
 105       if Nextc = C then
 106          Skipc;
 107       else
 108          raise Data_Error;
 109       end if;
 110    end Check;
 111
 112    -------------
 113    -- Get_Nat --
 114    -------------
 115
 116    function Get_Nat return Nat is
 117       Val : Nat;
 118       C   : Character;
 119
 120    begin
 121       C := Nextc;
 122       Val := 0;
 123
 124       if C not in '0' .. '9' then
 125          raise Data_Error;
 126       end if;
 127
 128       --  Loop to read digits of integer value
 129
 130       loop
 131          declare
 132             pragma Unsuppress (Overflow_Check);
 133          begin
 134             Val := Val * 10 + (Character'Pos (C) - Character'Pos ('0'));
 135          end;
 136
 137          Skipc;
 138          C := Nextc;
 139
 140          exit when C not in '0' .. '9';
 141       end loop;
 142
 143       return Val;
 144
 145    exception
 146       when Constraint_Error =>
 147          raise Data_Error;
 148    end Get_Nat;
 149
 150    --------------
 151    -- Get_Name --
 152    --------------
 153
 154    procedure Get_Name is
 155       N : Integer;
 156
 157    begin
 158       N := 0;
 159       while Nextc > ' ' loop
 160          N := N + 1;
 161          Name_Str (N) := Getc;
 162       end loop;
 163
 164       Name_Len := N;
 165    end Get_Name;
 166
 167    --------------
 168    -- Skip_EOL --
 169    --------------
 170
 171    procedure Skip_EOL is
 172       C : Character;
 173
 174    begin
 175       loop
 176          Skipc;
 177          C := Nextc;
 178          exit when C /= LF and then C /= CR;
 179
 180          if C = ' ' then
 181             Skip_Spaces;
 182             C := Nextc;
 183             exit when C /= LF and then C /= CR;
 184          end if;
 185       end loop;
 186    end Skip_EOL;
 187
 188    -----------------
 189    -- Skip_Spaces --
 190    -----------------
 191
 192    procedure Skip_Spaces is
 193    begin
 194       while Nextc = ' ' loop
 195          Skipc;
 196       end loop;
 197    end Skip_Spaces;
 198
 199 --  Start of processing for Get_SPARK_Xrefs
 200
 201 begin
 202    Initialize_SPARK_Tables;
 203
 204    Cur_File      := 0;
 205    Cur_Scope     := 0;
 206    Cur_File_Idx  := 1;
 207    Cur_Scope_Idx := 0;
 208
 209    --  Loop through lines of SPARK cross-reference information
 210
 211    while Nextc = 'F' loop
 212       Skipc;
 213
 214       C := Getc;
 215
 216       --  Make sure first line is a File line
 217
 218       if SPARK_File_Table.Last = 0 and then C /= 'D' then
 219          raise Data_Error;
 220       end if;
 221
 222       --  Otherwise dispatch on type of line
 223
 224       case C is
 225
 226          --  Header entry for scope section
 227
 228          when 'D' =>
 229
 230             --  Complete previous entry if any
 231
 232             if SPARK_File_Table.Last /= 0 then
 233                SPARK_File_Table.Table (SPARK_File_Table.Last).To_Scope :=
 234                  SPARK_Scope_Table.Last;
 235             end if;
 236
 237             --  Scan out dependency number and file name
 238
 239             Skip_Spaces;
 240             Cur_File := Get_Nat;
 241             Skip_Spaces;
 242
 243             Get_Name;
 244             File_Name := new String'(Name_Str (1 .. Name_Len));
 245             Skip_Spaces;
 246
 247             --  Scan out unit file name when present (for subunits)
 248
 249             if Nextc = '-' then
 250                Skipc;
 251                Check ('>');
 252                Skip_Spaces;
 253                Get_Name;
 254                Unit_File_Name := new String'(Name_Str (1 .. Name_Len));
 255
 256             else
 257                Unit_File_Name := null;
 258             end if;
 259
 260             --  Make new File table entry (will fill in To_Scope later)
 261
 262             SPARK_File_Table.Append (
 263               (File_Name      => File_Name,
 264                Unit_File_Name => Unit_File_Name,
 265                File_Num       => Cur_File,
 266                From_Scope     => SPARK_Scope_Table.Last + 1,
 267                To_Scope       => 0));
 268
 269             --  Initialize counter for scopes
 270
 271             Cur_Scope := 1;
 272
 273          --  Scope entry
 274
 275          when 'S' =>
 276             declare
 277                Spec_File  : Nat;
 278                Spec_Scope : Nat;
 279                Scope      : Nat;
 280                Line       : Nat;
 281                Col        : Nat;
 282                Typ        : Character;
 283
 284             begin
 285                --  Scan out location
 286
 287                Skip_Spaces;
 288                Check ('.');
 289                Scope := Get_Nat;
 290                Check (' ');
 291                Line  := Get_Nat;
 292                Typ   := Getc;
 293                Col   := Get_Nat;
 294
 295                pragma Assert (Scope = Cur_Scope);
 296                pragma Assert         (Typ = 'K'
 297                               or else Typ = 'V'
 298                               or else Typ = 'U');
 299
 300                --  Scan out scope entity name
 301
 302                Skip_Spaces;
 303                Get_Name;
 304                Skip_Spaces;
 305
 306                if Nextc = '-' then
 307                   Skipc;
 308                   Check ('>');
 309                   Skip_Spaces;
 310                   Spec_File := Get_Nat;
 311                   Check ('.');
 312                   Spec_Scope := Get_Nat;
 313
 314                else
 315                   Spec_File  := 0;
 316                   Spec_Scope := 0;
 317                end if;
 318
 319                --  Make new scope table entry (will fill in From_Xref and
 320                --  To_Xref later). Initial range (From_Xref .. To_Xref) is
 321                --  empty for scopes without entities.
 322
 323                SPARK_Scope_Table.Append (
 324                  (Scope_Entity   => Empty,
 325                   Scope_Name     => new String'(Name_Str (1 .. Name_Len)),
 326                   File_Num       => Cur_File,
 327                   Scope_Num      => Cur_Scope,
 328                   Spec_File_Num  => Spec_File,
 329                   Spec_Scope_Num => Spec_Scope,
 330                   Line           => Line,
 331                   Stype          => Typ,
 332                   Col            => Col,
 333                   From_Xref      => 1,
 334                   To_Xref        => 0));
 335             end;
 336
 337             --  Update counter for scopes
 338
 339             Cur_Scope := Cur_Scope + 1;
 340
 341          --  Header entry for cross-ref section
 342
 343          when 'X' =>
 344
 345             --  Scan out dependency number and file name (ignored)
 346
 347             Skip_Spaces;
 348             Cur_File := Get_Nat;
 349             Skip_Spaces;
 350             Get_Name;
 351
 352             --  Update component From_Xref of current file if first reference
 353             --  in this file.
 354
 355             while SPARK_File_Table.Table (Cur_File_Idx).File_Num /= Cur_File
 356             loop
 357                Cur_File_Idx := Cur_File_Idx + 1;
 358             end loop;
 359
 360             --  Scan out scope entity number and entity name (ignored)
 361
 362             Skip_Spaces;
 363             Check ('.');
 364             Cur_Scope := Get_Nat;
 365             Skip_Spaces;
 366             Get_Name;
 367
 368             --  Update component To_Xref of previous scope
 369
 370             if Cur_Scope_Idx /= 0 then
 371                SPARK_Scope_Table.Table (Cur_Scope_Idx).To_Xref :=
 372                  SPARK_Xref_Table.Last;
 373             end if;
 374
 375             --  Update component From_Xref of current scope
 376
 377             Cur_Scope_Idx := SPARK_File_Table.Table (Cur_File_Idx).From_Scope;
 378
 379             while SPARK_Scope_Table.Table (Cur_Scope_Idx).Scope_Num /=
 380               Cur_Scope
 381             loop
 382                Cur_Scope_Idx := Cur_Scope_Idx + 1;
 383             end loop;
 384
 385             SPARK_Scope_Table.Table (Cur_Scope_Idx).From_Xref :=
 386               SPARK_Xref_Table.Last + 1;
 387
 388          --  Cross reference entry
 389
 390          when ' ' =>
 391             declare
 392                XR_Entity      : String_Ptr;
 393                XR_Entity_Line : Nat;
 394                XR_Entity_Col  : Nat;
 395                XR_Entity_Typ  : Character;
 396
 397                XR_File : Nat;
 398                --  Keeps track of the current file (changed by nn|)
 399
 400                XR_Scope : Nat;
 401                --  Keeps track of the current scope (changed by nn:)
 402
 403             begin
 404                XR_File  := Cur_File;
 405                XR_Scope := Cur_Scope;
 406
 407                XR_Entity_Line := Get_Nat;
 408                XR_Entity_Typ  := Getc;
 409                XR_Entity_Col  := Get_Nat;
 410
 411                Skip_Spaces;
 412                Get_Name;
 413                XR_Entity := new String'(Name_Str (1 .. Name_Len));
 414
 415                --  Initialize to scan items on one line
 416
 417                Skip_Spaces;
 418
 419                --  Loop through cross-references for this entity
 420
 421                loop
 422
 423                   declare
 424                      Line  : Nat;
 425                      Col   : Nat;
 426                      N     : Nat;
 427                      Rtype : Character;
 428
 429                   begin
 430                      Skip_Spaces;
 431
 432                      if At_EOL then
 433                         Skip_EOL;
 434                         exit when Nextc /= '.';
 435                         Skipc;
 436                         Skip_Spaces;
 437                      end if;
 438
 439                      if Nextc = '.' then
 440                         Skipc;
 441                         XR_Scope := Get_Nat;
 442                         Check (':');
 443
 444                      else
 445                         N := Get_Nat;
 446
 447                         if Nextc = '|' then
 448                            XR_File := N;
 449                            Skipc;
 450
 451                         else
 452                            Line  := N;
 453                            Rtype := Getc;
 454                            Col   := Get_Nat;
 455
 456                            pragma Assert
 457                              (Rtype = 'r' or else
 458                               Rtype = 'c' or else
 459                               Rtype = 'm' or else
 460                               Rtype = 's');
 461
 462                            SPARK_Xref_Table.Append (
 463                              (Entity_Name => XR_Entity,
 464                               Entity_Line => XR_Entity_Line,
 465                               Etype       => XR_Entity_Typ,
 466                               Entity_Col  => XR_Entity_Col,
 467                               File_Num    => XR_File,
 468                               Scope_Num   => XR_Scope,
 469                               Line        => Line,
 470                               Rtype       => Rtype,
 471                               Col         => Col));
 472                         end if;
 473                      end if;
 474                   end;
 475                end loop;
 476             end;
 477
 478          --  No other SPARK lines are possible
 479
 480          when others =>
 481             raise Data_Error;
 482       end case;
 483
 484       --  For cross reference lines, the EOL character has been skipped already
 485
 486       if C /= ' ' then
 487          Skip_EOL;
 488       end if;
 489    end loop;
 490
 491    --  Here with all Xrefs stored, complete last entries in File/Scope tables
 492
 493    if SPARK_File_Table.Last /= 0 then
 494       SPARK_File_Table.Table (SPARK_File_Table.Last).To_Scope :=
 495         SPARK_Scope_Table.Last;
 496    end if;
 497
 498    if Cur_Scope_Idx /= 0 then
 499       SPARK_Scope_Table.Table (Cur_Scope_Idx).To_Xref := SPARK_Xref_Table.Last;
 500    end if;
 501 end Get_SPARK_Xrefs;