aboutsummaryrefslogtreecommitdiffstats
path: root/gcc-4.9/gcc/ada/get_spark_xrefs.adb
diff options
context:
space:
mode:
Diffstat (limited to 'gcc-4.9/gcc/ada/get_spark_xrefs.adb')
-rw-r--r--gcc-4.9/gcc/ada/get_spark_xrefs.adb501
1 files changed, 501 insertions, 0 deletions
diff --git a/gcc-4.9/gcc/ada/get_spark_xrefs.adb b/gcc-4.9/gcc/ada/get_spark_xrefs.adb
new file mode 100644
index 000000000..ea1f1b45a
--- /dev/null
+++ b/gcc-4.9/gcc/ada/get_spark_xrefs.adb
@@ -0,0 +1,501 @@
+------------------------------------------------------------------------------
+-- --
+-- GNAT COMPILER COMPONENTS --
+-- --
+-- G E T _ S P A R K _ X R E F S --
+-- --
+-- B o d y --
+-- --
+-- Copyright (C) 2011-2013, 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. --
+-- --
+------------------------------------------------------------------------------
+
+with SPARK_Xrefs; use SPARK_Xrefs;
+with Types; use Types;
+
+with Ada.IO_Exceptions; use Ada.IO_Exceptions;
+
+procedure Get_SPARK_Xrefs is
+ C : Character;
+
+ use ASCII;
+ -- For CR/LF
+
+ Cur_File : Nat;
+ -- Dependency number for the current file
+
+ Cur_Scope : Nat;
+ -- Scope number for the current scope entity
+
+ Cur_File_Idx : File_Index;
+ -- Index in SPARK_File_Table of the current file
+
+ Cur_Scope_Idx : Scope_Index;
+ -- Index in SPARK_Scope_Table of the current scope
+
+ Name_Str : String (1 .. 32768);
+ Name_Len : Natural := 0;
+ -- Local string used to store name of File/entity scanned as
+ -- Name_Str (1 .. Name_Len).
+
+ File_Name : String_Ptr;
+ Unit_File_Name : String_Ptr;
+
+ -----------------------
+ -- Local Subprograms --
+ -----------------------
+
+ function At_EOL return Boolean;
+ -- Skips any spaces, then checks if at the end of a line. If so, returns
+ -- True (but does not skip the EOL sequence). If not, then returns False.
+
+ procedure Check (C : Character);
+ -- Checks that file is positioned at given character, and if so skips past
+ -- it, If not, raises Data_Error.
+
+ function Get_Nat return Nat;
+ -- On entry the file is positioned to a digit. On return, the file is
+ -- positioned past the last digit, and the returned result is the decimal
+ -- value read. Data_Error is raised for overflow (value greater than
+ -- Int'Last), or if the initial character is not a digit.
+
+ procedure Get_Name;
+ -- On entry the file is positioned to a name. On return, the file is
+ -- positioned past the last character, and the name scanned is returned
+ -- in Name_Str (1 .. Name_Len).
+
+ procedure Skip_EOL;
+ -- Called with the current character about to be read being LF or CR. Skips
+ -- past CR/LF characters until either a non-CR/LF character is found, or
+ -- the end of file is encountered.
+
+ procedure Skip_Spaces;
+ -- Skips zero or more spaces at the current position, leaving the file
+ -- positioned at the first non-blank character (or Types.EOF).
+
+ ------------
+ -- At_EOL --
+ ------------
+
+ function At_EOL return Boolean is
+ begin
+ Skip_Spaces;
+ return Nextc = CR or else Nextc = LF;
+ end At_EOL;
+
+ -----------
+ -- Check --
+ -----------
+
+ procedure Check (C : Character) is
+ begin
+ if Nextc = C then
+ Skipc;
+ else
+ raise Data_Error;
+ end if;
+ end Check;
+
+ -------------
+ -- Get_Nat --
+ -------------
+
+ function Get_Nat return Nat is
+ Val : Nat;
+ C : Character;
+
+ begin
+ C := Nextc;
+ Val := 0;
+
+ if C not in '0' .. '9' then
+ raise Data_Error;
+ end if;
+
+ -- Loop to read digits of integer value
+
+ loop
+ declare
+ pragma Unsuppress (Overflow_Check);
+ begin
+ Val := Val * 10 + (Character'Pos (C) - Character'Pos ('0'));
+ end;
+
+ Skipc;
+ C := Nextc;
+
+ exit when C not in '0' .. '9';
+ end loop;
+
+ return Val;
+
+ exception
+ when Constraint_Error =>
+ raise Data_Error;
+ end Get_Nat;
+
+ --------------
+ -- Get_Name --
+ --------------
+
+ procedure Get_Name is
+ N : Integer;
+
+ begin
+ N := 0;
+ while Nextc > ' ' loop
+ N := N + 1;
+ Name_Str (N) := Getc;
+ end loop;
+
+ Name_Len := N;
+ end Get_Name;
+
+ --------------
+ -- Skip_EOL --
+ --------------
+
+ procedure Skip_EOL is
+ C : Character;
+
+ begin
+ loop
+ Skipc;
+ C := Nextc;
+ exit when C /= LF and then C /= CR;
+
+ if C = ' ' then
+ Skip_Spaces;
+ C := Nextc;
+ exit when C /= LF and then C /= CR;
+ end if;
+ end loop;
+ end Skip_EOL;
+
+ -----------------
+ -- Skip_Spaces --
+ -----------------
+
+ procedure Skip_Spaces is
+ begin
+ while Nextc = ' ' loop
+ Skipc;
+ end loop;
+ end Skip_Spaces;
+
+-- Start of processing for Get_SPARK_Xrefs
+
+begin
+ Initialize_SPARK_Tables;
+
+ Cur_File := 0;
+ Cur_Scope := 0;
+ Cur_File_Idx := 1;
+ Cur_Scope_Idx := 0;
+
+ -- Loop through lines of SPARK cross-reference information
+
+ while Nextc = 'F' loop
+ Skipc;
+
+ C := Getc;
+
+ -- Make sure first line is a File line
+
+ if SPARK_File_Table.Last = 0 and then C /= 'D' then
+ raise Data_Error;
+ end if;
+
+ -- Otherwise dispatch on type of line
+
+ case C is
+
+ -- Header entry for scope section
+
+ when 'D' =>
+
+ -- Complete previous entry if any
+
+ if SPARK_File_Table.Last /= 0 then
+ SPARK_File_Table.Table (SPARK_File_Table.Last).To_Scope :=
+ SPARK_Scope_Table.Last;
+ end if;
+
+ -- Scan out dependency number and file name
+
+ Skip_Spaces;
+ Cur_File := Get_Nat;
+ Skip_Spaces;
+
+ Get_Name;
+ File_Name := new String'(Name_Str (1 .. Name_Len));
+ Skip_Spaces;
+
+ -- Scan out unit file name when present (for subunits)
+
+ if Nextc = '-' then
+ Skipc;
+ Check ('>');
+ Skip_Spaces;
+ Get_Name;
+ Unit_File_Name := new String'(Name_Str (1 .. Name_Len));
+
+ else
+ Unit_File_Name := null;
+ end if;
+
+ -- Make new File table entry (will fill in To_Scope later)
+
+ SPARK_File_Table.Append (
+ (File_Name => File_Name,
+ Unit_File_Name => Unit_File_Name,
+ File_Num => Cur_File,
+ From_Scope => SPARK_Scope_Table.Last + 1,
+ To_Scope => 0));
+
+ -- Initialize counter for scopes
+
+ Cur_Scope := 1;
+
+ -- Scope entry
+
+ when 'S' =>
+ declare
+ Spec_File : Nat;
+ Spec_Scope : Nat;
+ Scope : Nat;
+ Line : Nat;
+ Col : Nat;
+ Typ : Character;
+
+ begin
+ -- Scan out location
+
+ Skip_Spaces;
+ Check ('.');
+ Scope := Get_Nat;
+ Check (' ');
+ Line := Get_Nat;
+ Typ := Getc;
+ Col := Get_Nat;
+
+ pragma Assert (Scope = Cur_Scope);
+ pragma Assert (Typ = 'K'
+ or else Typ = 'V'
+ or else Typ = 'U');
+
+ -- Scan out scope entity name
+
+ Skip_Spaces;
+ Get_Name;
+ Skip_Spaces;
+
+ if Nextc = '-' then
+ Skipc;
+ Check ('>');
+ Skip_Spaces;
+ Spec_File := Get_Nat;
+ Check ('.');
+ Spec_Scope := Get_Nat;
+
+ else
+ Spec_File := 0;
+ Spec_Scope := 0;
+ end if;
+
+ -- Make new scope table entry (will fill in From_Xref and
+ -- To_Xref later). Initial range (From_Xref .. To_Xref) is
+ -- empty for scopes without entities.
+
+ SPARK_Scope_Table.Append (
+ (Scope_Entity => Empty,
+ Scope_Name => new String'(Name_Str (1 .. Name_Len)),
+ File_Num => Cur_File,
+ Scope_Num => Cur_Scope,
+ Spec_File_Num => Spec_File,
+ Spec_Scope_Num => Spec_Scope,
+ Line => Line,
+ Stype => Typ,
+ Col => Col,
+ From_Xref => 1,
+ To_Xref => 0));
+ end;
+
+ -- Update counter for scopes
+
+ Cur_Scope := Cur_Scope + 1;
+
+ -- Header entry for cross-ref section
+
+ when 'X' =>
+
+ -- Scan out dependency number and file name (ignored)
+
+ Skip_Spaces;
+ Cur_File := Get_Nat;
+ Skip_Spaces;
+ Get_Name;
+
+ -- Update component From_Xref of current file if first reference
+ -- in this file.
+
+ while SPARK_File_Table.Table (Cur_File_Idx).File_Num /= Cur_File
+ loop
+ Cur_File_Idx := Cur_File_Idx + 1;
+ end loop;
+
+ -- Scan out scope entity number and entity name (ignored)
+
+ Skip_Spaces;
+ Check ('.');
+ Cur_Scope := Get_Nat;
+ Skip_Spaces;
+ Get_Name;
+
+ -- Update component To_Xref of previous scope
+
+ if Cur_Scope_Idx /= 0 then
+ SPARK_Scope_Table.Table (Cur_Scope_Idx).To_Xref :=
+ SPARK_Xref_Table.Last;
+ end if;
+
+ -- Update component From_Xref of current scope
+
+ Cur_Scope_Idx := SPARK_File_Table.Table (Cur_File_Idx).From_Scope;
+
+ while SPARK_Scope_Table.Table (Cur_Scope_Idx).Scope_Num /=
+ Cur_Scope
+ loop
+ Cur_Scope_Idx := Cur_Scope_Idx + 1;
+ end loop;
+
+ SPARK_Scope_Table.Table (Cur_Scope_Idx).From_Xref :=
+ SPARK_Xref_Table.Last + 1;
+
+ -- Cross reference entry
+
+ when ' ' =>
+ declare
+ XR_Entity : String_Ptr;
+ XR_Entity_Line : Nat;
+ XR_Entity_Col : Nat;
+ XR_Entity_Typ : Character;
+
+ XR_File : Nat;
+ -- Keeps track of the current file (changed by nn|)
+
+ XR_Scope : Nat;
+ -- Keeps track of the current scope (changed by nn:)
+
+ begin
+ XR_File := Cur_File;
+ XR_Scope := Cur_Scope;
+
+ XR_Entity_Line := Get_Nat;
+ XR_Entity_Typ := Getc;
+ XR_Entity_Col := Get_Nat;
+
+ Skip_Spaces;
+ Get_Name;
+ XR_Entity := new String'(Name_Str (1 .. Name_Len));
+
+ -- Initialize to scan items on one line
+
+ Skip_Spaces;
+
+ -- Loop through cross-references for this entity
+
+ loop
+
+ declare
+ Line : Nat;
+ Col : Nat;
+ N : Nat;
+ Rtype : Character;
+
+ begin
+ Skip_Spaces;
+
+ if At_EOL then
+ Skip_EOL;
+ exit when Nextc /= '.';
+ Skipc;
+ Skip_Spaces;
+ end if;
+
+ if Nextc = '.' then
+ Skipc;
+ XR_Scope := Get_Nat;
+ Check (':');
+
+ else
+ N := Get_Nat;
+
+ if Nextc = '|' then
+ XR_File := N;
+ Skipc;
+
+ else
+ Line := N;
+ Rtype := Getc;
+ Col := Get_Nat;
+
+ pragma Assert
+ (Rtype = 'r' or else
+ Rtype = 'c' or else
+ Rtype = 'm' or else
+ Rtype = 's');
+
+ SPARK_Xref_Table.Append (
+ (Entity_Name => XR_Entity,
+ Entity_Line => XR_Entity_Line,
+ Etype => XR_Entity_Typ,
+ Entity_Col => XR_Entity_Col,
+ File_Num => XR_File,
+ Scope_Num => XR_Scope,
+ Line => Line,
+ Rtype => Rtype,
+ Col => Col));
+ end if;
+ end if;
+ end;
+ end loop;
+ end;
+
+ -- No other SPARK lines are possible
+
+ when others =>
+ raise Data_Error;
+ end case;
+
+ -- For cross reference lines, the EOL character has been skipped already
+
+ if C /= ' ' then
+ Skip_EOL;
+ end if;
+ end loop;
+
+ -- Here with all Xrefs stored, complete last entries in File/Scope tables
+
+ if SPARK_File_Table.Last /= 0 then
+ SPARK_File_Table.Table (SPARK_File_Table.Last).To_Scope :=
+ SPARK_Scope_Table.Last;
+ end if;
+
+ if Cur_Scope_Idx /= 0 then
+ SPARK_Scope_Table.Table (Cur_Scope_Idx).To_Xref := SPARK_Xref_Table.Last;
+ end if;
+end Get_SPARK_Xrefs;
generated by cgit v1.2.3 (git 2.25.1) at 2024-04-18 07:28:47 +0000