aboutsummaryrefslogtreecommitdiffstats
path: root/gcc-4.9/gcc/ada/put_spark_xrefs.adb
diff options
context:
space:
mode:
Diffstat (limited to 'gcc-4.9/gcc/ada/put_spark_xrefs.adb')
-rw-r--r--gcc-4.9/gcc/ada/put_spark_xrefs.adb243
1 files changed, 243 insertions, 0 deletions
diff --git a/gcc-4.9/gcc/ada/put_spark_xrefs.adb b/gcc-4.9/gcc/ada/put_spark_xrefs.adb
new file mode 100644
index 000000000..f200e2132
--- /dev/null
+++ b/gcc-4.9/gcc/ada/put_spark_xrefs.adb
@@ -0,0 +1,243 @@
+------------------------------------------------------------------------------
+-- --
+-- 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;