|
111
|
1 ------------------------------------------------------------------------------
|
|
|
2 -- --
|
|
|
3 -- GNAT COMPILER COMPONENTS --
|
|
|
4 -- --
|
|
|
5 -- E X P _ S P A R K --
|
|
|
6 -- --
|
|
|
7 -- B o d y --
|
|
|
8 -- --
|
|
131
|
9 -- Copyright (C) 1992-2018, Free Software Foundation, Inc. --
|
|
111
|
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 Atree; use Atree;
|
|
|
27 with Checks; use Checks;
|
|
|
28 with Einfo; use Einfo;
|
|
|
29 with Exp_Ch4;
|
|
|
30 with Exp_Ch5; use Exp_Ch5;
|
|
|
31 with Exp_Dbug; use Exp_Dbug;
|
|
|
32 with Exp_Util; use Exp_Util;
|
|
|
33 with Namet; use Namet;
|
|
|
34 with Nlists; use Nlists;
|
|
|
35 with Nmake; use Nmake;
|
|
|
36 with Rtsfind; use Rtsfind;
|
|
|
37 with Sem; use Sem;
|
|
|
38 with Sem_Eval; use Sem_Eval;
|
|
|
39 with Sem_Prag; use Sem_Prag;
|
|
|
40 with Sem_Res; use Sem_Res;
|
|
|
41 with Sem_Util; use Sem_Util;
|
|
|
42 with Sinfo; use Sinfo;
|
|
|
43 with Snames; use Snames;
|
|
|
44 with Stand; use Stand;
|
|
|
45 with Tbuild; use Tbuild;
|
|
|
46 with Uintp; use Uintp;
|
|
|
47
|
|
|
48 package body Exp_SPARK is
|
|
|
49
|
|
|
50 -----------------------
|
|
|
51 -- Local Subprograms --
|
|
|
52 -----------------------
|
|
|
53
|
|
|
54 procedure Expand_SPARK_N_Attribute_Reference (N : Node_Id);
|
|
|
55 -- Replace occurrences of System'To_Address by calls to
|
|
|
56 -- System.Storage_Elements.To_Address
|
|
|
57
|
|
|
58 procedure Expand_SPARK_N_Freeze_Type (E : Entity_Id);
|
|
|
59 -- Build the DIC procedure of a type when needed, if not already done
|
|
|
60
|
|
|
61 procedure Expand_SPARK_N_Indexed_Component (N : Node_Id);
|
|
|
62 -- Insert explicit dereference if required
|
|
|
63
|
|
|
64 procedure Expand_SPARK_N_Loop_Statement (N : Node_Id);
|
|
|
65 -- Perform loop statement-specific expansion
|
|
|
66
|
|
|
67 procedure Expand_SPARK_N_Object_Declaration (N : Node_Id);
|
|
|
68 -- Perform object-declaration-specific expansion
|
|
|
69
|
|
|
70 procedure Expand_SPARK_N_Object_Renaming_Declaration (N : Node_Id);
|
|
|
71 -- Perform name evaluation for a renamed object
|
|
|
72
|
|
|
73 procedure Expand_SPARK_N_Op_Ne (N : Node_Id);
|
|
|
74 -- Rewrite operator /= based on operator = when defined explicitly
|
|
|
75
|
|
|
76 procedure Expand_SPARK_N_Selected_Component (N : Node_Id);
|
|
|
77 -- Insert explicit dereference if required
|
|
|
78
|
|
|
79 ------------------
|
|
|
80 -- Expand_SPARK --
|
|
|
81 ------------------
|
|
|
82
|
|
|
83 procedure Expand_SPARK (N : Node_Id) is
|
|
|
84 begin
|
|
|
85 case Nkind (N) is
|
|
|
86
|
|
|
87 -- Qualification of entity names in formal verification mode
|
|
|
88 -- is limited to the addition of a suffix for homonyms (see
|
|
|
89 -- Exp_Dbug.Qualify_Entity_Name). We used to qualify entity names
|
|
|
90 -- as full expansion does, but this was removed as this prevents the
|
|
|
91 -- verification back-end from using a short name for debugging and
|
|
|
92 -- user interaction. The verification back-end already takes care
|
|
|
93 -- of qualifying names when needed.
|
|
|
94
|
|
|
95 when N_Block_Statement
|
|
|
96 | N_Entry_Declaration
|
|
|
97 | N_Package_Body
|
|
|
98 | N_Package_Declaration
|
|
|
99 | N_Protected_Type_Declaration
|
|
|
100 | N_Subprogram_Body
|
|
|
101 | N_Task_Type_Declaration
|
|
|
102 =>
|
|
|
103 Qualify_Entity_Names (N);
|
|
|
104
|
|
|
105 -- Replace occurrences of System'To_Address by calls to
|
|
|
106 -- System.Storage_Elements.To_Address.
|
|
|
107
|
|
|
108 when N_Attribute_Reference =>
|
|
|
109 Expand_SPARK_N_Attribute_Reference (N);
|
|
|
110
|
|
|
111 when N_Expanded_Name
|
|
|
112 | N_Identifier
|
|
|
113 =>
|
|
|
114 Expand_SPARK_Potential_Renaming (N);
|
|
|
115
|
|
|
116 -- Loop iterations over arrays need to be expanded, to avoid getting
|
|
|
117 -- two names referring to the same object in memory (the array and
|
|
|
118 -- the iterator) in GNATprove, especially since both can be written
|
|
|
119 -- (thus possibly leading to interferences due to aliasing). No such
|
|
|
120 -- problem arises with quantified expressions over arrays, which are
|
|
|
121 -- dealt with specially in GNATprove.
|
|
|
122
|
|
|
123 when N_Loop_Statement =>
|
|
|
124 Expand_SPARK_N_Loop_Statement (N);
|
|
|
125
|
|
|
126 when N_Object_Declaration =>
|
|
|
127 Expand_SPARK_N_Object_Declaration (N);
|
|
|
128
|
|
|
129 when N_Object_Renaming_Declaration =>
|
|
|
130 Expand_SPARK_N_Object_Renaming_Declaration (N);
|
|
|
131
|
|
|
132 when N_Op_Ne =>
|
|
|
133 Expand_SPARK_N_Op_Ne (N);
|
|
|
134
|
|
|
135 when N_Freeze_Entity =>
|
|
|
136 if Is_Type (Entity (N)) then
|
|
|
137 Expand_SPARK_N_Freeze_Type (Entity (N));
|
|
|
138 end if;
|
|
|
139
|
|
|
140 when N_Indexed_Component =>
|
|
|
141 Expand_SPARK_N_Indexed_Component (N);
|
|
|
142
|
|
|
143 when N_Selected_Component =>
|
|
|
144 Expand_SPARK_N_Selected_Component (N);
|
|
|
145
|
|
|
146 -- In SPARK mode, no other constructs require expansion
|
|
|
147
|
|
|
148 when others =>
|
|
|
149 null;
|
|
|
150 end case;
|
|
|
151 end Expand_SPARK;
|
|
|
152
|
|
|
153 --------------------------------
|
|
|
154 -- Expand_SPARK_N_Freeze_Type --
|
|
|
155 --------------------------------
|
|
|
156
|
|
|
157 procedure Expand_SPARK_N_Freeze_Type (E : Entity_Id) is
|
|
|
158 begin
|
|
|
159 -- When a DIC is inherited by a tagged type, it may need to be
|
|
|
160 -- specialized to the descendant type, hence build a separate DIC
|
|
|
161 -- procedure for it as done during regular expansion for compilation.
|
|
|
162
|
|
|
163 if Has_DIC (E) and then Is_Tagged_Type (E) then
|
|
|
164 Build_DIC_Procedure_Body (E, For_Freeze => True);
|
|
|
165 end if;
|
|
|
166 end Expand_SPARK_N_Freeze_Type;
|
|
|
167
|
|
|
168 ----------------------------------------
|
|
|
169 -- Expand_SPARK_N_Attribute_Reference --
|
|
|
170 ----------------------------------------
|
|
|
171
|
|
|
172 procedure Expand_SPARK_N_Attribute_Reference (N : Node_Id) is
|
|
|
173 Aname : constant Name_Id := Attribute_Name (N);
|
|
|
174 Attr_Id : constant Attribute_Id := Get_Attribute_Id (Aname);
|
|
|
175 Loc : constant Source_Ptr := Sloc (N);
|
|
|
176 Typ : constant Entity_Id := Etype (N);
|
|
|
177 Expr : Node_Id;
|
|
|
178
|
|
|
179 begin
|
|
|
180 if Attr_Id = Attribute_To_Address then
|
|
|
181
|
|
|
182 -- Extract and convert argument to expected type for call
|
|
|
183
|
|
|
184 Expr :=
|
|
|
185 Make_Type_Conversion (Loc,
|
|
|
186 Subtype_Mark =>
|
|
|
187 New_Occurrence_Of (RTE (RE_Integer_Address), Loc),
|
|
|
188 Expression => Relocate_Node (First (Expressions (N))));
|
|
|
189
|
|
|
190 -- Replace attribute reference with call
|
|
|
191
|
|
|
192 Rewrite (N,
|
|
|
193 Make_Function_Call (Loc,
|
|
|
194 Name =>
|
|
|
195 New_Occurrence_Of (RTE (RE_To_Address), Loc),
|
|
|
196 Parameter_Associations => New_List (Expr)));
|
|
|
197 Analyze_And_Resolve (N, Typ);
|
|
|
198
|
|
|
199 -- For attributes which return Universal_Integer, introduce a conversion
|
|
|
200 -- to the expected type with the appropriate check flags set.
|
|
|
201
|
|
|
202 elsif Attr_Id = Attribute_Alignment
|
|
|
203 or else Attr_Id = Attribute_Bit
|
|
|
204 or else Attr_Id = Attribute_Bit_Position
|
|
|
205 or else Attr_Id = Attribute_Descriptor_Size
|
|
|
206 or else Attr_Id = Attribute_First_Bit
|
|
|
207 or else Attr_Id = Attribute_Last_Bit
|
|
|
208 or else Attr_Id = Attribute_Length
|
|
|
209 or else Attr_Id = Attribute_Max_Size_In_Storage_Elements
|
|
|
210 or else Attr_Id = Attribute_Pos
|
|
|
211 or else Attr_Id = Attribute_Position
|
|
|
212 or else Attr_Id = Attribute_Range_Length
|
|
|
213 or else Attr_Id = Attribute_Object_Size
|
|
|
214 or else Attr_Id = Attribute_Size
|
|
|
215 or else Attr_Id = Attribute_Value_Size
|
|
|
216 or else Attr_Id = Attribute_VADS_Size
|
|
|
217 or else Attr_Id = Attribute_Aft
|
|
|
218 or else Attr_Id = Attribute_Max_Alignment_For_Allocation
|
|
|
219 then
|
|
|
220 -- If the expected type is Long_Long_Integer, there will be no check
|
|
|
221 -- flag as the compiler assumes attributes always fit in this type.
|
|
|
222 -- Since in SPARK_Mode we do not take Storage_Error into account, we
|
|
|
223 -- cannot make this assumption and need to produce a check.
|
|
|
224 -- ??? It should be enough to add this check for attributes 'Length
|
|
|
225 -- and 'Range_Length when the type is as big as Long_Long_Integer.
|
|
|
226
|
|
|
227 declare
|
|
|
228 Typ : Entity_Id := Empty;
|
|
|
229 begin
|
|
|
230 if Attr_Id = Attribute_Range_Length then
|
|
|
231 Typ := Etype (Prefix (N));
|
|
|
232
|
|
|
233 elsif Attr_Id = Attribute_Length then
|
|
|
234 Typ := Etype (Prefix (N));
|
|
|
235
|
|
|
236 declare
|
|
|
237 Indx : Node_Id;
|
|
|
238 J : Int;
|
|
|
239
|
|
|
240 begin
|
|
|
241 if Is_Access_Type (Typ) then
|
|
|
242 Typ := Designated_Type (Typ);
|
|
|
243 end if;
|
|
|
244
|
|
|
245 if No (Expressions (N)) then
|
|
|
246 J := 1;
|
|
|
247 else
|
|
|
248 J := UI_To_Int (Expr_Value (First (Expressions (N))));
|
|
|
249 end if;
|
|
|
250
|
|
|
251 Indx := First_Index (Typ);
|
|
|
252 while J > 1 loop
|
|
|
253 Next_Index (Indx);
|
|
|
254 J := J - 1;
|
|
|
255 end loop;
|
|
|
256
|
|
|
257 Typ := Etype (Indx);
|
|
|
258 end;
|
|
|
259 end if;
|
|
|
260
|
|
|
261 Apply_Universal_Integer_Attribute_Checks (N);
|
|
|
262
|
|
|
263 if Present (Typ)
|
|
|
264 and then RM_Size (Typ) = RM_Size (Standard_Long_Long_Integer)
|
|
|
265 then
|
|
|
266 Set_Do_Overflow_Check (N);
|
|
|
267 end if;
|
|
|
268 end;
|
|
|
269 end if;
|
|
|
270 end Expand_SPARK_N_Attribute_Reference;
|
|
|
271
|
|
|
272 -----------------------------------
|
|
|
273 -- Expand_SPARK_N_Loop_Statement --
|
|
|
274 -----------------------------------
|
|
|
275
|
|
|
276 procedure Expand_SPARK_N_Loop_Statement (N : Node_Id) is
|
|
|
277 Scheme : constant Node_Id := Iteration_Scheme (N);
|
|
|
278
|
|
|
279 begin
|
|
|
280 -- Loop iterations over arrays need to be expanded, to avoid getting
|
|
|
281 -- two names referring to the same object in memory (the array and the
|
|
|
282 -- iterator) in GNATprove, especially since both can be written (thus
|
|
|
283 -- possibly leading to interferences due to aliasing). No such problem
|
|
|
284 -- arises with quantified expressions over arrays, which are dealt with
|
|
|
285 -- specially in GNATprove.
|
|
|
286
|
|
|
287 if Present (Scheme)
|
|
|
288 and then Present (Iterator_Specification (Scheme))
|
|
|
289 and then Is_Iterator_Over_Array (Iterator_Specification (Scheme))
|
|
|
290 then
|
|
|
291 Expand_Iterator_Loop_Over_Array (N);
|
|
|
292 end if;
|
|
|
293 end Expand_SPARK_N_Loop_Statement;
|
|
|
294
|
|
|
295 --------------------------------------
|
|
|
296 -- Expand_SPARK_N_Indexed_Component --
|
|
|
297 --------------------------------------
|
|
|
298
|
|
|
299 procedure Expand_SPARK_N_Indexed_Component (N : Node_Id) is
|
|
|
300 Pref : constant Node_Id := Prefix (N);
|
|
|
301 Typ : constant Entity_Id := Etype (Pref);
|
|
|
302
|
|
|
303 begin
|
|
|
304 if Is_Access_Type (Typ) then
|
|
|
305 Insert_Explicit_Dereference (Pref);
|
|
|
306 Analyze_And_Resolve (Pref, Designated_Type (Typ));
|
|
|
307 end if;
|
|
|
308 end Expand_SPARK_N_Indexed_Component;
|
|
|
309
|
|
|
310 ---------------------------------------
|
|
|
311 -- Expand_SPARK_N_Object_Declaration --
|
|
|
312 ---------------------------------------
|
|
|
313
|
|
|
314 procedure Expand_SPARK_N_Object_Declaration (N : Node_Id) is
|
|
|
315 Loc : constant Source_Ptr := Sloc (N);
|
|
|
316 Obj_Id : constant Entity_Id := Defining_Identifier (N);
|
|
|
317 Typ : constant Entity_Id := Etype (Obj_Id);
|
|
|
318
|
|
|
319 Call : Node_Id;
|
|
|
320
|
|
|
321 begin
|
|
|
322 -- If the object declaration denotes a variable without initialization
|
|
|
323 -- whose type is subject to pragma Default_Initial_Condition, create
|
|
|
324 -- and analyze a dummy call to the DIC procedure of the type in order
|
|
|
325 -- to detect potential elaboration issues.
|
|
|
326
|
|
|
327 if Comes_From_Source (Obj_Id)
|
|
|
328 and then Ekind (Obj_Id) = E_Variable
|
|
|
329 and then Has_DIC (Typ)
|
|
|
330 and then Present (DIC_Procedure (Typ))
|
|
|
331 and then not Has_Init_Expression (N)
|
|
|
332 then
|
|
|
333 Call := Build_DIC_Call (Loc, Obj_Id, Typ);
|
|
|
334
|
|
|
335 -- Partially insert the call into the tree by setting its parent
|
|
|
336 -- pointer.
|
|
|
337
|
|
|
338 Set_Parent (Call, N);
|
|
|
339 Analyze (Call);
|
|
|
340 end if;
|
|
|
341 end Expand_SPARK_N_Object_Declaration;
|
|
|
342
|
|
|
343 ------------------------------------------------
|
|
|
344 -- Expand_SPARK_N_Object_Renaming_Declaration --
|
|
|
345 ------------------------------------------------
|
|
|
346
|
|
|
347 procedure Expand_SPARK_N_Object_Renaming_Declaration (N : Node_Id) is
|
|
|
348 CFS : constant Boolean := Comes_From_Source (N);
|
|
|
349 Loc : constant Source_Ptr := Sloc (N);
|
|
|
350 Obj_Id : constant Entity_Id := Defining_Entity (N);
|
|
|
351 Nam : constant Node_Id := Name (N);
|
|
131
|
352 Typ : constant Entity_Id := Etype (Obj_Id);
|
|
111
|
353
|
|
|
354 begin
|
|
|
355 -- Transform a renaming of the form
|
|
|
356
|
|
|
357 -- Obj_Id : <subtype mark> renames <function call>;
|
|
|
358
|
|
|
359 -- into
|
|
|
360
|
|
|
361 -- Obj_Id : constant <subtype mark> := <function call>;
|
|
|
362
|
|
|
363 -- Invoking Evaluate_Name and ultimately Remove_Side_Effects introduces
|
|
|
364 -- a temporary to capture the function result. Once potential renamings
|
|
|
365 -- are rewritten for SPARK, the temporary may be leaked out into source
|
|
|
366 -- constructs and lead to confusing error diagnostics. Using an object
|
|
|
367 -- declaration prevents this unwanted side effect.
|
|
|
368
|
|
|
369 if Nkind (Nam) = N_Function_Call then
|
|
|
370 Rewrite (N,
|
|
|
371 Make_Object_Declaration (Loc,
|
|
|
372 Defining_Identifier => Obj_Id,
|
|
|
373 Constant_Present => True,
|
|
|
374 Object_Definition => New_Occurrence_Of (Typ, Loc),
|
|
|
375 Expression => Nam));
|
|
|
376
|
|
|
377 -- Inherit the original Comes_From_Source status of the renaming
|
|
|
378
|
|
|
379 Set_Comes_From_Source (N, CFS);
|
|
|
380
|
|
|
381 -- Sever the link to the renamed function result because the entity
|
|
|
382 -- will no longer alias anything.
|
|
|
383
|
|
|
384 Set_Renamed_Object (Obj_Id, Empty);
|
|
|
385
|
|
|
386 -- Remove the entity of the renaming declaration from visibility as
|
|
|
387 -- the analysis of the object declaration will reintroduce it again.
|
|
|
388
|
|
131
|
389 Remove_Entity_And_Homonym (Obj_Id);
|
|
111
|
390 Analyze (N);
|
|
|
391
|
|
|
392 -- Otherwise unconditionally remove all side effects from the name
|
|
|
393
|
|
|
394 else
|
|
|
395 Evaluate_Name (Nam);
|
|
|
396 end if;
|
|
|
397 end Expand_SPARK_N_Object_Renaming_Declaration;
|
|
|
398
|
|
|
399 --------------------------
|
|
|
400 -- Expand_SPARK_N_Op_Ne --
|
|
|
401 --------------------------
|
|
|
402
|
|
|
403 procedure Expand_SPARK_N_Op_Ne (N : Node_Id) is
|
|
|
404 Typ : constant Entity_Id := Etype (Left_Opnd (N));
|
|
|
405
|
|
|
406 begin
|
|
|
407 -- Case of elementary type with standard operator
|
|
|
408
|
|
|
409 if Is_Elementary_Type (Typ)
|
|
|
410 and then Sloc (Entity (N)) = Standard_Location
|
|
|
411 then
|
|
|
412 null;
|
|
|
413
|
|
|
414 else
|
|
|
415 Exp_Ch4.Expand_N_Op_Ne (N);
|
|
|
416 end if;
|
|
|
417 end Expand_SPARK_N_Op_Ne;
|
|
|
418
|
|
|
419 -------------------------------------
|
|
|
420 -- Expand_SPARK_Potential_Renaming --
|
|
|
421 -------------------------------------
|
|
|
422
|
|
|
423 procedure Expand_SPARK_Potential_Renaming (N : Node_Id) is
|
|
|
424 function In_Insignificant_Pragma (Nod : Node_Id) return Boolean;
|
|
|
425 -- Determine whether arbitrary node Nod appears within a significant
|
|
|
426 -- pragma for SPARK.
|
|
|
427
|
|
|
428 -----------------------------
|
|
|
429 -- In_Insignificant_Pragma --
|
|
|
430 -----------------------------
|
|
|
431
|
|
|
432 function In_Insignificant_Pragma (Nod : Node_Id) return Boolean is
|
|
|
433 Par : Node_Id;
|
|
|
434
|
|
|
435 begin
|
|
|
436 -- Climb the parent chain looking for an enclosing pragma
|
|
|
437
|
|
|
438 Par := Nod;
|
|
|
439 while Present (Par) loop
|
|
|
440 if Nkind (Par) = N_Pragma then
|
|
|
441 return not Pragma_Significant_In_SPARK (Get_Pragma_Id (Par));
|
|
|
442
|
|
|
443 -- Prevent the search from going too far
|
|
|
444
|
|
|
445 elsif Is_Body_Or_Package_Declaration (Par) then
|
|
|
446 exit;
|
|
|
447 end if;
|
|
|
448
|
|
|
449 Par := Parent (Par);
|
|
|
450 end loop;
|
|
|
451
|
|
|
452 return False;
|
|
|
453 end In_Insignificant_Pragma;
|
|
|
454
|
|
|
455 -- Local variables
|
|
|
456
|
|
|
457 Loc : constant Source_Ptr := Sloc (N);
|
|
|
458 Obj_Id : constant Entity_Id := Entity (N);
|
|
|
459 Typ : constant Entity_Id := Etype (N);
|
|
|
460 Ren : Node_Id;
|
|
|
461
|
|
|
462 -- Start of processing for Expand_SPARK_Potential_Renaming
|
|
|
463
|
|
|
464 begin
|
|
|
465 -- Replace a reference to a renaming with the actual renamed object
|
|
|
466
|
|
|
467 if Ekind (Obj_Id) in Object_Kind then
|
|
|
468 Ren := Renamed_Object (Obj_Id);
|
|
|
469
|
|
|
470 if Present (Ren) then
|
|
|
471
|
|
|
472 -- Do not process a reference when it appears within a pragma of
|
|
|
473 -- no significance to SPARK. It is assumed that the replacement
|
|
|
474 -- will violate the semantics of the pragma and cause a spurious
|
|
|
475 -- error.
|
|
|
476
|
|
|
477 if In_Insignificant_Pragma (N) then
|
|
|
478 return;
|
|
|
479
|
|
|
480 -- Instantiations and inlining of subprograms employ "prologues"
|
|
|
481 -- which map actual to formal parameters by means of renamings.
|
|
|
482 -- Replace a reference to a formal by the corresponding actual
|
|
|
483 -- parameter.
|
|
|
484
|
|
|
485 elsif Nkind (Ren) in N_Entity then
|
|
|
486 Rewrite (N, New_Occurrence_Of (Ren, Loc));
|
|
|
487
|
|
|
488 -- Otherwise the renamed object denotes a name
|
|
|
489
|
|
|
490 else
|
|
|
491 Rewrite (N, New_Copy_Tree (Ren, New_Sloc => Loc));
|
|
|
492 Reset_Analyzed_Flags (N);
|
|
|
493 end if;
|
|
|
494
|
|
|
495 Analyze_And_Resolve (N, Typ);
|
|
|
496 end if;
|
|
|
497 end if;
|
|
|
498 end Expand_SPARK_Potential_Renaming;
|
|
|
499
|
|
|
500 ---------------------------------------
|
|
|
501 -- Expand_SPARK_N_Selected_Component --
|
|
|
502 ---------------------------------------
|
|
|
503
|
|
|
504 procedure Expand_SPARK_N_Selected_Component (N : Node_Id) is
|
|
|
505 Pref : constant Node_Id := Prefix (N);
|
|
|
506 Typ : constant Entity_Id := Underlying_Type (Etype (Pref));
|
|
|
507
|
|
|
508 begin
|
|
|
509 if Present (Typ) and then Is_Access_Type (Typ) then
|
|
|
510
|
|
|
511 -- First set prefix type to proper access type, in case it currently
|
|
|
512 -- has a private (non-access) view of this type.
|
|
|
513
|
|
|
514 Set_Etype (Pref, Typ);
|
|
|
515
|
|
|
516 Insert_Explicit_Dereference (Pref);
|
|
|
517 Analyze_And_Resolve (Pref, Designated_Type (Typ));
|
|
|
518
|
|
|
519 if Ekind (Etype (Pref)) = E_Private_Subtype
|
|
|
520 and then Is_For_Access_Subtype (Etype (Pref))
|
|
|
521 then
|
|
|
522 Set_Etype (Pref, Base_Type (Etype (Pref)));
|
|
|
523 end if;
|
|
|
524 end if;
|
|
|
525 end Expand_SPARK_N_Selected_Component;
|
|
|
526
|
|
|
527 end Exp_SPARK;
|
