blob: f200e21327075351e2d475cf52e2eeddcd7a685a [file] [log] [blame]
------------------------------------------------------------------------------
-- --
-- GNAT COMPILER COMPONENTS --
-- --
-- P U 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;
procedure Put_SPARK_Xrefs is
begin
-- Loop through entries in SPARK_File_Table
for J in 1 .. SPARK_File_Table.Last loop
declare
F : SPARK_File_Record renames SPARK_File_Table.Table (J);
Start : Scope_Index;
Stop : Scope_Index;
begin
Start := F.From_Scope;
Stop := F.To_Scope;
Write_Info_Initiate ('F');
Write_Info_Char ('D');
Write_Info_Char (' ');
Write_Info_Nat (F.File_Num);
Write_Info_Char (' ');
for N in F.File_Name'Range loop
Write_Info_Char (F.File_Name (N));
end loop;
-- If file is a subunit, print the file name for the unit
if F.Unit_File_Name /= null then
Write_Info_Char (' ');
Write_Info_Char ('-');
Write_Info_Char ('>');
Write_Info_Char (' ');
for N in F.Unit_File_Name'Range loop
Write_Info_Char (F.Unit_File_Name (N));
end loop;
end if;
Write_Info_Terminate;
-- Loop through scope entries for this file
loop
exit when Start = Stop + 1;
pragma Assert (Start <= Stop);
declare
S : SPARK_Scope_Record renames SPARK_Scope_Table.Table (Start);
begin
Write_Info_Initiate ('F');
Write_Info_Char ('S');
Write_Info_Char (' ');
Write_Info_Char ('.');
Write_Info_Nat (S.Scope_Num);
Write_Info_Char (' ');
Write_Info_Nat (S.Line);
Write_Info_Char (S.Stype);
Write_Info_Nat (S.Col);
Write_Info_Char (' ');
pragma Assert (S.Scope_Name.all /= "");
for N in S.Scope_Name'Range loop
Write_Info_Char (S.Scope_Name (N));
end loop;
if S.Spec_File_Num /= 0 then
Write_Info_Char (' ');
Write_Info_Char ('-');
Write_Info_Char ('>');
Write_Info_Char (' ');
Write_Info_Nat (S.Spec_File_Num);
Write_Info_Char ('.');
Write_Info_Nat (S.Spec_Scope_Num);
end if;
Write_Info_Terminate;
end;
Start := Start + 1;
end loop;
end;
end loop;
-- Loop through entries in SPARK_File_Table
for J in 1 .. SPARK_File_Table.Last loop
declare
F : SPARK_File_Record renames SPARK_File_Table.Table (J);
Start : Scope_Index;
Stop : Scope_Index;
File : Nat;
Scope : Nat;
Entity_Line : Nat;
Entity_Col : Nat;
begin
Start := F.From_Scope;
Stop := F.To_Scope;
-- Loop through scope entries for this file
loop
exit when Start = Stop + 1;
pragma Assert (Start <= Stop);
Output_One_Scope : declare
S : SPARK_Scope_Record renames SPARK_Scope_Table.Table (Start);
XStart : Xref_Index;
XStop : Xref_Index;
begin
XStart := S.From_Xref;
XStop := S.To_Xref;
if XStart > XStop then
goto Continue;
end if;
Write_Info_Initiate ('F');
Write_Info_Char ('X');
Write_Info_Char (' ');
Write_Info_Nat (F.File_Num);
Write_Info_Char (' ');
for N in F.File_Name'Range loop
Write_Info_Char (F.File_Name (N));
end loop;
Write_Info_Char (' ');
Write_Info_Char ('.');
Write_Info_Nat (S.Scope_Num);
Write_Info_Char (' ');
for N in S.Scope_Name'Range loop
Write_Info_Char (S.Scope_Name (N));
end loop;
-- Default value of (0,0) is used for the special __HEAP
-- variable so use another default value.
Entity_Line := 0;
Entity_Col := 1;
-- Loop through cross reference entries for this scope
loop
exit when XStart = XStop + 1;
pragma Assert (XStart <= XStop);
Output_One_Xref : declare
R : SPARK_Xref_Record renames
SPARK_Xref_Table.Table (XStart);
begin
if R.Entity_Line /= Entity_Line
or else R.Entity_Col /= Entity_Col
then
Write_Info_Terminate;
Write_Info_Initiate ('F');
Write_Info_Char (' ');
Write_Info_Nat (R.Entity_Line);
Write_Info_Char (R.Etype);
Write_Info_Nat (R.Entity_Col);
Write_Info_Char (' ');
for N in R.Entity_Name'Range loop
Write_Info_Char (R.Entity_Name (N));
end loop;
Entity_Line := R.Entity_Line;
Entity_Col := R.Entity_Col;
File := F.File_Num;
Scope := S.Scope_Num;
end if;
if Write_Info_Col > 72 then
Write_Info_Terminate;
Write_Info_Initiate ('.');
end if;
Write_Info_Char (' ');
if R.File_Num /= File then
Write_Info_Nat (R.File_Num);
Write_Info_Char ('|');
File := R.File_Num;
Scope := 0;
end if;
if R.Scope_Num /= Scope then
Write_Info_Char ('.');
Write_Info_Nat (R.Scope_Num);
Write_Info_Char (':');
Scope := R.Scope_Num;
end if;
Write_Info_Nat (R.Line);
Write_Info_Char (R.Rtype);
Write_Info_Nat (R.Col);
end Output_One_Xref;
XStart := XStart + 1;
end loop;
Write_Info_Terminate;
end Output_One_Scope;
<<Continue>>
Start := Start + 1;
end loop;
end;
end loop;
end Put_SPARK_Xrefs;