1 ------------------------------------------------------------------------------
3 -- GNAT COMPILER COMPONENTS --
5 -- L I B . X R E F . S P A R K _ S P E C I F I C --
9 -- Copyright (C) 2011-2019, Free Software Foundation, Inc. --
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. --
21 -- GNAT was originally developed by the GNAT team at New York University. --
22 -- Extensive contributions were provided by Ada Core Technologies Inc. --
24 ------------------------------------------------------------------------------
26 with Einfo; use Einfo;
27 with Nmake; use Nmake;
28 with SPARK_Xrefs; use SPARK_Xrefs;
31 package body SPARK_Specific is
37 -- Table of SPARK_Entities, True for each entity kind used in SPARK
39 SPARK_Entities : constant array (Entity_Kind) of Boolean :=
43 E_In_Out_Parameter => True,
44 E_In_Parameter => True,
45 E_Loop_Parameter => True,
47 E_Out_Parameter => True,
52 -- True for each reference type used in SPARK
54 SPARK_References : constant array (Character) of Boolean :=
64 package Drefs is new Table.Table (
65 Table_Component_Type => Xref_Entry,
66 Table_Index_Type => Xref_Entry_Number,
68 Table_Initial => Alloc.Drefs_Initial,
69 Table_Increment => Alloc.Drefs_Increment,
70 Table_Name => "Drefs");
71 -- Table of cross-references for reads and writes through explicit
72 -- dereferences, that are output as reads/writes to the special variable
73 -- "Heap". These references are added to the regular references when
74 -- computing SPARK cross-references.
76 -------------------------
77 -- Iterate_SPARK_Xrefs --
78 -------------------------
80 procedure Iterate_SPARK_Xrefs is
82 procedure Add_SPARK_Xref (Index : Int; Xref : Xref_Entry);
84 function Is_SPARK_Reference
86 Typ : Character) return Boolean;
87 -- Return whether entity reference E meets SPARK requirements. Typ is
88 -- the reference type.
90 function Is_SPARK_Scope (E : Entity_Id) return Boolean;
91 -- Return whether the entity or reference scope meets requirements for
92 -- being a SPARK scope.
98 procedure Add_SPARK_Xref (Index : Int; Xref : Xref_Entry) is
99 Ref : Xref_Key renames Xref.Key;
101 -- Eliminate entries not appropriate for SPARK
103 if SPARK_Entities (Ekind (Ref.Ent))
104 and then SPARK_References (Ref.Typ)
105 and then Is_SPARK_Scope (Ref.Ent_Scope)
106 and then Is_SPARK_Scope (Ref.Ref_Scope)
107 and then Is_SPARK_Reference (Ref.Ent, Ref.Typ)
112 Ref_Scope => Ref.Ref_Scope,
118 ------------------------
119 -- Is_SPARK_Reference --
120 ------------------------
122 function Is_SPARK_Reference
124 Typ : Character) return Boolean
127 -- The only references of interest on callable entities are calls. On
128 -- uncallable entities, the only references of interest are reads and
131 if Ekind (E) in Overloadable_Kind then
134 -- In all other cases, result is true for reference/modify cases,
135 -- and false for all other cases.
138 return Typ = 'r' or else Typ = 'm';
140 end Is_SPARK_Reference;
146 function Is_SPARK_Scope (E : Entity_Id) return Boolean is
147 Can_Be_Renamed : constant Boolean :=
149 and then (Is_Subprogram_Or_Entry (E)
150 or else Ekind (E) = E_Package);
153 and then not Is_Generic_Unit (E)
154 and then (not Can_Be_Renamed or else No (Renamed_Entity (E)));
157 -- Start of processing for Add_SPARK_Xrefs
160 -- Expose cross-references from private frontend tables to the backend
162 for Index in Drefs.First .. Drefs.Last loop
163 Add_SPARK_Xref (Index, Drefs.Table (Index));
166 for Index in Xrefs.First .. Xrefs.Last loop
167 Add_SPARK_Xref (-Index, Xrefs.Table (Index));
169 end Iterate_SPARK_Xrefs;
171 ---------------------------------------------
172 -- Enclosing_Subprogram_Or_Library_Package --
173 ---------------------------------------------
175 function Enclosing_Subprogram_Or_Library_Package
176 (N : Node_Id) return Entity_Id
181 -- If N is the defining identifier for a subprogram, then return the
182 -- enclosing subprogram or package, not this subprogram.
184 if Nkind_In (N, N_Defining_Identifier, N_Defining_Operator_Symbol)
185 and then (Ekind (N) in Entry_Kind
186 or else Ekind (N) = E_Subprogram_Body
187 or else Ekind (N) in Generic_Subprogram_Kind
188 or else Ekind (N) in Subprogram_Kind)
190 Context := Parent (Unit_Declaration_Node (N));
192 -- If this was a library-level subprogram then replace Context with
193 -- its Unit, which points to N_Subprogram_* node.
195 if Nkind (Context) = N_Compilation_Unit then
196 Context := Unit (Context);
202 while Present (Context) loop
203 case Nkind (Context) is
205 | N_Package_Specification
207 -- Only return a library-level package
209 if Is_Library_Level_Entity (Defining_Entity (Context)) then
210 Context := Defining_Entity (Context);
213 Context := Parent (Context);
218 -- The enclosing subprogram for a precondition, postcondition,
219 -- or contract case should be the declaration preceding the
220 -- pragma (skipping any other pragmas between this pragma and
223 while Nkind (Context) = N_Pragma
224 and then Is_List_Member (Context)
225 and then Present (Prev (Context))
227 Context := Prev (Context);
230 if Nkind (Context) = N_Pragma then
232 -- When used for cross-references then aspects might not be
233 -- yet linked to pragmas; when used for AST navigation in
234 -- GNATprove this routine is expected to follow those links.
236 if From_Aspect_Specification (Context) then
237 Context := Corresponding_Aspect (Context);
238 pragma Assert (Nkind (Context) = N_Aspect_Specification);
239 Context := Entity (Context);
241 Context := Parent (Context);
246 | N_Entry_Declaration
247 | N_Protected_Type_Declaration
249 | N_Subprogram_Declaration
250 | N_Subprogram_Specification
252 | N_Task_Type_Declaration
254 Context := Defining_Entity (Context);
258 Context := Parent (Context);
262 if Nkind (Context) = N_Defining_Program_Unit_Name then
263 Context := Defining_Identifier (Context);
266 -- Do not return a scope without a proper location
269 and then Sloc (Context) = No_Location
275 end Enclosing_Subprogram_Or_Library_Package;
277 --------------------------
278 -- Generate_Dereference --
279 --------------------------
281 procedure Generate_Dereference
283 Typ : Character := 'r')
285 procedure Create_Heap;
286 -- Create and decorate the special entity which denotes the heap
292 procedure Create_Heap is
294 Name_Len := Name_Of_Heap_Variable'Length;
295 Name_Buffer (1 .. Name_Len) := Name_Of_Heap_Variable;
297 Heap := Make_Defining_Identifier (Standard_Location, Name_Enter);
299 Set_Ekind (Heap, E_Variable);
300 Set_Is_Internal (Heap, True);
301 Set_Etype (Heap, Standard_Void_Type);
302 Set_Scope (Heap, Standard_Standard);
303 Set_Has_Fully_Qualified_Name (Heap);
308 Loc : constant Source_Ptr := Sloc (N);
310 -- Start of processing for Generate_Dereference
313 if Loc > No_Location then
314 Drefs.Increment_Last;
317 Deref_Entry : Xref_Entry renames Drefs.Table (Drefs.Last);
318 Deref : Xref_Key renames Deref_Entry.Key;
329 -- It is as if the special "Heap" was defined in the main unit,
330 -- in the scope of the entity for the main unit. This single
331 -- definition point is required to ensure that sorting cross
332 -- references works for "Heap" references as well.
334 Deref.Eun := Main_Unit;
335 Deref.Lun := Get_Top_Level_Code_Unit (Loc);
337 Deref.Ref_Scope := Enclosing_Subprogram_Or_Library_Package (N);
338 Deref.Ent_Scope := Cunit_Entity (Main_Unit);
340 Deref_Entry.Def := No_Location;
342 Deref_Entry.Ent_Scope_File := Main_Unit;
345 end Generate_Dereference;