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