File : get_spark_xrefs.adb
1 ------------------------------------------------------------------------------
2 -- --
3 -- GNAT COMPILER COMPONENTS --
4 -- --
5 -- G E 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 with Types; use Types;
28
29 with Ada.IO_Exceptions; use Ada.IO_Exceptions;
30
31 procedure Get_SPARK_Xrefs is
32 C : Character;
33
34 use ASCII;
35 -- For CR/LF
36
37 Cur_File : Nat;
38 -- Dependency number for the current file
39
40 Cur_Scope : Nat;
41 -- Scope number for the current scope entity
42
43 Cur_File_Idx : File_Index;
44 -- Index in SPARK_File_Table of the current file
45
46 Cur_Scope_Idx : Scope_Index;
47 -- Index in SPARK_Scope_Table of the current scope
48
49 Name_Str : String (1 .. 32768);
50 Name_Len : Natural := 0;
51 -- Local string used to store name of File/entity scanned as
52 -- Name_Str (1 .. Name_Len).
53
54 File_Name : String_Ptr;
55 Unit_File_Name : String_Ptr;
56
57 -----------------------
58 -- Local Subprograms --
59 -----------------------
60
61 function At_EOL return Boolean;
62 -- Skips any spaces, then checks if at the end of a line. If so, returns
63 -- True (but does not skip the EOL sequence). If not, then returns False.
64
65 procedure Check (C : Character);
66 -- Checks that file is positioned at given character, and if so skips past
67 -- it, If not, raises Data_Error.
68
69 function Get_Nat return Nat;
70 -- On entry the file is positioned to a digit. On return, the file is
71 -- positioned past the last digit, and the returned result is the decimal
72 -- value read. Data_Error is raised for overflow (value greater than
73 -- Int'Last), or if the initial character is not a digit.
74
75 procedure Get_Name;
76 -- On entry the file is positioned to a name. On return, the file is
77 -- positioned past the last character, and the name scanned is returned
78 -- in Name_Str (1 .. Name_Len).
79
80 procedure Skip_EOL;
81 -- Called with the current character about to be read being LF or CR. Skips
82 -- past CR/LF characters until either a non-CR/LF character is found, or
83 -- the end of file is encountered.
84
85 procedure Skip_Spaces;
86 -- Skips zero or more spaces at the current position, leaving the file
87 -- positioned at the first non-blank character (or Types.EOF).
88
89 ------------
90 -- At_EOL --
91 ------------
92
93 function At_EOL return Boolean is
94 begin
95 Skip_Spaces;
96 return Nextc = CR or else Nextc = LF;
97 end At_EOL;
98
99 -----------
100 -- Check --
101 -----------
102
103 procedure Check (C : Character) is
104 begin
105 if Nextc = C then
106 Skipc;
107 else
108 raise Data_Error;
109 end if;
110 end Check;
111
112 -------------
113 -- Get_Nat --
114 -------------
115
116 function Get_Nat return Nat is
117 C : Character := Nextc;
118 Val : Nat := 0;
119
120 begin
121 if C not in '0' .. '9' then
122 raise Data_Error;
123 end if;
124
125 -- Loop to read digits of integer value
126
127 loop
128 declare
129 pragma Unsuppress (Overflow_Check);
130 begin
131 Val := Val * 10 + (Character'Pos (C) - Character'Pos ('0'));
132 end;
133
134 Skipc;
135 C := Nextc;
136
137 exit when C not in '0' .. '9';
138 end loop;
139
140 return Val;
141
142 exception
143 when Constraint_Error =>
144 raise Data_Error;
145 end Get_Nat;
146
147 --------------
148 -- Get_Name --
149 --------------
150
151 procedure Get_Name is
152 N : Natural := 0;
153
154 begin
155 while Nextc > ' ' loop
156 N := N + 1;
157 Name_Str (N) := Getc;
158 end loop;
159
160 Name_Len := N;
161 end Get_Name;
162
163 --------------
164 -- Skip_EOL --
165 --------------
166
167 procedure Skip_EOL is
168 C : Character;
169
170 begin
171 loop
172 Skipc;
173 C := Nextc;
174 exit when C /= LF and then C /= CR;
175
176 if C = ' ' then
177 Skip_Spaces;
178 C := Nextc;
179 exit when C /= LF and then C /= CR;
180 end if;
181 end loop;
182 end Skip_EOL;
183
184 -----------------
185 -- Skip_Spaces --
186 -----------------
187
188 procedure Skip_Spaces is
189 begin
190 while Nextc = ' ' loop
191 Skipc;
192 end loop;
193 end Skip_Spaces;
194
195 -- Start of processing for Get_SPARK_Xrefs
196
197 begin
198 Initialize_SPARK_Tables;
199
200 Cur_File := 0;
201 Cur_Scope := 0;
202 Cur_File_Idx := 1;
203 Cur_Scope_Idx := 0;
204
205 -- Loop through lines of SPARK cross-reference information
206
207 while Nextc = 'F' loop
208 Skipc;
209
210 C := Getc;
211
212 -- Make sure first line is a File line
213
214 if SPARK_File_Table.Last = 0 and then C /= 'D' then
215 raise Data_Error;
216 end if;
217
218 -- Otherwise dispatch on type of line
219
220 case C is
221
222 -- Header entry for scope section
223
224 when 'D' =>
225
226 -- Complete previous entry if any
227
228 if SPARK_File_Table.Last /= 0 then
229 SPARK_File_Table.Table (SPARK_File_Table.Last).To_Scope :=
230 SPARK_Scope_Table.Last;
231 end if;
232
233 -- Scan out dependency number and file name
234
235 Skip_Spaces;
236 Cur_File := Get_Nat;
237 Skip_Spaces;
238
239 Get_Name;
240 File_Name := new String'(Name_Str (1 .. Name_Len));
241 Skip_Spaces;
242
243 -- Scan out unit file name when present (for subunits)
244
245 if Nextc = '-' then
246 Skipc;
247 Check ('>');
248 Skip_Spaces;
249 Get_Name;
250 Unit_File_Name := new String'(Name_Str (1 .. Name_Len));
251
252 else
253 Unit_File_Name := null;
254 end if;
255
256 -- Make new File table entry (will fill in To_Scope later)
257
258 SPARK_File_Table.Append (
259 (File_Name => File_Name,
260 Unit_File_Name => Unit_File_Name,
261 File_Num => Cur_File,
262 From_Scope => SPARK_Scope_Table.Last + 1,
263 To_Scope => 0));
264
265 -- Initialize counter for scopes
266
267 Cur_Scope := 1;
268
269 -- Scope entry
270
271 when 'S' =>
272 declare
273 Spec_File : Nat;
274 Spec_Scope : Nat;
275 Scope : Nat;
276 Line : Nat;
277 Col : Nat;
278 Typ : Character;
279
280 begin
281 -- Scan out location
282
283 Skip_Spaces;
284 Check ('.');
285 Scope := Get_Nat;
286 Check (' ');
287 Line := Get_Nat;
288 Typ := Getc;
289 Col := Get_Nat;
290
291 pragma Assert (Scope = Cur_Scope);
292
293 -- Scan out scope entity name
294
295 Skip_Spaces;
296 Get_Name;
297 Skip_Spaces;
298
299 if Nextc = '-' then
300 Skipc;
301 Check ('>');
302 Skip_Spaces;
303 Spec_File := Get_Nat;
304 Check ('.');
305 Spec_Scope := Get_Nat;
306
307 else
308 Spec_File := 0;
309 Spec_Scope := 0;
310 end if;
311
312 -- Make new scope table entry (will fill in From_Xref and
313 -- To_Xref later). Initial range (From_Xref .. To_Xref) is
314 -- empty for scopes without entities.
315
316 SPARK_Scope_Table.Append (
317 (Scope_Entity => Empty,
318 Scope_Name => new String'(Name_Str (1 .. Name_Len)),
319 File_Num => Cur_File,
320 Scope_Num => Cur_Scope,
321 Spec_File_Num => Spec_File,
322 Spec_Scope_Num => Spec_Scope,
323 Line => Line,
324 Stype => Typ,
325 Col => Col,
326 From_Xref => 1,
327 To_Xref => 0));
328 end;
329
330 -- Update counter for scopes
331
332 Cur_Scope := Cur_Scope + 1;
333
334 -- Header entry for cross-ref section
335
336 when 'X' =>
337
338 -- Scan out dependency number and file name (ignored)
339
340 Skip_Spaces;
341 Cur_File := Get_Nat;
342 Skip_Spaces;
343 Get_Name;
344
345 -- Update component From_Xref of current file if first reference
346 -- in this file.
347
348 while SPARK_File_Table.Table (Cur_File_Idx).File_Num /= Cur_File
349 loop
350 Cur_File_Idx := Cur_File_Idx + 1;
351 end loop;
352
353 -- Scan out scope entity number and entity name (ignored)
354
355 Skip_Spaces;
356 Check ('.');
357 Cur_Scope := Get_Nat;
358 Skip_Spaces;
359 Get_Name;
360
361 -- Update component To_Xref of previous scope
362
363 if Cur_Scope_Idx /= 0 then
364 SPARK_Scope_Table.Table (Cur_Scope_Idx).To_Xref :=
365 SPARK_Xref_Table.Last;
366 end if;
367
368 -- Update component From_Xref of current scope
369
370 Cur_Scope_Idx := SPARK_File_Table.Table (Cur_File_Idx).From_Scope;
371
372 while SPARK_Scope_Table.Table (Cur_Scope_Idx).Scope_Num /=
373 Cur_Scope
374 loop
375 Cur_Scope_Idx := Cur_Scope_Idx + 1;
376 end loop;
377
378 SPARK_Scope_Table.Table (Cur_Scope_Idx).From_Xref :=
379 SPARK_Xref_Table.Last + 1;
380
381 -- Cross reference entry
382
383 when ' ' =>
384 declare
385 XR_Entity : String_Ptr;
386 XR_Entity_Line : Nat;
387 XR_Entity_Col : Nat;
388 XR_Entity_Typ : Character;
389
390 XR_File : Nat;
391 -- Keeps track of the current file (changed by nn|)
392
393 XR_Scope : Nat;
394 -- Keeps track of the current scope (changed by nn:)
395
396 begin
397 XR_File := Cur_File;
398 XR_Scope := Cur_Scope;
399
400 XR_Entity_Line := Get_Nat;
401 XR_Entity_Typ := Getc;
402 XR_Entity_Col := Get_Nat;
403
404 Skip_Spaces;
405 Get_Name;
406 XR_Entity := new String'(Name_Str (1 .. Name_Len));
407
408 -- Initialize to scan items on one line
409
410 Skip_Spaces;
411
412 -- Loop through cross-references for this entity
413
414 loop
415
416 declare
417 Line : Nat;
418 Col : Nat;
419 N : Nat;
420 Rtype : Character;
421
422 begin
423 Skip_Spaces;
424
425 if At_EOL then
426 Skip_EOL;
427 exit when Nextc /= '.';
428 Skipc;
429 Skip_Spaces;
430 end if;
431
432 if Nextc = '.' then
433 Skipc;
434 XR_Scope := Get_Nat;
435 Check (':');
436
437 else
438 N := Get_Nat;
439
440 if Nextc = '|' then
441 XR_File := N;
442 Skipc;
443
444 else
445 Line := N;
446 Rtype := Getc;
447 Col := Get_Nat;
448
449 pragma Assert
450 (Rtype = 'r' or else
451 Rtype = 'c' or else
452 Rtype = 'm' or else
453 Rtype = 's');
454
455 SPARK_Xref_Table.Append (
456 (Entity_Name => XR_Entity,
457 Entity_Line => XR_Entity_Line,
458 Etype => XR_Entity_Typ,
459 Entity_Col => XR_Entity_Col,
460 File_Num => XR_File,
461 Scope_Num => XR_Scope,
462 Line => Line,
463 Rtype => Rtype,
464 Col => Col));
465 end if;
466 end if;
467 end;
468 end loop;
469 end;
470
471 -- No other SPARK lines are possible
472
473 when others =>
474 raise Data_Error;
475 end case;
476
477 -- For cross reference lines, the EOL character has been skipped already
478
479 if C /= ' ' then
480 Skip_EOL;
481 end if;
482 end loop;
483
484 -- Here with all Xrefs stored, complete last entries in File/Scope tables
485
486 if SPARK_File_Table.Last /= 0 then
487 SPARK_File_Table.Table (SPARK_File_Table.Last).To_Scope :=
488 SPARK_Scope_Table.Last;
489 end if;
490
491 if Cur_Scope_Idx /= 0 then
492 SPARK_Scope_Table.Table (Cur_Scope_Idx).To_Xref := SPARK_Xref_Table.Last;
493 end if;
494 end Get_SPARK_Xrefs;