?  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
blob7e7d52bb07bc8fc96ec55a47f14cdeed447ebdce
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 pragma Unreferenced (Dummy);
489 begin
490 return True;
491 end;
492 end if;
493 end loop;
494
495 return False;
496 end Is_Past_Scope_Entity;
497
498 -- Start of processing for Is_Future_Scope_Entity
499
500 begin
501 for Index in S .. SPARK_Scope_Table.Last loop
502 if SPARK_Scope_Table.Table (Index).Scope_Entity = E then
503 return True;
504 end if;
505 end loop;
506
507 -- If this assertion fails, this means that the scope which we are
508 -- looking for has been treated already, which reveals a problem in
509 -- the order of cross-references.
510
511 pragma Assert (not Is_Past_Scope_Entity);
512
513 return False;
514 end Is_Future_Scope_Entity;
515
516 --------
517 -- Lt --
518 --------
519
520 function Lt (Op1, Op2 : Natural) return Boolean is
521 T1 : constant Xref_Entry := Xrefs.Table (Rnums (Nat (Op1)));
522 T2 : constant Xref_Entry := Xrefs.Table (Rnums (Nat (Op2)));
523
524 begin
525 -- First test: if entity is in different unit, sort by unit. Note:
526 -- that we use Ent_Scope_File rather than Eun, as Eun may refer to
527 -- the file where the generic scope is defined, which may differ from
528 -- the file where the enclosing scope is defined. It is the latter
529 -- which matters for a correct order here.
530
531 if T1.Ent_Scope_File /= T2.Ent_Scope_File then
532 return Dependency_Num (T1.Ent_Scope_File) <
533 Dependency_Num (T2.Ent_Scope_File);
534
535 -- Second test: within same unit, sort by location of the scope of
536 -- the entity definition.
537
538 elsif Get_Scope_Num (T1.Key.Ent_Scope) /=
539 Get_Scope_Num (T2.Key.Ent_Scope)
540 then
541 return Get_Scope_Num (T1.Key.Ent_Scope) <
542 Get_Scope_Num (T2.Key.Ent_Scope);
543
544 -- Third test: within same unit and scope, sort by location of
545 -- entity definition.
546
547 elsif T1.Def /= T2.Def then
548 return T1.Def < T2.Def;
549
550 else
551 -- Both entities must be equal at this point
552
553 pragma Assert (T1.Key.Ent = T2.Key.Ent);
554
555 -- Fourth test: if reference is in same unit as entity definition,
556 -- sort first.
557
558 if T1.Key.Lun /= T2.Key.Lun
559 and then T1.Ent_Scope_File = T1.Key.Lun
560 then
561 return True;
562
563 elsif T1.Key.Lun /= T2.Key.Lun
564 and then T2.Ent_Scope_File = T2.Key.Lun
565 then
566 return False;
567
568 -- Fifth test: if reference is in same unit and same scope as
569 -- entity definition, sort first.
570
571 elsif T1.Ent_Scope_File = T1.Key.Lun
572 and then T1.Key.Ref_Scope /= T2.Key.Ref_Scope
573 and then T1.Key.Ent_Scope = T1.Key.Ref_Scope
574 then
575 return True;
576
577 elsif T2.Ent_Scope_File = T2.Key.Lun
578 and then T1.Key.Ref_Scope /= T2.Key.Ref_Scope
579 and then T2.Key.Ent_Scope = T2.Key.Ref_Scope
580 then
581 return False;
582
583 -- Sixth test: for same entity, sort by reference location unit
584
585 elsif T1.Key.Lun /= T2.Key.Lun then
586 return Dependency_Num (T1.Key.Lun) <
587 Dependency_Num (T2.Key.Lun);
588
589 -- Seventh test: for same entity, sort by reference location scope
590
591 elsif Get_Scope_Num (T1.Key.Ref_Scope) /=
592 Get_Scope_Num (T2.Key.Ref_Scope)
593 then
594 return Get_Scope_Num (T1.Key.Ref_Scope) <
595 Get_Scope_Num (T2.Key.Ref_Scope);
596
597 -- Eighth test: order of location within referencing unit
598
599 elsif T1.Key.Loc /= T2.Key.Loc then
600 return T1.Key.Loc < T2.Key.Loc;
601
602 -- Finally, for two locations at the same address prefer the one
603 -- that does NOT have the type 'r', so that a modification or
604 -- extension takes preference, when there are more than one
605 -- reference at the same location. As a result, in the case of
606 -- entities that are in-out actuals, the read reference follows
607 -- the modify reference.
608
609 else
610 return T2.Key.Typ = 'r';
611 end if;
612 end if;
613 end Lt;
614
615 ----------
616 -- Move --
617 ----------
618
619 procedure Move (From : Natural; To : Natural) is
620 begin
621 Rnums (Nat (To)) := Rnums (Nat (From));
622 end Move;
623
624 -------------------
625 -- Set_Scope_Num --
626 -------------------
627
628 procedure Set_Scope_Num (N : Entity_Id; Num : Nat) is
629 begin
630 Scopes.Set (K => N, E => Scope_Rec'(Num => Num, Entity => N));
631 end Set_Scope_Num;
632
633 ------------------------
634 -- Update_Scope_Range --
635 ------------------------
636
637 procedure Update_Scope_Range
638 (S : Scope_Index;
639 From : Xref_Index;
640 To : Xref_Index)
641 is
642 begin
643 SPARK_Scope_Table.Table (S).From_Xref := From;
644 SPARK_Scope_Table.Table (S).To_Xref := To;
645 end Update_Scope_Range;
646
647 -- Local variables
648
649 Col : Nat;
650 From_Index : Xref_Index;
651 Line : Nat;
652 Loc : Source_Ptr;
653 Prev_Typ : Character;
654 Ref_Count : Nat;
655 Ref_Id : Entity_Id;
656 Ref_Name : String_Ptr;
657 Scope_Id : Scope_Index;
658
659 -- Start of processing for Add_SPARK_Xrefs
660
661 begin
662 for Index in SPARK_Scope_Table.First .. SPARK_Scope_Table.Last loop
663 declare
664 S : SPARK_Scope_Record renames SPARK_Scope_Table.Table (Index);
665 begin
666 Set_Scope_Num (S.Scope_Entity, S.Scope_Num);
667 end;
668 end loop;
669
670 -- Set up the pointer vector for the sort
671
672 for Index in 1 .. Nrefs loop
673 Rnums (Index) := Index;
674 end loop;
675
676 for Index in Drefs.First .. Drefs.Last loop
677 Xrefs.Append (Drefs.Table (Index));
678
679 Nrefs := Nrefs + 1;
680 Rnums (Nrefs) := Xrefs.Last;
681 end loop;
682
683 -- Capture the definition Sloc values. As in the case of normal cross
684 -- references, we have to wait until now to get the correct value.
685
686 for Index in 1 .. Nrefs loop
687 Xrefs.Table (Index).Def := Sloc (Xrefs.Table (Index).Key.Ent);
688 end loop;
689
690 -- Eliminate entries not appropriate for SPARK. Done prior to sorting
691 -- cross-references, as it discards useless references which do not have
692 -- a proper format for the comparison function (like no location).
693
694 Ref_Count := Nrefs;
695 Nrefs := 0;
696
697 for Index in 1 .. Ref_Count loop
698 declare
699 Ref : Xref_Key renames Xrefs.Table (Rnums (Index)).Key;
700
701 begin
702 if SPARK_Entities (Ekind (Ref.Ent))
703 and then SPARK_References (Ref.Typ)
704 and then Is_SPARK_Scope (Ref.Ent_Scope)
705 and then Is_SPARK_Scope (Ref.Ref_Scope)
706 and then Is_SPARK_Reference (Ref.Ent, Ref.Typ)
707
708 -- Discard references from unknown scopes, e.g. generic scopes
709
710 and then Get_Scope_Num (Ref.Ent_Scope) /= No_Scope
711 and then Get_Scope_Num (Ref.Ref_Scope) /= No_Scope
712 then
713 Nrefs := Nrefs + 1;
714 Rnums (Nrefs) := Rnums (Index);
715 end if;
716 end;
717 end loop;
718
719 -- Sort the references
720
721 Sorting.Sort (Integer (Nrefs));
722
723 -- Eliminate duplicate entries
724
725 -- We need this test for Ref_Count because if we force ALI file
726 -- generation in case of errors detected, it may be the case that
727 -- Nrefs is 0, so we should not reset it here.
728
729 if Nrefs >= 2 then
730 Ref_Count := Nrefs;
731 Nrefs := 1;
732
733 for Index in 2 .. Ref_Count loop
734 if Xrefs.Table (Rnums (Index)) /=
735 Xrefs.Table (Rnums (Nrefs))
736 then
737 Nrefs := Nrefs + 1;
738 Rnums (Nrefs) := Rnums (Index);
739 end if;
740 end loop;
741 end if;
742
743 -- Eliminate the reference if it is at the same location as the previous
744 -- one, unless it is a read-reference indicating that the entity is an
745 -- in-out actual in a call.
746
747 Ref_Count := Nrefs;
748 Nrefs := 0;
749 Loc := No_Location;
750 Prev_Typ := 'm';
751
752 for Index in 1 .. Ref_Count loop
753 declare
754 Ref : Xref_Key renames Xrefs.Table (Rnums (Index)).Key;
755
756 begin
757 if Ref.Loc /= Loc
758 or else (Prev_Typ = 'm' and then Ref.Typ = 'r')
759 then
760 Loc := Ref.Loc;
761 Prev_Typ := Ref.Typ;
762 Nrefs := Nrefs + 1;
763 Rnums (Nrefs) := Rnums (Index);
764 end if;
765 end;
766 end loop;
767
768 -- The two steps have eliminated all references, nothing to do
769
770 if SPARK_Scope_Table.Last = 0 then
771 return;
772 end if;
773
774 Ref_Id := Empty;
775 Scope_Id := 1;
776 From_Index := 1;
777
778 -- Loop to output references
779
780 for Refno in 1 .. Nrefs loop
781 declare
782 Ref_Entry : Xref_Entry renames Xrefs.Table (Rnums (Refno));
783 Ref : Xref_Key renames Ref_Entry.Key;
784 Typ : Character;
785
786 begin
787 -- If this assertion fails, the scope which we are looking for is
788 -- not in SPARK scope table, which reveals either a problem in the
789 -- construction of the scope table, or an erroneous scope for the
790 -- current cross-reference.
791
792 pragma Assert (Is_Future_Scope_Entity (Ref.Ent_Scope, Scope_Id));
793
794 -- Update the range of cross references to which the current scope
795 -- refers to. This may be the empty range only for the first scope
796 -- considered.
797
798 if Ref.Ent_Scope /= Entity_Of_Scope (Scope_Id) then
799 Update_Scope_Range
800 (S => Scope_Id,
801 From => From_Index,
802 To => SPARK_Xref_Table.Last);
803
804 From_Index := SPARK_Xref_Table.Last + 1;
805 end if;
806
807 while Ref.Ent_Scope /= Entity_Of_Scope (Scope_Id) loop
808 Scope_Id := Scope_Id + 1;
809 pragma Assert (Scope_Id <= SPARK_Scope_Table.Last);
810 end loop;
811
812 if Ref.Ent /= Ref_Id then
813 Ref_Name := new String'(Unique_Name (Ref.Ent));
814 end if;
815
816 if Ref.Ent = Heap then
817 Line := 0;
818 Col := 0;
819 else
820 Line := Int (Get_Logical_Line_Number (Ref_Entry.Def));
821 Col := Int (Get_Column_Number (Ref_Entry.Def));
822 end if;
823
824 -- References to constant objects are considered specially in
825 -- SPARK section, because these will be translated as constants in
826 -- the intermediate language for formal verification, and should
827 -- therefore never appear in frame conditions.
828
829 if Is_Constant_Object (Ref.Ent) then
830 Typ := 'c';
831 else
832 Typ := Ref.Typ;
833 end if;
834
835 SPARK_Xref_Table.Append (
836 (Entity_Name => Ref_Name,
837 Entity_Line => Line,
838 Etype => Get_Entity_Type (Ref.Ent),
839 Entity_Col => Col,
840 File_Num => Dependency_Num (Ref.Lun),
841 Scope_Num => Get_Scope_Num (Ref.Ref_Scope),
842 Line => Int (Get_Logical_Line_Number (Ref.Loc)),
843 Rtype => Typ,
844 Col => Int (Get_Column_Number (Ref.Loc))));
845 end;
846 end loop;
847
848 -- Update the range of cross references to which the scope refers to
849
850 Update_Scope_Range
851 (S => Scope_Id,
852 From => From_Index,
853 To => SPARK_Xref_Table.Last);
854 end Add_SPARK_Xrefs;
855
856 -------------------------
857 -- Collect_SPARK_Xrefs --
858 -------------------------
859
860 procedure Collect_SPARK_Xrefs
861 (Sdep_Table : Unit_Ref_Table;
862 Num_Sdep : Nat)
863 is
864 D1 : Nat;
865 D2 : Nat;
866
867 begin
868 -- Cross-references should have been computed first
869
870 pragma Assert (Xrefs.Last /= 0);
871
872 Initialize_SPARK_Tables;
873
874 -- Generate file and scope SPARK cross-reference information
875
876 D1 := 1;
877 while D1 <= Num_Sdep loop
878
879 -- In rare cases, when treating the library-level instantiation of a
880 -- generic, two consecutive units refer to the same compilation unit
881 -- node and entity. In that case, treat them as a single unit for the
882 -- sake of SPARK cross references by passing to Add_SPARK_File.
883
884 if D1 < Num_Sdep
885 and then Cunit_Entity (Sdep_Table (D1)) =
886 Cunit_Entity (Sdep_Table (D1 + 1))
887 then
888 D2 := D1 + 1;
889 else
890 D2 := D1;
891 end if;
892
893 Add_SPARK_File
894 (Ubody => Sdep_Table (D1),
895 Uspec => Sdep_Table (D2),
896 Dspec => D2);
897 D1 := D2 + 1;
898 end loop;
899
900 -- Fill in the spec information when relevant
901
902 declare
903 package Entity_Hash_Table is new
904 GNAT.HTable.Simple_HTable
905 (Header_Num => Entity_Hashed_Range,
906 Element => Scope_Index,
907 No_Element => 0,
908 Key => Entity_Id,
909 Hash => Entity_Hash,
910 Equal => "=");
911
912 begin
913 -- Fill in the hash-table
914
915 for S in SPARK_Scope_Table.First .. SPARK_Scope_Table.Last loop
916 declare
917 Srec : SPARK_Scope_Record renames SPARK_Scope_Table.Table (S);
918 begin
919 Entity_Hash_Table.Set (Srec.Scope_Entity, S);
920 end;
921 end loop;
922
923 -- Use the hash-table to locate spec entities
924
925 for S in SPARK_Scope_Table.First .. SPARK_Scope_Table.Last loop
926 declare
927 Srec : SPARK_Scope_Record renames SPARK_Scope_Table.Table (S);
928
929 Spec_Entity : constant Entity_Id :=
930 Unique_Entity (Srec.Scope_Entity);
931 Spec_Scope : constant Scope_Index :=
932 Entity_Hash_Table.Get (Spec_Entity);
933
934 begin
935 -- Generic spec may be missing in which case Spec_Scope is zero
936
937 if Spec_Entity /= Srec.Scope_Entity
938 and then Spec_Scope /= 0
939 then
940 Srec.Spec_File_Num :=
941 SPARK_Scope_Table.Table (Spec_Scope).File_Num;
942 Srec.Spec_Scope_Num :=
943 SPARK_Scope_Table.Table (Spec_Scope).Scope_Num;
944 end if;
945 end;
946 end loop;
947 end;
948
949 -- Generate SPARK cross-reference information
950
951 Add_SPARK_Xrefs;
952 end Collect_SPARK_Xrefs;
953
954 --------------------------------
955 -- Detect_And_Add_SPARK_Scope --
956 --------------------------------
957
958 procedure Detect_And_Add_SPARK_Scope (N : Node_Id) is
959 begin
960 if Nkind_In (N, N_Subprogram_Declaration,
961 N_Subprogram_Body,
962 N_Subprogram_Body_Stub,
963 N_Package_Declaration,
964 N_Package_Body)
965 then
966 Add_SPARK_Scope (N);
967 end if;
968 end Detect_And_Add_SPARK_Scope;
969
970 -------------------------------------
971 -- Enclosing_Subprogram_Or_Package --
972 -------------------------------------
973
974 function Enclosing_Subprogram_Or_Library_Package
975 (N : Node_Id) return Entity_Id
976 is
977 Result : Entity_Id;
978
979 begin
980 -- If N is the defining identifier for a subprogram, then return the
981 -- enclosing subprogram or package, not this subprogram.
982
983 if Nkind_In (N, N_Defining_Identifier, N_Defining_Operator_Symbol)
984 and then Nkind (Parent (N)) in N_Subprogram_Specification
985 then
986 Result := Parent (Parent (Parent (N)));
987 else
988 Result := N;
989 end if;
990
991 while Present (Result) loop
992 case Nkind (Result) is
993 when N_Package_Specification =>
994
995 -- Only return a library-level package
996
997 if Is_Library_Level_Entity (Defining_Entity (Result)) then
998 Result := Defining_Entity (Result);
999 exit;
1000 else
1001 Result := Parent (Result);
1002 end if;
1003
1004 when N_Package_Body =>
1005
1006 -- Only return a library-level package
1007
1008 if Is_Library_Level_Entity (Defining_Entity (Result)) then
1009 Result := Defining_Entity (Result);
1010 exit;
1011 else
1012 Result := Parent (Result);
1013 end if;
1014
1015 when N_Subprogram_Specification =>
1016 Result := Defining_Unit_Name (Result);
1017 exit;
1018
1019 when N_Subprogram_Declaration =>
1020 Result := Defining_Unit_Name (Specification (Result));
1021 exit;
1022
1023 when N_Subprogram_Body =>
1024 Result := Defining_Unit_Name (Specification (Result));
1025 exit;
1026
1027 when N_Pragma =>
1028
1029 -- The enclosing subprogram for a precondition, postcondition,
1030 -- or contract case should be the declaration preceding the
1031 -- pragma (skipping any other pragmas between this pragma and
1032 -- this declaration.
1033
1034 while Nkind (Result) = N_Pragma
1035 and then Is_List_Member (Result)
1036 and then Present (Prev (Result))
1037 loop
1038 Result := Prev (Result);
1039 end loop;
1040
1041 if Nkind (Result) = N_Pragma then
1042 Result := Parent (Result);
1043 end if;
1044
1045 when others =>
1046 Result := Parent (Result);
1047 end case;
1048 end loop;
1049
1050 if Nkind (Result) = N_Defining_Program_Unit_Name then
1051 Result := Defining_Identifier (Result);
1052 end if;
1053
1054 -- Do not return a scope without a proper location
1055
1056 if Present (Result)
1057 and then Sloc (Result) = No_Location
1058 then
1059 return Empty;
1060 end if;
1061
1062 return Result;
1063 end Enclosing_Subprogram_Or_Library_Package;
1064
1065 -----------------
1066 -- Entity_Hash --
1067 -----------------
1068
1069 function Entity_Hash (E : Entity_Id) return Entity_Hashed_Range is
1070 begin
1071 return
1072 Entity_Hashed_Range (E mod (Entity_Id (Entity_Hashed_Range'Last) + 1));
1073 end Entity_Hash;
1074
1075 --------------------------
1076 -- Generate_Dereference --
1077 --------------------------
1078
1079 procedure Generate_Dereference
1080 (N : Node_Id;
1081 Typ : Character := 'r')
1082 is
1083 procedure Create_Heap;
1084 -- Create and decorate the special entity which denotes the heap
1085
1086 -----------------
1087 -- Create_Heap --
1088 -----------------
1089
1090 procedure Create_Heap is
1091 begin
1092 Name_Len := Name_Of_Heap_Variable'Length;
1093 Name_Buffer (1 .. Name_Len) := Name_Of_Heap_Variable;
1094
1095 Heap := Make_Defining_Identifier (Standard_Location, Name_Enter);
1096
1097 Set_Ekind (Heap, E_Variable);
1098 Set_Is_Internal (Heap, True);
1099 Set_Has_Fully_Qualified_Name (Heap);
1100 end Create_Heap;
1101
1102 -- Local variables
1103
1104 Loc : constant Source_Ptr := Sloc (N);
1105 Index : Nat;
1106 Ref_Scope : Entity_Id;
1107
1108 -- Start of processing for Generate_Dereference
1109
1110 begin
1111
1112 if Loc > No_Location then
1113 Drefs.Increment_Last;
1114 Index := Drefs.Last;
1115
1116 declare
1117 Deref_Entry : Xref_Entry renames Drefs.Table (Index);
1118 Deref : Xref_Key renames Deref_Entry.Key;
1119
1120 begin
1121 if No (Heap) then
1122 Create_Heap;
1123 end if;
1124
1125 Ref_Scope := Enclosing_Subprogram_Or_Library_Package (N);
1126
1127 Deref.Ent := Heap;
1128 Deref.Loc := Loc;
1129 Deref.Typ := Typ;
1130
1131 -- It is as if the special "Heap" was defined in every scope where
1132 -- it is referenced.
1133
1134 Deref.Eun := Get_Code_Unit (Loc);
1135 Deref.Lun := Get_Code_Unit (Loc);
1136
1137 Deref.Ref_Scope := Ref_Scope;
1138 Deref.Ent_Scope := Ref_Scope;
1139
1140 Deref_Entry.Def := No_Location;
1141
1142 Deref_Entry.Ent_Scope_File := Get_Code_Unit (N);
1143 end;
1144 end if;
1145 end Generate_Dereference;
1146
1147 ------------------------------------
1148 -- Traverse_All_Compilation_Units --
1149 ------------------------------------
1150
1151 procedure Traverse_All_Compilation_Units (Process : Node_Processing) is
1152 begin
1153 for U in Units.First .. Last_Unit loop
1154 Traverse_Compilation_Unit (Cunit (U), Process, Inside_Stubs => False);
1155 end loop;
1156 end Traverse_All_Compilation_Units;
1157
1158 -------------------------------
1159 -- Traverse_Compilation_Unit --
1160 -------------------------------
1161
1162 procedure Traverse_Compilation_Unit
1163 (CU : Node_Id;
1164 Process : Node_Processing;
1165 Inside_Stubs : Boolean)
1166 is
1167 Lu : Node_Id;
1168
1169 begin
1170 -- Get Unit (checking case of subunit)
1171
1172 Lu := Unit (CU);
1173
1174 if Nkind (Lu) = N_Subunit then
1175 Lu := Proper_Body (Lu);
1176 end if;
1177
1178 -- Do not add scopes for generic units
1179
1180 if Nkind (Lu) = N_Package_Body
1181 and then Ekind (Corresponding_Spec (Lu)) in Generic_Unit_Kind
1182 then
1183 return;
1184 end if;
1185
1186 -- Call Process on all declarations
1187
1188 if Nkind (Lu) in N_Declaration
1189 or else Nkind (Lu) in N_Later_Decl_Item
1190 then
1191 Process (Lu);
1192 end if;
1193
1194 -- Traverse the unit
1195
1196 if Nkind (Lu) = N_Subprogram_Body then
1197 Traverse_Subprogram_Body (Lu, Process, Inside_Stubs);
1198
1199 elsif Nkind (Lu) = N_Subprogram_Declaration then
1200 null;
1201
1202 elsif Nkind (Lu) = N_Package_Declaration then
1203 Traverse_Package_Declaration (Lu, Process, Inside_Stubs);
1204
1205 elsif Nkind (Lu) = N_Package_Body then
1206 Traverse_Package_Body (Lu, Process, Inside_Stubs);
1207
1208 -- All other cases of compilation units (e.g. renamings), are not
1209 -- declarations, or else generic declarations which are ignored.
1210
1211 else
1212 null;
1213 end if;
1214 end Traverse_Compilation_Unit;
1215
1216 -----------------------------------------
1217 -- Traverse_Declarations_Or_Statements --
1218 -----------------------------------------
1219
1220 procedure Traverse_Declarations_Or_Statements
1221 (L : List_Id;
1222 Process : Node_Processing;
1223 Inside_Stubs : Boolean)
1224 is
1225 N : Node_Id;
1226
1227 begin
1228 -- Loop through statements or declarations
1229
1230 N := First (L);
1231 while Present (N) loop
1232 -- Call Process on all declarations
1233
1234 if Nkind (N) in N_Declaration
1235 or else
1236 Nkind (N) in N_Later_Decl_Item
1237 then
1238 Process (N);
1239 end if;
1240
1241 case Nkind (N) is
1242
1243 -- Package declaration
1244
1245 when N_Package_Declaration =>
1246 Traverse_Package_Declaration (N, Process, Inside_Stubs);
1247
1248 -- Package body
1249
1250 when N_Package_Body =>
1251 if Ekind (Defining_Entity (N)) /= E_Generic_Package then
1252 Traverse_Package_Body (N, Process, Inside_Stubs);
1253 end if;
1254
1255 when N_Package_Body_Stub =>
1256 if Present (Library_Unit (N)) then
1257 declare
1258 Body_N : constant Node_Id := Get_Body_From_Stub (N);
1259 begin
1260 if Inside_Stubs
1261 and then
1262 Ekind (Defining_Entity (Body_N)) /= E_Generic_Package
1263 then
1264 Traverse_Package_Body (Body_N, Process, Inside_Stubs);
1265 end if;
1266 end;
1267 end if;
1268
1269 -- Subprogram declaration
1270
1271 when N_Subprogram_Declaration =>
1272 null;
1273
1274 -- Subprogram body
1275
1276 when N_Subprogram_Body =>
1277 if not Is_Generic_Subprogram (Defining_Entity (N)) then
1278 Traverse_Subprogram_Body (N, Process, Inside_Stubs);
1279 end if;
1280
1281 when N_Subprogram_Body_Stub =>
1282 if Present (Library_Unit (N)) then
1283 declare
1284 Body_N : constant Node_Id := Get_Body_From_Stub (N);
1285 begin
1286 if Inside_Stubs
1287 and then
1288 not Is_Generic_Subprogram (Defining_Entity (Body_N))
1289 then
1290 Traverse_Subprogram_Body
1291 (Body_N, Process, Inside_Stubs);
1292 end if;
1293 end;
1294 end if;
1295
1296 -- Block statement
1297
1298 when N_Block_Statement =>
1299 Traverse_Declarations_Or_Statements
1300 (Declarations (N), Process, Inside_Stubs);
1301 Traverse_Handled_Statement_Sequence
1302 (Handled_Statement_Sequence (N), Process, Inside_Stubs);
1303
1304 when N_If_Statement =>
1305
1306 -- Traverse the statements in the THEN part
1307
1308 Traverse_Declarations_Or_Statements
1309 (Then_Statements (N), Process, Inside_Stubs);
1310
1311 -- Loop through ELSIF parts if present
1312
1313 if Present (Elsif_Parts (N)) then
1314 declare
1315 Elif : Node_Id := First (Elsif_Parts (N));
1316
1317 begin
1318 while Present (Elif) loop
1319 Traverse_Declarations_Or_Statements
1320 (Then_Statements (Elif), Process, Inside_Stubs);
1321 Next (Elif);
1322 end loop;
1323 end;
1324 end if;
1325
1326 -- Finally traverse the ELSE statements if present
1327
1328 Traverse_Declarations_Or_Statements
1329 (Else_Statements (N), Process, Inside_Stubs);
1330
1331 -- Case statement
1332
1333 when N_Case_Statement =>
1334
1335 -- Process case branches
1336
1337 declare
1338 Alt : Node_Id;
1339 begin
1340 Alt := First (Alternatives (N));
1341 while Present (Alt) loop
1342 Traverse_Declarations_Or_Statements
1343 (Statements (Alt), Process, Inside_Stubs);
1344 Next (Alt);
1345 end loop;
1346 end;
1347
1348 -- Extended return statement
1349
1350 when N_Extended_Return_Statement =>
1351 Traverse_Handled_Statement_Sequence
1352 (Handled_Statement_Sequence (N), Process, Inside_Stubs);
1353
1354 -- Loop
1355
1356 when N_Loop_Statement =>
1357 Traverse_Declarations_Or_Statements
1358 (Statements (N), Process, Inside_Stubs);
1359
1360 -- Generic declarations are ignored
1361
1362 when others =>
1363 null;
1364 end case;
1365
1366 Next (N);
1367 end loop;
1368 end Traverse_Declarations_Or_Statements;
1369
1370 -----------------------------------------
1371 -- Traverse_Handled_Statement_Sequence --
1372 -----------------------------------------
1373
1374 procedure Traverse_Handled_Statement_Sequence
1375 (N : Node_Id;
1376 Process : Node_Processing;
1377 Inside_Stubs : Boolean)
1378 is
1379 Handler : Node_Id;
1380
1381 begin
1382 if Present (N) then
1383 Traverse_Declarations_Or_Statements
1384 (Statements (N), Process, Inside_Stubs);
1385
1386 if Present (Exception_Handlers (N)) then
1387 Handler := First (Exception_Handlers (N));
1388 while Present (Handler) loop
1389 Traverse_Declarations_Or_Statements
1390 (Statements (Handler), Process, Inside_Stubs);
1391 Next (Handler);
1392 end loop;
1393 end if;
1394 end if;
1395 end Traverse_Handled_Statement_Sequence;
1396
1397 ---------------------------
1398 -- Traverse_Package_Body --
1399 ---------------------------
1400
1401 procedure Traverse_Package_Body
1402 (N : Node_Id;
1403 Process : Node_Processing;
1404 Inside_Stubs : Boolean) is
1405 begin
1406 Traverse_Declarations_Or_Statements
1407 (Declarations (N), Process, Inside_Stubs);
1408 Traverse_Handled_Statement_Sequence
1409 (Handled_Statement_Sequence (N), Process, Inside_Stubs);
1410 end Traverse_Package_Body;
1411
1412 ----------------------------------
1413 -- Traverse_Package_Declaration --
1414 ----------------------------------
1415
1416 procedure Traverse_Package_Declaration
1417 (N : Node_Id;
1418 Process : Node_Processing;
1419 Inside_Stubs : Boolean)
1420 is
1421 Spec : constant Node_Id := Specification (N);
1422 begin
1423 Traverse_Declarations_Or_Statements
1424 (Visible_Declarations (Spec), Process, Inside_Stubs);
1425 Traverse_Declarations_Or_Statements
1426 (Private_Declarations (Spec), Process, Inside_Stubs);
1427 end Traverse_Package_Declaration;
1428
1429 ------------------------------
1430 -- Traverse_Subprogram_Body --
1431 ------------------------------
1432
1433 procedure Traverse_Subprogram_Body
1434 (N : Node_Id;
1435 Process : Node_Processing;
1436 Inside_Stubs : Boolean)
1437 is
1438 begin
1439 Traverse_Declarations_Or_Statements
1440 (Declarations (N), Process, Inside_Stubs);
1441 Traverse_Handled_Statement_Sequence
1442 (Handled_Statement_Sequence (N), Process, Inside_Stubs);
1443 end Traverse_Subprogram_Body;
1444
1445 end SPARK_Specific;
Mirror of the offical gcc git repository hosted at gcc.gnu.org