| ------------------------------------------------------------------------------ |
| -- -- |
| -- 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; |
