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