?  search:
summary | log | graphiclog1 | graphiclog2 | commit | commitdiff | tree | refs | edit | fork
blame | history | raw | HEAD
gcc/
[official-gcc.git] / gcc / ada / lib-xref-spark_specific.adb
blobb38d65b23dd4894a75161c16c276413bde236940
1 ------------------------------------------------------------------------------
2 -- --
3 -- GNAT COMPILER COMPONENTS --
4 -- --
5 -- L I B . X R E F . S P A R K _ S P E C I F I C --
6 -- --
7 -- B o d y --
8 -- --
9 -- Copyright (C) 2011-2014, 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 Einfo; use Einfo;
27 with Nmake; use Nmake;
28 with SPARK_Xrefs; use SPARK_Xrefs;
29
30 with GNAT.HTable;
31
32 separate (Lib.Xref)
33 package body SPARK_Specific is
34
35 ---------------------
36 -- Local Constants --
37 ---------------------
38
39 -- Table of SPARK_Entities, True for each entity kind used in SPARK
40
41 SPARK_Entities : constant array (Entity_Kind) of Boolean :=
42 (E_Constant => True,
43 E_Function => True,
44 E_In_Out_Parameter => True,
45 E_In_Parameter => True,
46 E_Loop_Parameter => True,
47 E_Operator => True,
48 E_Out_Parameter => True,
49 E_Procedure => True,
50 E_Variable => True,
51 others => False);
52
53 -- True for each reference type used in SPARK
54
55 SPARK_References : constant array (Character) of Boolean :=
56 ('m' => True,
57 'r' => True,
58 's' => True,
59 others => False);
60
61 type Entity_Hashed_Range is range 0 .. 255;
62 -- Size of hash table headers
63
64 ---------------------
65 -- Local Variables --
66 ---------------------
67
68 Heap : Entity_Id := Empty;
69 -- A special entity which denotes the heap object
70
71 package Drefs is new Table.Table (
72 Table_Component_Type => Xref_Entry,
73 Table_Index_Type => Xref_Entry_Number,
74 Table_Low_Bound => 1,
75 Table_Initial => Alloc.Drefs_Initial,
76 Table_Increment => Alloc.Drefs_Increment,
77 Table_Name => "Drefs");
78 -- Table of cross-references for reads and writes through explicit
79 -- dereferences, that are output as reads/writes to the special variable
80 -- "Heap". These references are added to the regular references when
81 -- computing SPARK cross-references.
82
83 -----------------------
84 -- Local Subprograms --
85 -----------------------
86
87 procedure Add_SPARK_File (Ubody, Uspec : Unit_Number_Type; Dspec : Nat);
88 -- Add file and corresponding scopes for unit to the tables
89 -- SPARK_File_Table and SPARK_Scope_Table. When two units are present for
90 -- the same compilation unit, as it happens for library-level
91 -- instantiations of generics, then Ubody /= Uspec, and all scopes are
92 -- added to the same SPARK file. Otherwise Ubody = Uspec.
93
94 procedure Add_SPARK_Scope (N : Node_Id);
95 -- Add scope N to the table SPARK_Scope_Table
96
97 procedure Add_SPARK_Xrefs;
98 -- Filter table Xrefs to add all references used in SPARK to the table
99 -- SPARK_Xref_Table.
100
101 procedure Detect_And_Add_SPARK_Scope (N : Node_Id);
102 -- Call Add_SPARK_Scope on scopes
103
104 function Entity_Hash (E : Entity_Id) return Entity_Hashed_Range;
105 -- Hash function for hash table
106
107 procedure Traverse_Declarations_Or_Statements
108 (L : List_Id;
109 Process : Node_Processing;
110 Inside_Stubs : Boolean);
111 procedure Traverse_Handled_Statement_Sequence
112 (N : Node_Id;
113 Process : Node_Processing;
114 Inside_Stubs : Boolean);
115 procedure Traverse_Package_Body
116 (N : Node_Id;
117 Process : Node_Processing;
118 Inside_Stubs : Boolean);
119 procedure Traverse_Package_Declaration
120 (N : Node_Id;
121 Process : Node_Processing;
122 Inside_Stubs : Boolean);
123 procedure Traverse_Subprogram_Body
124 (N : Node_Id;
125 Process : Node_Processing;
126 Inside_Stubs : Boolean);
127 -- Traverse corresponding construct, calling Process on all declarations
128
129 --------------------
130 -- Add_SPARK_File --
131 --------------------
132
133 procedure Add_SPARK_File (Ubody, Uspec : Unit_Number_Type; Dspec : Nat) is
134 File : constant Source_File_Index := Source_Index (Uspec);
135 From : Scope_Index;
136
137 File_Name : String_Ptr;
138 Unit_File_Name : String_Ptr;
139
140 begin
141 -- Source file could be inexistant as a result of an error, if option
142 -- gnatQ is used.
143
144 if File = No_Source_File then
145 return;
146 end if;
147
148 From := SPARK_Scope_Table.Last + 1;
149
150 -- Unit might not have an associated compilation unit, as seen in code
151 -- filling Sdep_Table in Write_ALI.
152
153 if Present (Cunit (Ubody)) then
154 Traverse_Compilation_Unit
155 (CU => Cunit (Ubody),
156 Process => Detect_And_Add_SPARK_Scope'Access,
157 Inside_Stubs => False);
158 end if;
159
160 -- When two units are present for the same compilation unit, as it
161 -- happens for library-level instantiations of generics, then add all
162 -- scopes to the same SPARK file.
163
164 if Ubody /= Uspec then
165 if Present (Cunit (Uspec)) then
166 Traverse_Compilation_Unit
167 (CU => Cunit (Uspec),
168 Process => Detect_And_Add_SPARK_Scope'Access,
169 Inside_Stubs => False);
170 end if;
171 end if;
172
173 -- Update scope numbers
174
175 declare
176 Scope_Id : Int;
177 begin
178 Scope_Id := 1;
179 for Index in From .. SPARK_Scope_Table.Last loop
180 declare
181 S : SPARK_Scope_Record renames SPARK_Scope_Table.Table (Index);
182 begin
183 S.Scope_Num := Scope_Id;
184 S.File_Num := Dspec;
185 Scope_Id := Scope_Id + 1;
186 end;
187 end loop;
188 end;
189
190 -- Remove those scopes previously marked for removal
191
192 declare
193 Scope_Id : Scope_Index;
194
195 begin
196 Scope_Id := From;
197 for Index in From .. SPARK_Scope_Table.Last loop
198 declare
199 S : SPARK_Scope_Record renames SPARK_Scope_Table.Table (Index);
200 begin
201 if S.Scope_Num /= 0 then
202 SPARK_Scope_Table.Table (Scope_Id) := S;
203 Scope_Id := Scope_Id + 1;
204 end if;
205 end;
206 end loop;
207
208 SPARK_Scope_Table.Set_Last (Scope_Id - 1);
209 end;
210
211 -- Make entry for new file in file table
212
213 Get_Name_String (Reference_Name (File));
214 File_Name := new String'(Name_Buffer (1 .. Name_Len));
215
216 -- For subunits, also retrieve the file name of the unit. Only do so if
217 -- unit has an associated compilation unit.
218
219 if Present (Cunit (Uspec))
220 and then Present (Cunit (Unit (File)))
221 and then Nkind (Unit (Cunit (Unit (File)))) = N_Subunit
222 then
223 Get_Name_String (Reference_Name (Main_Source_File));
224 Unit_File_Name := new String'(Name_Buffer (1 .. Name_Len));
225 end if;
226
227 SPARK_File_Table.Append (
228 (File_Name => File_Name,
229 Unit_File_Name => Unit_File_Name,
230 File_Num => Dspec,
231 From_Scope => From,
232 To_Scope => SPARK_Scope_Table.Last));
233 end Add_SPARK_File;
234
235 ---------------------
236 -- Add_SPARK_Scope --
237 ---------------------
238
239 procedure Add_SPARK_Scope (N : Node_Id) is
240 E : constant Entity_Id := Defining_Entity (N);
241 Loc : constant Source_Ptr := Sloc (E);
242 Typ : Character;
243
244 begin
245 -- Ignore scopes without a proper location
246
247 if Sloc (N) = No_Location then
248 return;
249 end if;
250
251 case Ekind (E) is
252 when E_Function | E_Generic_Function =>
253 Typ := 'V';
254
255 when E_Procedure | E_Generic_Procedure =>
256 Typ := 'U';
257
258 when E_Subprogram_Body =>
259 declare
260 Spec : Node_Id;
261
262 begin
263 Spec := Parent (E);
264
265 if Nkind (Spec) = N_Defining_Program_Unit_Name then
266 Spec := Parent (Spec);
267 end if;
268
269 if Nkind (Spec) = N_Function_Specification then
270 Typ := 'V';
271 else
272 pragma Assert
273 (Nkind (Spec) = N_Procedure_Specification);
274 Typ := 'U';
275 end if;
276 end;
277
278 when E_Package | E_Package_Body | E_Generic_Package =>
279 Typ := 'K';
280
281 when E_Void =>
282 -- Compilation of prj-attr.adb with -gnatn creates a node with
283 -- entity E_Void for the package defined at a-charac.ads16:13
284
285 -- ??? TBD
286
287 return;
288
289 when others =>
290 raise Program_Error;
291 end case;
292
293 -- File_Num and Scope_Num are filled later. From_Xref and To_Xref are
294 -- filled even later, but are initialized to represent an empty range.
295
296 SPARK_Scope_Table.Append (
297 (Scope_Name => new String'(Unique_Name (E)),
298 File_Num => 0,
299 Scope_Num => 0,
300 Spec_File_Num => 0,
301 Spec_Scope_Num => 0,
302 Line => Nat (Get_Logical_Line_Number (Loc)),
303 Stype => Typ,
304 Col => Nat (Get_Column_Number (Loc)),
305 From_Xref => 1,
306 To_Xref => 0,
307 Scope_Entity => E));
308 end Add_SPARK_Scope;
309
310 ---------------------
311 -- Add_SPARK_Xrefs --
312 ---------------------
313
314 procedure Add_SPARK_Xrefs is
315 function Entity_Of_Scope (S : Scope_Index) return Entity_Id;
316 -- Return the entity which maps to the input scope index
317
318 function Get_Entity_Type (E : Entity_Id) return Character;
319 -- Return a character representing the type of entity
320
321 function Is_SPARK_Reference
322 (E : Entity_Id;
323 Typ : Character) return Boolean;
324 -- Return whether entity reference E meets SPARK requirements. Typ is
325 -- the reference type.
326
327 function Is_SPARK_Scope (E : Entity_Id) return Boolean;
328 -- Return whether the entity or reference scope meets requirements for
329 -- being an SPARK scope.
330
331 function Is_Future_Scope_Entity
332 (E : Entity_Id;
333 S : Scope_Index) return Boolean;
334 -- Check whether entity E is in SPARK_Scope_Table at index S or higher
335
336 function Lt (Op1 : Natural; Op2 : Natural) return Boolean;
337 -- Comparison function for Sort call
338
339 procedure Move (From : Natural; To : Natural);
340 -- Move procedure for Sort call
341
342 procedure Update_Scope_Range
343 (S : Scope_Index;
344 From : Xref_Index;
345 To : Xref_Index);
346 -- Update the scope which maps to S with the new range From .. To
347
348 package Sorting is new GNAT.Heap_Sort_G (Move, Lt);
349
350 function Get_Scope_Num (N : Entity_Id) return Nat;
351 -- Return the scope number associated to entity N
352
353 procedure Set_Scope_Num (N : Entity_Id; Num : Nat);
354 -- Associate entity N to scope number Num
355
356 No_Scope : constant Nat := 0;
357 -- Initial scope counter
358
359 type Scope_Rec is record
360 Num : Nat;
361 Entity : Entity_Id;
362 end record;
363 -- Type used to relate an entity and a scope number
364
365 package Scopes is new GNAT.HTable.Simple_HTable
366 (Header_Num => Entity_Hashed_Range,
367 Element => Scope_Rec,
368 No_Element => (Num => No_Scope, Entity => Empty),
369 Key => Entity_Id,
370 Hash => Entity_Hash,
371 Equal => "=");
372 -- Package used to build a correspondance between entities and scope
373 -- numbers used in SPARK cross references.
374
375 Nrefs : Nat := Xrefs.Last;
376 -- Number of references in table. This value may get reset (reduced)
377 -- when we eliminate duplicate reference entries as well as references
378 -- not suitable for local cross-references.
379
380 Nrefs_Add : constant Nat := Drefs.Last;
381 -- Number of additional references which correspond to dereferences in
382 -- the source code.
383
384 Rnums : array (0 .. Nrefs + Nrefs_Add) of Nat;
385 -- This array contains numbers of references in the Xrefs table. This
386 -- list is sorted in output order. The extra 0'th entry is convenient
387 -- for the call to sort. When we sort the table, we move the entries in
388 -- Rnums around, but we do not move the original table entries.
389
390 ---------------------
391 -- Entity_Of_Scope --
392 ---------------------
393
394 function Entity_Of_Scope (S : Scope_Index) return Entity_Id is
395 begin
396 return SPARK_Scope_Table.Table (S).Scope_Entity;
397 end Entity_Of_Scope;
398
399 ---------------------
400 -- Get_Entity_Type --
401 ---------------------
402
403 function Get_Entity_Type (E : Entity_Id) return Character is
404 begin
405 case Ekind (E) is
406 when E_Out_Parameter => return '<';
407 when E_In_Out_Parameter => return '=';
408 when E_In_Parameter => return '>';
409 when others => return '*';
410 end case;
411 end Get_Entity_Type;
412
413 -------------------
414 -- Get_Scope_Num --
415 -------------------
416
417 function Get_Scope_Num (N : Entity_Id) return Nat is
418 begin
419 return Scopes.Get (N).Num;
420 end Get_Scope_Num;
421
422 ------------------------
423 -- Is_SPARK_Reference --
424 ------------------------
425
426 function Is_SPARK_Reference
427 (E : Entity_Id;
428 Typ : Character) return Boolean
429 is
430 begin
431 -- The only references of interest on callable entities are calls. On
432 -- non-callable entities, the only references of interest are reads
433 -- and writes.
434
435 if Ekind (E) in Overloadable_Kind then
436 return Typ = 's';
437
438 -- Objects of Task type or protected type are not SPARK references
439
440 elsif Present (Etype (E))
441 and then Ekind (Etype (E)) in Concurrent_Kind
442 then
443 return False;
444
445 -- In all other cases, result is true for reference/modify cases,
446 -- and false for all other cases.
447
448 else
449 return Typ = 'r' or else Typ = 'm';
450 end if;
451 end Is_SPARK_Reference;
452
453 --------------------
454 -- Is_SPARK_Scope --
455 --------------------
456
457 function Is_SPARK_Scope (E : Entity_Id) return Boolean is
458 begin
459 return Present (E)
460 and then not Is_Generic_Unit (E)
461 and then Renamed_Entity (E) = Empty
462 and then Get_Scope_Num (E) /= No_Scope;
463 end Is_SPARK_Scope;
464
465 ----------------------------
466 -- Is_Future_Scope_Entity --
467 ----------------------------
468
469 function Is_Future_Scope_Entity
470 (E : Entity_Id;
471 S : Scope_Index) return Boolean
472 is
473 function Is_Past_Scope_Entity return Boolean;
474 -- Check whether entity E is in SPARK_Scope_Table at index strictly
475 -- lower than S.
476
477 --------------------------
478 -- Is_Past_Scope_Entity --
479 --------------------------
480
481 function Is_Past_Scope_Entity return Boolean is
482 begin
483 for Index in SPARK_Scope_Table.First .. S - 1 loop
484 if SPARK_Scope_Table.Table (Index).Scope_Entity = E then
485 declare
486 Dummy : constant SPARK_Scope_Record :=
487 SPARK_Scope_Table.Table (Index);
488 begin
489 return True;
490 end;
491 end if;
492 end loop;
493
494 return False;
495 end Is_Past_Scope_Entity;
496
497 -- Start of processing for Is_Future_Scope_Entity
498
499 begin
500 for Index in S .. SPARK_Scope_Table.Last loop
501 if SPARK_Scope_Table.Table (Index).Scope_Entity = E then
502 return True;
503 end if;
504 end loop;
505
506 -- If this assertion fails, this means that the scope which we are
507 -- looking for has been treated already, which reveals a problem in
508 -- the order of cross-references.
509
510 pragma Assert (not Is_Past_Scope_Entity);
511
512 return False;
513 end Is_Future_Scope_Entity;
514
515 --------
516 -- Lt --
517 --------
518
519 function Lt (Op1, Op2 : Natural) return Boolean is
520 T1 : constant Xref_Entry := Xrefs.Table (Rnums (Nat (Op1)));
521 T2 : constant Xref_Entry := Xrefs.Table (Rnums (Nat (Op2)));
522
523 begin
524 -- First test: if entity is in different unit, sort by unit. Note:
525 -- that we use Ent_Scope_File rather than Eun, as Eun may refer to
526 -- the file where the generic scope is defined, which may differ from
527 -- the file where the enclosing scope is defined. It is the latter
528 -- which matters for a correct order here.
529
530 if T1.Ent_Scope_File /= T2.Ent_Scope_File then
531 return Dependency_Num (T1.Ent_Scope_File) <
532 Dependency_Num (T2.Ent_Scope_File);
533
534 -- Second test: within same unit, sort by location of the scope of
535 -- the entity definition.
536
537 elsif Get_Scope_Num (T1.Key.Ent_Scope) /=
538 Get_Scope_Num (T2.Key.Ent_Scope)
539 then
540 return Get_Scope_Num (T1.Key.Ent_Scope) <
541 Get_Scope_Num (T2.Key.Ent_Scope);
542
543 -- Third test: within same unit and scope, sort by location of
544 -- entity definition.
545
546 elsif T1.Def /= T2.Def then
547 return T1.Def < T2.Def;
548
549 else
550 -- Both entities must be equal at this point
551
552 pragma Assert (T1.Key.Ent = T2.Key.Ent);
553
554 -- Fourth test: if reference is in same unit as entity definition,
555 -- sort first.
556
557 if T1.Key.Lun /= T2.Key.Lun
558 and then T1.Ent_Scope_File = T1.Key.Lun
559 then
560 return True;
561
562 elsif T1.Key.Lun /= T2.Key.Lun
563 and then T2.Ent_Scope_File = T2.Key.Lun
564 then
565 return False;
566
567 -- Fifth test: if reference is in same unit and same scope as
568 -- entity definition, sort first.
569
570 elsif T1.Ent_Scope_File = T1.Key.Lun
571 and then T1.Key.Ref_Scope /= T2.Key.Ref_Scope
572 and then T1.Key.Ent_Scope = T1.Key.Ref_Scope
573 then
574 return True;
575
576 elsif T2.Ent_Scope_File = T2.Key.Lun
577 and then T1.Key.Ref_Scope /= T2.Key.Ref_Scope
578 and then T2.Key.Ent_Scope = T2.Key.Ref_Scope
579 then
580 return False;
581
582 -- Sixth test: for same entity, sort by reference location unit
583
584 elsif T1.Key.Lun /= T2.Key.Lun then
585 return Dependency_Num (T1.Key.Lun) <
586 Dependency_Num (T2.Key.Lun);
587
588 -- Seventh test: for same entity, sort by reference location scope
589
590 elsif Get_Scope_Num (T1.Key.Ref_Scope) /=
591 Get_Scope_Num (T2.Key.Ref_Scope)
592 then
593 return Get_Scope_Num (T1.Key.Ref_Scope) <
594 Get_Scope_Num (T2.Key.Ref_Scope);
595
596 -- Eighth test: order of location within referencing unit
597
598 elsif T1.Key.Loc /= T2.Key.Loc then
599 return T1.Key.Loc < T2.Key.Loc;
600
601 -- Finally, for two locations at the same address prefer the one
602 -- that does NOT have the type 'r', so that a modification or
603 -- extension takes preference, when there are more than one
604 -- reference at the same location. As a result, in the case of
605 -- entities that are in-out actuals, the read reference follows
606 -- the modify reference.
607
608 else
609 return T2.Key.Typ = 'r';
610 end if;
611 end if;
612 end Lt;
613
614 ----------
615 -- Move --
616 ----------
617
618 procedure Move (From : Natural; To : Natural) is
619 begin
620 Rnums (Nat (To)) := Rnums (Nat (From));
621 end Move;
622
623 -------------------
624 -- Set_Scope_Num --
625 -------------------
626
627 procedure Set_Scope_Num (N : Entity_Id; Num : Nat) is
628 begin
629 Scopes.Set (K => N, E => Scope_Rec'(Num => Num, Entity => N));
630 end Set_Scope_Num;
631
632 ------------------------
633 -- Update_Scope_Range --
634 ------------------------
635
636 procedure Update_Scope_Range
637 (S : Scope_Index;
638 From : Xref_Index;
639 To : Xref_Index)
640 is
641 begin
642 SPARK_Scope_Table.Table (S).From_Xref := From;
643 SPARK_Scope_Table.Table (S).To_Xref := To;
644 end Update_Scope_Range;
645
646 -- Local variables
647
648 Col : Nat;
649 From_Index : Xref_Index;
650 Line : Nat;
651 Loc : Source_Ptr;
652 Prev_Typ : Character;
653 Ref_Count : Nat;
654 Ref_Id : Entity_Id;
655 Ref_Name : String_Ptr;
656 Scope_Id : Scope_Index;
657
658 -- Start of processing for Add_SPARK_Xrefs
659
660 begin
661 for Index in SPARK_Scope_Table.First .. SPARK_Scope_Table.Last loop
662 declare
663 S : SPARK_Scope_Record renames SPARK_Scope_Table.Table (Index);
664 begin
665 Set_Scope_Num (S.Scope_Entity, S.Scope_Num);
666 end;
667 end loop;
668
669 -- Set up the pointer vector for the sort
670
671 for Index in 1 .. Nrefs loop
672 Rnums (Index) := Index;
673 end loop;
674
675 for Index in Drefs.First .. Drefs.Last loop
676 Xrefs.Append (Drefs.Table (Index));
677
678 Nrefs := Nrefs + 1;
679 Rnums (Nrefs) := Xrefs.Last;
680 end loop;
681
682 -- Capture the definition Sloc values. As in the case of normal cross
683 -- references, we have to wait until now to get the correct value.
684
685 for Index in 1 .. Nrefs loop
686 Xrefs.Table (Index).Def := Sloc (Xrefs.Table (Index).Key.Ent);
687 end loop;
688
689 -- Eliminate entries not appropriate for SPARK. Done prior to sorting
690 -- cross-references, as it discards useless references which do not have
691 -- a proper format for the comparison function (like no location).
692
693 Ref_Count := Nrefs;
694 Nrefs := 0;
695
696 for Index in 1 .. Ref_Count loop
697 declare
698 Ref : Xref_Key renames Xrefs.Table (Rnums (Index)).Key;
699
700 begin
701 if SPARK_Entities (Ekind (Ref.Ent))
702 and then SPARK_References (Ref.Typ)
703 and then Is_SPARK_Scope (Ref.Ent_Scope)
704 and then Is_SPARK_Scope (Ref.Ref_Scope)
705 and then Is_SPARK_Reference (Ref.Ent, Ref.Typ)
706
707 -- Discard references from unknown scopes, e.g. generic scopes
708
709 and then Get_Scope_Num (Ref.Ent_Scope) /= No_Scope
710 and then Get_Scope_Num (Ref.Ref_Scope) /= No_Scope
711 then
712 Nrefs := Nrefs + 1;
713 Rnums (Nrefs) := Rnums (Index);
714 end if;
715 end;
716 end loop;
717
718 -- Sort the references
719
720 Sorting.Sort (Integer (Nrefs));
721
722 -- Eliminate duplicate entries
723
724 -- We need this test for Ref_Count because if we force ALI file
725 -- generation in case of errors detected, it may be the case that
726 -- Nrefs is 0, so we should not reset it here.
727
728 if Nrefs >= 2 then
729 Ref_Count := Nrefs;
730 Nrefs := 1;
731
732 for Index in 2 .. Ref_Count loop
733 if Xrefs.Table (Rnums (Index)) /=
734 Xrefs.Table (Rnums (Nrefs))
735 then
736 Nrefs := Nrefs + 1;
737 Rnums (Nrefs) := Rnums (Index);
738 end if;
739 end loop;
740 end if;
741
742 -- Eliminate the reference if it is at the same location as the previous
743 -- one, unless it is a read-reference indicating that the entity is an
744 -- in-out actual in a call.
745
746 Ref_Count := Nrefs;
747 Nrefs := 0;
748 Loc := No_Location;
749 Prev_Typ := 'm';
750
751 for Index in 1 .. Ref_Count loop
752 declare
753 Ref : Xref_Key renames Xrefs.Table (Rnums (Index)).Key;
754
755 begin
756 if Ref.Loc /= Loc
757 or else (Prev_Typ = 'm' and then Ref.Typ = 'r')
758 then
759 Loc := Ref.Loc;
760 Prev_Typ := Ref.Typ;
761 Nrefs := Nrefs + 1;
762 Rnums (Nrefs) := Rnums (Index);
763 end if;
764 end;
765 end loop;
766
767 -- The two steps have eliminated all references, nothing to do
768
769 if SPARK_Scope_Table.Last = 0 then
770 return;
771 end if;
772
773 Ref_Id := Empty;
774 Scope_Id := 1;
775 From_Index := 1;
776
777 -- Loop to output references
778
779 for Refno in 1 .. Nrefs loop
780 declare
781 Ref_Entry : Xref_Entry renames Xrefs.Table (Rnums (Refno));
782 Ref : Xref_Key renames Ref_Entry.Key;
783 Typ : Character;
784
785 begin
786 -- If this assertion fails, the scope which we are looking for is
787 -- not in SPARK scope table, which reveals either a problem in the
788 -- construction of the scope table, or an erroneous scope for the
789 -- current cross-reference.
790
791 pragma Assert (Is_Future_Scope_Entity (Ref.Ent_Scope, Scope_Id));
792
793 -- Update the range of cross references to which the current scope
794 -- refers to. This may be the empty range only for the first scope
795 -- considered.
796
797 if Ref.Ent_Scope /= Entity_Of_Scope (Scope_Id) then
798 Update_Scope_Range
799 (S => Scope_Id,
800 From => From_Index,
801 To => SPARK_Xref_Table.Last);
802
803 From_Index := SPARK_Xref_Table.Last + 1;
804 end if;
805
806 while Ref.Ent_Scope /= Entity_Of_Scope (Scope_Id) loop
807 Scope_Id := Scope_Id + 1;
808 pragma Assert (Scope_Id <= SPARK_Scope_Table.Last);
809 end loop;
810
811 if Ref.Ent /= Ref_Id then
812 Ref_Name := new String'(Unique_Name (Ref.Ent));
813 end if;
814
815 if Ref.Ent = Heap then
816 Line := 0;
817 Col := 0;
818 else
819 Line := Int (Get_Logical_Line_Number (Ref_Entry.Def));
820 Col := Int (Get_Column_Number (Ref_Entry.Def));
821 end if;
822
823 -- References to constant objects are considered specially in
824 -- SPARK section, because these will be translated as constants in
825 -- the intermediate language for formal verification, and should
826 -- therefore never appear in frame conditions.
827
828 if Is_Constant_Object (Ref.Ent) then
829 Typ := 'c';
830 else
831 Typ := Ref.Typ;
832 end if;
833
834 SPARK_Xref_Table.Append (
835 (Entity_Name => Ref_Name,
836 Entity_Line => Line,
837 Etype => Get_Entity_Type (Ref.Ent),
838 Entity_Col => Col,
839 File_Num => Dependency_Num (Ref.Lun),
840 Scope_Num => Get_Scope_Num (Ref.Ref_Scope),
841 Line => Int (Get_Logical_Line_Number (Ref.Loc)),
842 Rtype => Typ,
843 Col => Int (Get_Column_Number (Ref.Loc))));
844 end;
845 end loop;
846
847 -- Update the range of cross references to which the scope refers to
848
849 Update_Scope_Range
850 (S => Scope_Id,
851 From => From_Index,
852 To => SPARK_Xref_Table.Last);
853 end Add_SPARK_Xrefs;
854
855 -------------------------
856 -- Collect_SPARK_Xrefs --
857 -------------------------
858
859 procedure Collect_SPARK_Xrefs
860 (Sdep_Table : Unit_Ref_Table;
861 Num_Sdep : Nat)
862 is
863 D1 : Nat;
864 D2 : Nat;
865
866 begin
867 -- Cross-references should have been computed first
868
869 pragma Assert (Xrefs.Last /= 0);
870
871 Initialize_SPARK_Tables;
872
873 -- Generate file and scope SPARK cross-reference information
874
875 D1 := 1;
876 while D1 <= Num_Sdep loop
877
878 -- In rare cases, when treating the library-level instantiation of a
879 -- generic, two consecutive units refer to the same compilation unit
880 -- node and entity. In that case, treat them as a single unit for the
881 -- sake of SPARK cross references by passing to Add_SPARK_File.
882
883 if D1 < Num_Sdep
884 and then Cunit_Entity (Sdep_Table (D1)) =
885 Cunit_Entity (Sdep_Table (D1 + 1))
886 then
887 D2 := D1 + 1;
888 else
889 D2 := D1;
890 end if;
891
892 -- Some files do not correspond to Ada units, and as such present no
893 -- interest for SPARK cross references. Skip these files, as printing
894 -- their name may require printing the full name with spaces, which
895 -- is not handled in the code doing I/O of SPARK cross references.
896
897 if Present (Cunit_Entity (Sdep_Table (D1))) then
898 Add_SPARK_File
899 (Ubody => Sdep_Table (D1),
900 Uspec => Sdep_Table (D2),
901 Dspec => D2);
902 end if;
903
904 D1 := D2 + 1;
905 end loop;
906
907 -- Fill in the spec information when relevant
908
909 declare
910 package Entity_Hash_Table is new
911 GNAT.HTable.Simple_HTable
912 (Header_Num => Entity_Hashed_Range,
913 Element => Scope_Index,
914 No_Element => 0,
915 Key => Entity_Id,
916 Hash => Entity_Hash,
917 Equal => "=");
918
919 begin
920 -- Fill in the hash-table
921
922 for S in SPARK_Scope_Table.First .. SPARK_Scope_Table.Last loop
923 declare
924 Srec : SPARK_Scope_Record renames SPARK_Scope_Table.Table (S);
925 begin
926 Entity_Hash_Table.Set (Srec.Scope_Entity, S);
927 end;
928 end loop;
929
930 -- Use the hash-table to locate spec entities
931
932 for S in SPARK_Scope_Table.First .. SPARK_Scope_Table.Last loop
933 declare
934 Srec : SPARK_Scope_Record renames SPARK_Scope_Table.Table (S);
935
936 Spec_Entity : constant Entity_Id :=
937 Unique_Entity (Srec.Scope_Entity);
938 Spec_Scope : constant Scope_Index :=
939 Entity_Hash_Table.Get (Spec_Entity);
940
941 begin
942 -- Generic spec may be missing in which case Spec_Scope is zero
943
944 if Spec_Entity /= Srec.Scope_Entity
945 and then Spec_Scope /= 0
946 then
947 Srec.Spec_File_Num :=
948 SPARK_Scope_Table.Table (Spec_Scope).File_Num;
949 Srec.Spec_Scope_Num :=
950 SPARK_Scope_Table.Table (Spec_Scope).Scope_Num;
951 end if;
952 end;
953 end loop;
954 end;
955
956 -- Generate SPARK cross-reference information
957
958 Add_SPARK_Xrefs;
959 end Collect_SPARK_Xrefs;
960
961 --------------------------------
962 -- Detect_And_Add_SPARK_Scope --
963 --------------------------------
964
965 procedure Detect_And_Add_SPARK_Scope (N : Node_Id) is
966 begin
967 if Nkind_In (N, N_Subprogram_Declaration,
968 N_Subprogram_Body,
969 N_Subprogram_Body_Stub,
970 N_Package_Declaration,
971 N_Package_Body)
972 then
973 Add_SPARK_Scope (N);
974 end if;
975 end Detect_And_Add_SPARK_Scope;
976
977 -------------------------------------
978 -- Enclosing_Subprogram_Or_Package --
979 -------------------------------------
980
981 function Enclosing_Subprogram_Or_Library_Package
982 (N : Node_Id) return Entity_Id
983 is
984 Result : Entity_Id;
985
986 begin
987 -- If N is the defining identifier for a subprogram, then return the
988 -- enclosing subprogram or package, not this subprogram.
989
990 if Nkind_In (N, N_Defining_Identifier, N_Defining_Operator_Symbol)
991 and then Nkind (Parent (N)) in N_Subprogram_Specification
992 then
993 Result := Parent (Parent (Parent (N)));
994 else
995 Result := N;
996 end if;
997
998 while Present (Result) loop
999 case Nkind (Result) is
1000 when N_Package_Specification =>
1001
1002 -- Only return a library-level package
1003
1004 if Is_Library_Level_Entity (Defining_Entity (Result)) then
1005 Result := Defining_Entity (Result);
1006 exit;
1007 else
1008 Result := Parent (Result);
1009 end if;
1010
1011 when N_Package_Body =>
1012
1013 -- Only return a library-level package
1014
1015 if Is_Library_Level_Entity (Defining_Entity (Result)) then
1016 Result := Defining_Entity (Result);
1017 exit;
1018 else
1019 Result := Parent (Result);
1020 end if;
1021
1022 when N_Subprogram_Specification =>
1023 Result := Defining_Unit_Name (Result);
1024 exit;
1025
1026 when N_Subprogram_Declaration =>
1027 Result := Defining_Unit_Name (Specification (Result));
1028 exit;
1029
1030 when N_Subprogram_Body =>
1031 Result := Defining_Unit_Name (Specification (Result));
1032 exit;
1033
1034 when N_Pragma =>
1035
1036 -- The enclosing subprogram for a precondition, postcondition,
1037 -- or contract case should be the declaration preceding the
1038 -- pragma (skipping any other pragmas between this pragma and
1039 -- this declaration.
1040
1041 while Nkind (Result) = N_Pragma
1042 and then Is_List_Member (Result)
1043 and then Present (Prev (Result))
1044 loop
1045 Result := Prev (Result);
1046 end loop;
1047
1048 if Nkind (Result) = N_Pragma then
1049 Result := Parent (Result);
1050 end if;
1051
1052 when others =>
1053 Result := Parent (Result);
1054 end case;
1055 end loop;
1056
1057 if Nkind (Result) = N_Defining_Program_Unit_Name then
1058 Result := Defining_Identifier (Result);
1059 end if;
1060
1061 -- Do not return a scope without a proper location
1062
1063 if Present (Result)
1064 and then Sloc (Result) = No_Location
1065 then
1066 return Empty;
1067 end if;
1068
1069 return Result;
1070 end Enclosing_Subprogram_Or_Library_Package;
1071
1072 -----------------
1073 -- Entity_Hash --
1074 -----------------
1075
1076 function Entity_Hash (E : Entity_Id) return Entity_Hashed_Range is
1077 begin
1078 return
1079 Entity_Hashed_Range (E mod (Entity_Id (Entity_Hashed_Range'Last) + 1));
1080 end Entity_Hash;
1081
1082 --------------------------
1083 -- Generate_Dereference --
1084 --------------------------
1085
1086 procedure Generate_Dereference
1087 (N : Node_Id;
1088 Typ : Character := 'r')
1089 is
1090 procedure Create_Heap;
1091 -- Create and decorate the special entity which denotes the heap
1092
1093 -----------------
1094 -- Create_Heap --
1095 -----------------
1096
1097 procedure Create_Heap is
1098 begin
1099 Name_Len := Name_Of_Heap_Variable'Length;
1100 Name_Buffer (1 .. Name_Len) := Name_Of_Heap_Variable;
1101
1102 Heap := Make_Defining_Identifier (Standard_Location, Name_Enter);
1103
1104 Set_Ekind (Heap, E_Variable);
1105 Set_Is_Internal (Heap, True);
1106 Set_Has_Fully_Qualified_Name (Heap);
1107 end Create_Heap;
1108
1109 -- Local variables
1110
1111 Loc : constant Source_Ptr := Sloc (N);
1112 Index : Nat;
1113 Ref_Scope : Entity_Id;
1114
1115 -- Start of processing for Generate_Dereference
1116
1117 begin
1118
1119 if Loc > No_Location then
1120 Drefs.Increment_Last;
1121 Index := Drefs.Last;
1122
1123 declare
1124 Deref_Entry : Xref_Entry renames Drefs.Table (Index);
1125 Deref : Xref_Key renames Deref_Entry.Key;
1126
1127 begin
1128 if No (Heap) then
1129 Create_Heap;
1130 end if;
1131
1132 Ref_Scope := Enclosing_Subprogram_Or_Library_Package (N);
1133
1134 Deref.Ent := Heap;
1135 Deref.Loc := Loc;
1136 Deref.Typ := Typ;
1137
1138 -- It is as if the special "Heap" was defined in every scope where
1139 -- it is referenced.
1140
1141 Deref.Eun := Get_Code_Unit (Loc);
1142 Deref.Lun := Get_Code_Unit (Loc);
1143
1144 Deref.Ref_Scope := Ref_Scope;
1145 Deref.Ent_Scope := Ref_Scope;
1146
1147 Deref_Entry.Def := No_Location;
1148
1149 Deref_Entry.Ent_Scope_File := Get_Code_Unit (N);
1150 end;
1151 end if;
1152 end Generate_Dereference;
1153
1154 ------------------------------------
1155 -- Traverse_All_Compilation_Units --
1156 ------------------------------------
1157
1158 procedure Traverse_All_Compilation_Units (Process : Node_Processing) is
1159 begin
1160 for U in Units.First .. Last_Unit loop
1161 Traverse_Compilation_Unit (Cunit (U), Process, Inside_Stubs => False);
1162 end loop;
1163 end Traverse_All_Compilation_Units;
1164
1165 -------------------------------
1166 -- Traverse_Compilation_Unit --
1167 -------------------------------
1168
1169 procedure Traverse_Compilation_Unit
1170 (CU : Node_Id;
1171 Process : Node_Processing;
1172 Inside_Stubs : Boolean)
1173 is
1174 Lu : Node_Id;
1175
1176 begin
1177 -- Get Unit (checking case of subunit)
1178
1179 Lu := Unit (CU);
1180
1181 if Nkind (Lu) = N_Subunit then
1182 Lu := Proper_Body (Lu);
1183 end if;
1184
1185 -- Do not add scopes for generic units
1186
1187 if Nkind (Lu) = N_Package_Body
1188 and then Ekind (Corresponding_Spec (Lu)) in Generic_Unit_Kind
1189 then
1190 return;
1191 end if;
1192
1193 -- Call Process on all declarations
1194
1195 if Nkind (Lu) in N_Declaration
1196 or else Nkind (Lu) in N_Later_Decl_Item
1197 then
1198 Process (Lu);
1199 end if;
1200
1201 -- Traverse the unit
1202
1203 if Nkind (Lu) = N_Subprogram_Body then
1204 Traverse_Subprogram_Body (Lu, Process, Inside_Stubs);
1205
1206 elsif Nkind (Lu) = N_Subprogram_Declaration then
1207 null;
1208
1209 elsif Nkind (Lu) = N_Package_Declaration then
1210 Traverse_Package_Declaration (Lu, Process, Inside_Stubs);
1211
1212 elsif Nkind (Lu) = N_Package_Body then
1213 Traverse_Package_Body (Lu, Process, Inside_Stubs);
1214
1215 -- All other cases of compilation units (e.g. renamings), are not
1216 -- declarations, or else generic declarations which are ignored.
1217
1218 else
1219 null;
1220 end if;
1221 end Traverse_Compilation_Unit;
1222
1223 -----------------------------------------
1224 -- Traverse_Declarations_Or_Statements --
1225 -----------------------------------------
1226
1227 procedure Traverse_Declarations_Or_Statements
1228 (L : List_Id;
1229 Process : Node_Processing;
1230 Inside_Stubs : Boolean)
1231 is
1232 N : Node_Id;
1233
1234 begin
1235 -- Loop through statements or declarations
1236
1237 N := First (L);
1238 while Present (N) loop
1239 -- Call Process on all declarations
1240
1241 if Nkind (N) in N_Declaration
1242 or else
1243 Nkind (N) in N_Later_Decl_Item
1244 then
1245 Process (N);
1246 end if;
1247
1248 case Nkind (N) is
1249
1250 -- Package declaration
1251
1252 when N_Package_Declaration =>
1253 Traverse_Package_Declaration (N, Process, Inside_Stubs);
1254
1255 -- Package body
1256
1257 when N_Package_Body =>
1258 if Ekind (Defining_Entity (N)) /= E_Generic_Package then
1259 Traverse_Package_Body (N, Process, Inside_Stubs);
1260 end if;
1261
1262 when N_Package_Body_Stub =>
1263 if Present (Library_Unit (N)) then
1264 declare
1265 Body_N : constant Node_Id := Get_Body_From_Stub (N);
1266 begin
1267 if Inside_Stubs
1268 and then
1269 Ekind (Defining_Entity (Body_N)) /= E_Generic_Package
1270 then
1271 Traverse_Package_Body (Body_N, Process, Inside_Stubs);
1272 end if;
1273 end;
1274 end if;
1275
1276 -- Subprogram declaration
1277
1278 when N_Subprogram_Declaration =>
1279 null;
1280
1281 -- Subprogram body
1282
1283 when N_Subprogram_Body =>
1284 if not Is_Generic_Subprogram (Defining_Entity (N)) then
1285 Traverse_Subprogram_Body (N, Process, Inside_Stubs);
1286 end if;
1287
1288 when N_Subprogram_Body_Stub =>
1289 if Present (Library_Unit (N)) then
1290 declare
1291 Body_N : constant Node_Id := Get_Body_From_Stub (N);
1292 begin
1293 if Inside_Stubs
1294 and then
1295 not Is_Generic_Subprogram (Defining_Entity (Body_N))
1296 then
1297 Traverse_Subprogram_Body
1298 (Body_N, Process, Inside_Stubs);
1299 end if;
1300 end;
1301 end if;
1302
1303 -- Block statement
1304
1305 when N_Block_Statement =>
1306 Traverse_Declarations_Or_Statements
1307 (Declarations (N), Process, Inside_Stubs);
1308 Traverse_Handled_Statement_Sequence
1309 (Handled_Statement_Sequence (N), Process, Inside_Stubs);
1310
1311 when N_If_Statement =>
1312
1313 -- Traverse the statements in the THEN part
1314
1315 Traverse_Declarations_Or_Statements
1316 (Then_Statements (N), Process, Inside_Stubs);
1317
1318 -- Loop through ELSIF parts if present
1319
1320 if Present (Elsif_Parts (N)) then
1321 declare
1322 Elif : Node_Id := First (Elsif_Parts (N));
1323
1324 begin
1325 while Present (Elif) loop
1326 Traverse_Declarations_Or_Statements
1327 (Then_Statements (Elif), Process, Inside_Stubs);
1328 Next (Elif);
1329 end loop;
1330 end;
1331 end if;
1332
1333 -- Finally traverse the ELSE statements if present
1334
1335 Traverse_Declarations_Or_Statements
1336 (Else_Statements (N), Process, Inside_Stubs);
1337
1338 -- Case statement
1339
1340 when N_Case_Statement =>
1341
1342 -- Process case branches
1343
1344 declare
1345 Alt : Node_Id;
1346 begin
1347 Alt := First (Alternatives (N));
1348 while Present (Alt) loop
1349 Traverse_Declarations_Or_Statements
1350 (Statements (Alt), Process, Inside_Stubs);
1351 Next (Alt);
1352 end loop;
1353 end;
1354
1355 -- Extended return statement
1356
1357 when N_Extended_Return_Statement =>
1358 Traverse_Handled_Statement_Sequence
1359 (Handled_Statement_Sequence (N), Process, Inside_Stubs);
1360
1361 -- Loop
1362
1363 when N_Loop_Statement =>
1364 Traverse_Declarations_Or_Statements
1365 (Statements (N), Process, Inside_Stubs);
1366
1367 -- Generic declarations are ignored
1368
1369 when others =>
1370 null;
1371 end case;
1372
1373 Next (N);
1374 end loop;
1375 end Traverse_Declarations_Or_Statements;
1376
1377 -----------------------------------------
1378 -- Traverse_Handled_Statement_Sequence --
1379 -----------------------------------------
1380
1381 procedure Traverse_Handled_Statement_Sequence
1382 (N : Node_Id;
1383 Process : Node_Processing;
1384 Inside_Stubs : Boolean)
1385 is
1386 Handler : Node_Id;
1387
1388 begin
1389 if Present (N) then
1390 Traverse_Declarations_Or_Statements
1391 (Statements (N), Process, Inside_Stubs);
1392
1393 if Present (Exception_Handlers (N)) then
1394 Handler := First (Exception_Handlers (N));
1395 while Present (Handler) loop
1396 Traverse_Declarations_Or_Statements
1397 (Statements (Handler), Process, Inside_Stubs);
1398 Next (Handler);
1399 end loop;
1400 end if;
1401 end if;
1402 end Traverse_Handled_Statement_Sequence;
1403
1404 ---------------------------
1405 -- Traverse_Package_Body --
1406 ---------------------------
1407
1408 procedure Traverse_Package_Body
1409 (N : Node_Id;
1410 Process : Node_Processing;
1411 Inside_Stubs : Boolean) is
1412 begin
1413 Traverse_Declarations_Or_Statements
1414 (Declarations (N), Process, Inside_Stubs);
1415 Traverse_Handled_Statement_Sequence
1416 (Handled_Statement_Sequence (N), Process, Inside_Stubs);
1417 end Traverse_Package_Body;
1418
1419 ----------------------------------
1420 -- Traverse_Package_Declaration --
1421 ----------------------------------
1422
1423 procedure Traverse_Package_Declaration
1424 (N : Node_Id;
1425 Process : Node_Processing;
1426 Inside_Stubs : Boolean)
1427 is
1428 Spec : constant Node_Id := Specification (N);
1429 begin
1430 Traverse_Declarations_Or_Statements
1431 (Visible_Declarations (Spec), Process, Inside_Stubs);
1432 Traverse_Declarations_Or_Statements
1433 (Private_Declarations (Spec), Process, Inside_Stubs);
1434 end Traverse_Package_Declaration;
1435
1436 ------------------------------
1437 -- Traverse_Subprogram_Body --
1438 ------------------------------
1439
1440 procedure Traverse_Subprogram_Body
1441 (N : Node_Id;
1442 Process : Node_Processing;
1443 Inside_Stubs : Boolean)
1444 is
1445 begin
1446 Traverse_Declarations_Or_Statements
1447 (Declarations (N), Process, Inside_Stubs);
1448 Traverse_Handled_Statement_Sequence
1449 (Handled_Statement_Sequence (N), Process, Inside_Stubs);
1450 end Traverse_Subprogram_Body;
1451
1452 end SPARK_Specific;
Mirror of the offical gcc git repository hosted at gcc.gnu.org