File : put_spark_xrefs.adb
1 ------------------------------------------------------------------------------
2 -- --
3 -- GNAT COMPILER COMPONENTS --
4 -- --
5 -- P U T _ S P A R K _ X R E F S --
6 -- --
7 -- B o d y --
8 -- --
9 -- Copyright (C) 2011-2016, Free Software Foundation, Inc. --
10 -- --
11 -- GNAT is free software; you can redistribute it and/or modify it under --
12 -- terms of the GNU General Public License as published by the Free Soft- --
13 -- ware Foundation; either version 3, or (at your option) any later ver- --
14 -- sion. GNAT is distributed in the hope that it will be useful, but WITH- --
15 -- OUT ANY WARRANTY; without even the implied warranty of MERCHANTABILITY --
16 -- or FITNESS FOR A PARTICULAR PURPOSE. See the GNU General Public License --
17 -- for more details. You should have received a copy of the GNU General --
18 -- Public License distributed with GNAT; see file COPYING3. If not, go to --
19 -- http://www.gnu.org/licenses for a complete copy of the license. --
20 -- --
21 -- GNAT was originally developed by the GNAT team at New York University. --
22 -- Extensive contributions were provided by Ada Core Technologies Inc. --
23 -- --
24 ------------------------------------------------------------------------------
25
26 with SPARK_Xrefs; use SPARK_Xrefs;
27
28 procedure Put_SPARK_Xrefs is
29 begin
30 -- Loop through entries in SPARK_File_Table
31
32 for J in 1 .. SPARK_File_Table.Last loop
33 declare
34 F : SPARK_File_Record renames SPARK_File_Table.Table (J);
35
36 begin
37 Write_Info_Initiate ('F');
38 Write_Info_Char ('D');
39 Write_Info_Char (' ');
40 Write_Info_Nat (F.File_Num);
41 Write_Info_Char (' ');
42
43 Write_Info_Str (F.File_Name.all);
44
45 -- If file is a subunit, print the file name for the unit
46
47 if F.Unit_File_Name /= null then
48 Write_Info_Str (" -> " & F.Unit_File_Name.all);
49 end if;
50
51 Write_Info_Terminate;
52
53 -- Loop through scope entries for this file
54
55 for J in F.From_Scope .. F.To_Scope loop
56 declare
57 S : SPARK_Scope_Record renames SPARK_Scope_Table.Table (J);
58
59 begin
60 Write_Info_Initiate ('F');
61 Write_Info_Char ('S');
62 Write_Info_Char (' ');
63 Write_Info_Char ('.');
64 Write_Info_Nat (S.Scope_Num);
65 Write_Info_Char (' ');
66 Write_Info_Nat (S.Line);
67 Write_Info_Char (S.Stype);
68 Write_Info_Nat (S.Col);
69 Write_Info_Char (' ');
70
71 pragma Assert (S.Scope_Name.all /= "");
72
73 Write_Info_Str (S.Scope_Name.all);
74
75 if S.Spec_File_Num /= 0 then
76 Write_Info_Str (" -> ");
77 Write_Info_Nat (S.Spec_File_Num);
78 Write_Info_Char ('.');
79 Write_Info_Nat (S.Spec_Scope_Num);
80 end if;
81
82 Write_Info_Terminate;
83 end;
84 end loop;
85 end;
86 end loop;
87
88 -- Loop through entries in SPARK_File_Table
89
90 for J in 1 .. SPARK_File_Table.Last loop
91 declare
92 F : SPARK_File_Record renames SPARK_File_Table.Table (J);
93 File : Nat;
94 Scope : Nat;
95 Entity_Line : Nat;
96 Entity_Col : Nat;
97
98 begin
99 -- Loop through scope entries for this file
100
101 for K in F.From_Scope .. F.To_Scope loop
102 Output_One_Scope : declare
103 S : SPARK_Scope_Record renames SPARK_Scope_Table.Table (K);
104
105 begin
106 -- Write only non-empty tables
107
108 if S.From_Xref <= S.To_Xref then
109
110 Write_Info_Initiate ('F');
111 Write_Info_Char ('X');
112 Write_Info_Char (' ');
113 Write_Info_Nat (F.File_Num);
114 Write_Info_Char (' ');
115
116 Write_Info_Str (F.File_Name.all);
117
118 Write_Info_Char (' ');
119 Write_Info_Char ('.');
120 Write_Info_Nat (S.Scope_Num);
121 Write_Info_Char (' ');
122
123 Write_Info_Str (S.Scope_Name.all);
124
125 -- Default value of (0,0) is used for the special __HEAP
126 -- variable so use another default value.
127
128 Entity_Line := 0;
129 Entity_Col := 1;
130
131 -- Loop through cross reference entries for this scope
132
133 for X in S.From_Xref .. S.To_Xref loop
134
135 Output_One_Xref : declare
136 R : SPARK_Xref_Record renames
137 SPARK_Xref_Table.Table (X);
138
139 begin
140 if R.Entity_Line /= Entity_Line
141 or else R.Entity_Col /= Entity_Col
142 then
143 Write_Info_Terminate;
144
145 Write_Info_Initiate ('F');
146 Write_Info_Char (' ');
147 Write_Info_Nat (R.Entity_Line);
148 Write_Info_Char (R.Etype);
149 Write_Info_Nat (R.Entity_Col);
150 Write_Info_Char (' ');
151
152 Write_Info_Str (R.Entity_Name.all);
153
154 Entity_Line := R.Entity_Line;
155 Entity_Col := R.Entity_Col;
156 File := F.File_Num;
157 Scope := S.Scope_Num;
158 end if;
159
160 if Write_Info_Col > 72 then
161 Write_Info_Terminate;
162 Write_Info_Initiate ('.');
163 end if;
164
165 Write_Info_Char (' ');
166
167 if R.File_Num /= File then
168 Write_Info_Nat (R.File_Num);
169 Write_Info_Char ('|');
170 File := R.File_Num;
171 Scope := 0;
172 end if;
173
174 if R.Scope_Num /= Scope then
175 Write_Info_Char ('.');
176 Write_Info_Nat (R.Scope_Num);
177 Write_Info_Char (':');
178 Scope := R.Scope_Num;
179 end if;
180
181 Write_Info_Nat (R.Line);
182 Write_Info_Char (R.Rtype);
183 Write_Info_Nat (R.Col);
184 end Output_One_Xref;
185
186 end loop;
187
188 Write_Info_Terminate;
189 end if;
190 end Output_One_Scope;
191 end loop;
192 end;
193 end loop;
194 end Put_SPARK_Xrefs;