|
111
|
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 declare
|
|
|
416 Line : Nat;
|
|
|
417 Col : Nat;
|
|
|
418 N : Nat;
|
|
|
419 Rtype : Character;
|
|
|
420
|
|
|
421 begin
|
|
|
422 Skip_Spaces;
|
|
|
423
|
|
|
424 if At_EOL then
|
|
|
425 Skip_EOL;
|
|
|
426 exit when Nextc /= '.';
|
|
|
427 Skipc;
|
|
|
428 Skip_Spaces;
|
|
|
429 end if;
|
|
|
430
|
|
|
431 if Nextc = '.' then
|
|
|
432 Skipc;
|
|
|
433 XR_Scope := Get_Nat;
|
|
|
434 Check (':');
|
|
|
435
|
|
|
436 else
|
|
|
437 N := Get_Nat;
|
|
|
438
|
|
|
439 if Nextc = '|' then
|
|
|
440 XR_File := N;
|
|
|
441 Skipc;
|
|
|
442
|
|
|
443 else
|
|
|
444 Line := N;
|
|
|
445 Rtype := Getc;
|
|
|
446 Col := Get_Nat;
|
|
|
447
|
|
|
448 pragma Assert
|
|
|
449 (Rtype = 'r' or else
|
|
|
450 Rtype = 'c' or else
|
|
|
451 Rtype = 'm' or else
|
|
|
452 Rtype = 's');
|
|
|
453
|
|
|
454 SPARK_Xref_Table.Append (
|
|
|
455 (Entity_Name => XR_Entity,
|
|
|
456 Entity_Line => XR_Entity_Line,
|
|
|
457 Etype => XR_Entity_Typ,
|
|
|
458 Entity_Col => XR_Entity_Col,
|
|
|
459 File_Num => XR_File,
|
|
|
460 Scope_Num => XR_Scope,
|
|
|
461 Line => Line,
|
|
|
462 Rtype => Rtype,
|
|
|
463 Col => Col));
|
|
|
464 end if;
|
|
|
465 end if;
|
|
|
466 end;
|
|
|
467 end loop;
|
|
|
468 end;
|
|
|
469
|
|
|
470 -- No other SPARK lines are possible
|
|
|
471
|
|
|
472 when others =>
|
|
|
473 raise Data_Error;
|
|
|
474 end case;
|
|
|
475
|
|
|
476 -- For cross reference lines, the EOL character has been skipped already
|
|
|
477
|
|
|
478 if C /= ' ' then
|
|
|
479 Skip_EOL;
|
|
|
480 end if;
|
|
|
481 end loop;
|
|
|
482
|
|
|
483 -- Here with all Xrefs stored, complete last entries in File/Scope tables
|
|
|
484
|
|
|
485 if SPARK_File_Table.Last /= 0 then
|
|
|
486 SPARK_File_Table.Table (SPARK_File_Table.Last).To_Scope :=
|
|
|
487 SPARK_Scope_Table.Last;
|
|
|
488 end if;
|
|
|
489
|
|
|
490 if Cur_Scope_Idx /= 0 then
|
|
|
491 SPARK_Scope_Table.Table (Cur_Scope_Idx).To_Xref := SPARK_Xref_Table.Last;
|
|
|
492 end if;
|
|
|
493 end Get_SPARK_Xrefs;
|
