blob: ea1f1b45a0baa5ab3e74185b80bd67958d2a9737 [file] [log] [blame]
------------------------------------------------------------------------------
-- --
-- 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;