projects / gcc.git / blob
? search:
summary | shortlog | log | commit | commitdiff | tree
history | raw | HEAD
[Ada] Fix SPARK expansion of iterated_component_assoc in delta aggregate
[gcc.git] / gcc / ada / exp_spark.adb
1 ------------------------------------------------------------------------------
2 -- --
3 -- GNAT COMPILER COMPONENTS --
4 -- --
5 -- E X P _ S P A R K --
6 -- --
7 -- B o d y --
8 -- --
9 -- Copyright (C) 1992-2020, 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 Atree; use Atree;
27 with Checks; use Checks;
28 with Einfo; use Einfo;
29 with Exp_Attr;
30 with Exp_Ch4;
31 with Exp_Ch5; use Exp_Ch5;
32 with Exp_Dbug; use Exp_Dbug;
33 with Exp_Util; use Exp_Util;
34 with Namet; use Namet;
35 with Nlists; use Nlists;
36 with Nmake; use Nmake;
37 with Rtsfind; use Rtsfind;
38 with Sem; use Sem;
39 with Sem_Ch8; use Sem_Ch8;
40 with Sem_Prag; use Sem_Prag;
41 with Sem_Res; use Sem_Res;
42 with Sem_Util; use Sem_Util;
43 with Sinfo; use Sinfo;
44 with Snames; use Snames;
45 with Stand; use Stand;
46 with Tbuild; use Tbuild;
47 with Uintp; use Uintp;
48
49 package body Exp_SPARK is
50
51 -----------------------
52 -- Local Subprograms --
53 -----------------------
54
55 procedure Expand_SPARK_N_Aggregate (N : Node_Id);
56 -- Perform aggregate-specific expansion
57
58 procedure Expand_SPARK_N_Attribute_Reference (N : Node_Id);
59 -- Perform attribute-reference-specific expansion
60
61 procedure Expand_SPARK_N_Delta_Aggregate (N : Node_Id);
62 -- Perform delta-aggregate-specific expansion
63
64 procedure Expand_SPARK_N_Freeze_Type (E : Entity_Id);
65 -- Build the DIC procedure of a type when needed, if not already done
66
67 procedure Expand_SPARK_N_Loop_Statement (N : Node_Id);
68 -- Perform loop-statement-specific expansion
69
70 procedure Expand_SPARK_N_Object_Declaration (N : Node_Id);
71 -- Perform object-declaration-specific expansion
72
73 procedure Expand_SPARK_N_Object_Renaming_Declaration (N : Node_Id);
74 -- Perform name evaluation for a renamed object
75
76 procedure Expand_SPARK_N_Op_Ne (N : Node_Id);
77 -- Rewrite operator /= based on operator = when defined explicitly
78
79 procedure Expand_SPARK_Delta_Or_Update (Typ : Entity_Id; Aggr : Node_Id);
80 -- Common expansion for attribute Update and delta aggregates
81
82 ------------------
83 -- Expand_SPARK --
84 ------------------
85
86 procedure Expand_SPARK (N : Node_Id) is
87 begin
88 case Nkind (N) is
89
90 -- Qualification of entity names in formal verification mode
91 -- is limited to the addition of a suffix for homonyms (see
92 -- Exp_Dbug.Qualify_Entity_Name). We used to qualify entity names
93 -- as full expansion does, but this was removed as this prevents the
94 -- verification back-end from using a short name for debugging and
95 -- user interaction. The verification back-end already takes care
96 -- of qualifying names when needed.
97
98 when N_Block_Statement
99 | N_Entry_Declaration
100 | N_Package_Body
101 | N_Package_Declaration
102 | N_Protected_Type_Declaration
103 | N_Subprogram_Body
104 | N_Task_Type_Declaration
105 =>
106 Qualify_Entity_Names (N);
107
108 when N_Aggregate =>
109 Expand_SPARK_N_Aggregate (N);
110
111 -- Replace occurrences of System'To_Address by calls to
112 -- System.Storage_Elements.To_Address.
113
114 when N_Attribute_Reference =>
115 Expand_SPARK_N_Attribute_Reference (N);
116
117 when N_Delta_Aggregate =>
118 Expand_SPARK_N_Delta_Aggregate (N);
119
120 when N_Expanded_Name
121 | N_Identifier
122 =>
123 Expand_SPARK_Potential_Renaming (N);
124
125 -- Loop iterations over arrays need to be expanded, to avoid getting
126 -- two names referring to the same object in memory (the array and
127 -- the iterator) in GNATprove, especially since both can be written
128 -- (thus possibly leading to interferences due to aliasing). No such
129 -- problem arises with quantified expressions over arrays, which are
130 -- dealt with specially in GNATprove.
131
132 when N_Loop_Statement =>
133 Expand_SPARK_N_Loop_Statement (N);
134
135 when N_Object_Declaration =>
136 Expand_SPARK_N_Object_Declaration (N);
137
138 when N_Object_Renaming_Declaration =>
139 Expand_SPARK_N_Object_Renaming_Declaration (N);
140
141 when N_Op_Ne =>
142 Expand_SPARK_N_Op_Ne (N);
143
144 when N_Freeze_Entity =>
145 if Is_Type (Entity (N)) then
146 Expand_SPARK_N_Freeze_Type (Entity (N));
147 end if;
148
149 -- In SPARK mode, no other constructs require expansion
150
151 when others =>
152 null;
153 end case;
154 end Expand_SPARK;
155
156 ----------------------------------
157 -- Expand_SPARK_Delta_Or_Update --
158 ----------------------------------
159
160 procedure Expand_SPARK_Delta_Or_Update
161 (Typ : Entity_Id;
162 Aggr : Node_Id)
163 is
164 Assoc : Node_Id;
165 Comp : Node_Id;
166 Comp_Id : Entity_Id;
167 Comp_Type : Entity_Id;
168 Expr : Node_Id;
169 Index : Node_Id;
170 Index_Typ : Entity_Id;
171 New_Assoc : Node_Id;
172
173 begin
174 -- Apply scalar range checks on the updated components, if needed
175
176 if Is_Array_Type (Typ) then
177
178 -- Multidimensional arrays
179
180 if Present (Next_Index (First_Index (Typ))) then
181 Assoc := First (Component_Associations (Aggr));
182
183 while Present (Assoc) loop
184 Expr := Expression (Assoc);
185 Comp_Type := Component_Type (Typ);
186
187 if Is_Scalar_Type (Comp_Type) then
188 Apply_Scalar_Range_Check (Expr, Comp_Type);
189 end if;
190
191 -- The current association contains a sequence of indexes
192 -- denoting an element of a multidimensional array:
193 --
194 -- (Index_1, ..., Index_N)
195
196 Expr := First (Choices (Assoc));
197
198 pragma Assert (Nkind (Aggr) = N_Aggregate);
199
200 while Present (Expr) loop
201 Index := First (Expressions (Expr));
202 Index_Typ := First_Index (Typ);
203
204 while Present (Index_Typ) loop
205 Apply_Scalar_Range_Check (Index, Etype (Index_Typ));
206 Next (Index);
207 Next_Index (Index_Typ);
208 end loop;
209
210 Next (Expr);
211 end loop;
212
213 Next (Assoc);
214 end loop;
215
216 -- One-dimensional arrays
217
218 else
219 Assoc := First (Component_Associations (Aggr));
220
221 while Present (Assoc) loop
222 Expr := Expression (Assoc);
223 Comp_Type := Component_Type (Typ);
224
225 -- Analyze expression of the iterated_component_association
226 -- with its index parameter in scope.
227
228 if Nkind (Assoc) = N_Iterated_Component_Association then
229 Push_Scope (Scope (Defining_Identifier (Assoc)));
230 Enter_Name (Defining_Identifier (Assoc));
231 Analyze_And_Resolve (Expr, Comp_Type);
232 end if;
233
234 if Is_Scalar_Type (Comp_Type) then
235 Apply_Scalar_Range_Check (Expr, Comp_Type);
236 end if;
237
238 -- Restore scope of the iterated_component_association
239
240 if Nkind (Assoc) = N_Iterated_Component_Association then
241 End_Scope;
242 end if;
243
244 Index := First (Choice_List (Assoc));
245 Index_Typ := First_Index (Typ);
246
247 while Present (Index) loop
248 -- If the index denotes a range of elements or a constrained
249 -- subtype indication, then their low and high bounds
250 -- already have range checks applied.
251
252 if Nkind (Index) in N_Range | N_Subtype_Indication then
253 null;
254
255 -- Otherwise the index denotes a single expression where
256 -- range checks need to be applied or a subtype name
257 -- (without range constraints) where applying checks is
258 -- harmless.
259 --
260 -- In delta_aggregate and Update attribute on array the
261 -- others_choice is not allowed.
262
263 else pragma Assert (Nkind (Index) in N_Subexpr);
264 Apply_Scalar_Range_Check (Index, Etype (Index_Typ));
265 end if;
266
267 Next (Index);
268 end loop;
269
270 Next (Assoc);
271 end loop;
272 end if;
273
274 else pragma Assert (Is_Record_Type (Typ));
275
276 -- If the aggregate has multiple component choices, e.g.:
277 --
278 -- X'Update (A | B | C => 123)
279 --
280 -- then each component might be of a different type and might or
281 -- might not require a range check. We first rewrite associations
282 -- into single-component choices, e.g.:
283 --
284 -- X'Update (A => 123, B => 123, C => 123)
285 --
286 -- and then apply range checks to individual copies of the
287 -- expressions. We do the same for delta aggregates, accordingly.
288
289 -- Iterate over associations of the original aggregate
290
291 Assoc := First (Component_Associations (Aggr));
292
293 -- Rewrite into a new aggregate and decorate
294
295 case Nkind (Aggr) is
296 when N_Aggregate =>
297 Rewrite
298 (Aggr,
299 Make_Aggregate
300 (Sloc => Sloc (Aggr),
301 Component_Associations => New_List));
302
303 when N_Delta_Aggregate =>
304 Rewrite
305 (Aggr,
306 Make_Delta_Aggregate
307 (Sloc => Sloc (Aggr),
308 Expression => Expression (Aggr),
309 Component_Associations => New_List));
310
311 when others =>
312 raise Program_Error;
313 end case;
314
315 Set_Etype (Aggr, Typ);
316
317 -- Populate the new aggregate with component associations
318
319 while Present (Assoc) loop
320 Expr := Expression (Assoc);
321 Comp := First (Choices (Assoc));
322
323 while Present (Comp) loop
324 Comp_Id := Entity (Comp);
325 Comp_Type := Etype (Comp_Id);
326
327 New_Assoc :=
328 Make_Component_Association
329 (Sloc => Sloc (Assoc),
330 Choices =>
331 New_List
332 (New_Occurrence_Of (Comp_Id, Sloc (Comp))),
333 Expression => New_Copy_Tree (Expr));
334
335 -- New association must be attached to the aggregate before we
336 -- analyze it.
337
338 Append (New_Assoc, Component_Associations (Aggr));
339
340 Analyze_And_Resolve (Expression (New_Assoc), Comp_Type);
341
342 if Is_Scalar_Type (Comp_Type) then
343 Apply_Scalar_Range_Check
344 (Expression (New_Assoc), Comp_Type);
345 end if;
346
347 Next (Comp);
348 end loop;
349
350 Next (Assoc);
351 end loop;
352 end if;
353 end Expand_SPARK_Delta_Or_Update;
354
355 --------------------------------
356 -- Expand_SPARK_N_Freeze_Type --
357 --------------------------------
358
359 procedure Expand_SPARK_N_Freeze_Type (E : Entity_Id) is
360 begin
361 -- When a DIC is inherited by a tagged type, it may need to be
362 -- specialized to the descendant type, hence build a separate DIC
363 -- procedure for it as done during regular expansion for compilation.
364
365 if Has_DIC (E) and then Is_Tagged_Type (E) then
366 Build_DIC_Procedure_Body (E, For_Freeze => True);
367 end if;
368 end Expand_SPARK_N_Freeze_Type;
369
370 ------------------------------
371 -- Expand_SPARK_N_Aggregate --
372 ------------------------------
373
374 procedure Expand_SPARK_N_Aggregate (N : Node_Id) is
375 Assoc : Node_Id := First (Component_Associations (N));
376 begin
377 -- For compilation, frontend analyses a copy of the
378 -- iterated_component_association's expression for legality checking;
379 -- (then the expression is copied again when expanding association into
380 -- assignments for the individual choices). For SPARK we analyze the
381 -- original expression and apply range checks, if required.
382
383 while Present (Assoc) loop
384 if Nkind (Assoc) = N_Iterated_Component_Association then
385 declare
386 Typ : constant Entity_Id := Etype (N);
387
388 Comp_Type : constant Entity_Id := Component_Type (Typ);
389 Expr : constant Node_Id := Expression (Assoc);
390 Index_Typ : constant Entity_Id := First_Index (Typ);
391
392 Index : Node_Id;
393
394 begin
395 -- Analyze expression with index parameter in scope
396
397 Push_Scope (Scope (Defining_Identifier (Assoc)));
398 Enter_Name (Defining_Identifier (Assoc));
399 Analyze_And_Resolve (Expr, Comp_Type);
400
401 if Is_Scalar_Type (Comp_Type) then
402 Apply_Scalar_Range_Check (Expr, Comp_Type);
403 end if;
404
405 End_Scope;
406
407 -- Analyze discrete choices
408
409 Index := First (Discrete_Choices (Assoc));
410
411 while Present (Index) loop
412
413 -- The index denotes a range of elements where range checks
414 -- have been already applied.
415
416 if Nkind (Index) in N_Others_Choice
417 | N_Range
418 | N_Subtype_Indication
419 then
420 null;
421
422 -- Otherwise the index denotes a single element (or a
423 -- subtype name which doesn't require range checks).
424
425 else pragma Assert (Nkind (Index) in N_Subexpr);
426 Apply_Scalar_Range_Check (Index, Etype (Index_Typ));
427 end if;
428
429 Next (Index);
430 end loop;
431 end;
432 end if;
433
434 Next (Assoc);
435 end loop;
436 end Expand_SPARK_N_Aggregate;
437
438 ----------------------------------------
439 -- Expand_SPARK_N_Attribute_Reference --
440 ----------------------------------------
441
442 procedure Expand_SPARK_N_Attribute_Reference (N : Node_Id) is
443 Aname : constant Name_Id := Attribute_Name (N);
444 Attr_Id : constant Attribute_Id := Get_Attribute_Id (Aname);
445 Loc : constant Source_Ptr := Sloc (N);
446 Pref : constant Node_Id := Prefix (N);
447 Typ : constant Entity_Id := Etype (N);
448 Expr : Node_Id;
449
450 begin
451 if Attr_Id = Attribute_To_Address then
452
453 -- Extract and convert argument to expected type for call
454
455 Expr :=
456 Make_Type_Conversion (Loc,
457 Subtype_Mark =>
458 New_Occurrence_Of (RTE (RE_Integer_Address), Loc),
459 Expression => Relocate_Node (First (Expressions (N))));
460
461 -- Replace attribute reference with call
462
463 Rewrite (N,
464 Make_Function_Call (Loc,
465 Name =>
466 New_Occurrence_Of (RTE (RE_To_Address), Loc),
467 Parameter_Associations => New_List (Expr)));
468 Analyze_And_Resolve (N, Typ);
469
470 elsif Attr_Id = Attribute_Object_Size
471 or else Attr_Id = Attribute_Size
472 or else Attr_Id = Attribute_Value_Size
473 or else Attr_Id = Attribute_VADS_Size
474 then
475 Exp_Attr.Expand_Size_Attribute (N);
476
477 -- For attributes which return Universal_Integer, introduce a conversion
478 -- to the expected type with the appropriate check flags set.
479
480 elsif Attr_Id = Attribute_Alignment
481 or else Attr_Id = Attribute_Bit
482 or else Attr_Id = Attribute_Bit_Position
483 or else Attr_Id = Attribute_Descriptor_Size
484 or else Attr_Id = Attribute_First_Bit
485 or else Attr_Id = Attribute_Last_Bit
486 or else Attr_Id = Attribute_Length
487 or else Attr_Id = Attribute_Max_Size_In_Storage_Elements
488 or else Attr_Id = Attribute_Pos
489 or else Attr_Id = Attribute_Position
490 or else Attr_Id = Attribute_Range_Length
491 or else Attr_Id = Attribute_Aft
492 or else Attr_Id = Attribute_Max_Alignment_For_Allocation
493 then
494 -- If the expected type is Long_Long_Integer, there will be no check
495 -- flag as the compiler assumes attributes always fit in this type.
496 -- Since in SPARK_Mode we do not take Storage_Error into account, we
497 -- cannot make this assumption and need to produce a check.
498 -- ??? It should be enough to add this check for attributes
499 -- 'Length, 'Range_Length and 'Pos when the type is as big
500 -- as Long_Long_Integer.
501
502 declare
503 Typ : Entity_Id;
504 begin
505 if Attr_Id = Attribute_Range_Length
506 or else Attr_Id = Attribute_Pos
507 then
508 Typ := Etype (Prefix (N));
509
510 elsif Attr_Id = Attribute_Length then
511 Typ := Get_Index_Subtype (N);
512
513 else
514 Typ := Empty;
515 end if;
516
517 Apply_Universal_Integer_Attribute_Checks (N);
518
519 if Present (Typ)
520 and then RM_Size (Typ) = RM_Size (Standard_Long_Long_Integer)
521 then
522 -- ??? This should rather be a range check, but this would
523 -- crash GNATprove which somehow recovers the proper kind
524 -- of check anyway.
525 Set_Do_Overflow_Check (N);
526 end if;
527 end;
528
529 elsif Attr_Id = Attribute_Constrained then
530
531 -- If the prefix is an access to object, the attribute applies to
532 -- the designated object, so rewrite with an explicit dereference.
533
534 if Is_Access_Type (Etype (Pref))
535 and then
536 (not Is_Entity_Name (Pref) or else Is_Object (Entity (Pref)))
537 then
538 Rewrite (Pref,
539 Make_Explicit_Dereference (Loc, Relocate_Node (Pref)));
540 Analyze_And_Resolve (N, Standard_Boolean);
541 end if;
542
543 elsif Attr_Id = Attribute_Update then
544 Expand_SPARK_Delta_Or_Update (Typ, First (Expressions (N)));
545 end if;
546 end Expand_SPARK_N_Attribute_Reference;
547
548 ------------------------------------
549 -- Expand_SPARK_N_Delta_Aggregate --
550 ------------------------------------
551
552 procedure Expand_SPARK_N_Delta_Aggregate (N : Node_Id) is
553 begin
554 Expand_SPARK_Delta_Or_Update (Etype (N), N);
555 end Expand_SPARK_N_Delta_Aggregate;
556
557 -----------------------------------
558 -- Expand_SPARK_N_Loop_Statement --
559 -----------------------------------
560
561 procedure Expand_SPARK_N_Loop_Statement (N : Node_Id) is
562 Scheme : constant Node_Id := Iteration_Scheme (N);
563
564 begin
565 -- Loop iterations over arrays need to be expanded, to avoid getting
566 -- two names referring to the same object in memory (the array and the
567 -- iterator) in GNATprove, especially since both can be written (thus
568 -- possibly leading to interferences due to aliasing). No such problem
569 -- arises with quantified expressions over arrays, which are dealt with
570 -- specially in GNATprove.
571
572 if Present (Scheme)
573 and then Present (Iterator_Specification (Scheme))
574 and then Is_Iterator_Over_Array (Iterator_Specification (Scheme))
575 then
576 Expand_Iterator_Loop_Over_Array (N);
577 end if;
578 end Expand_SPARK_N_Loop_Statement;
579
580 ---------------------------------------
581 -- Expand_SPARK_N_Object_Declaration --
582 ---------------------------------------
583
584 procedure Expand_SPARK_N_Object_Declaration (N : Node_Id) is
585 Loc : constant Source_Ptr := Sloc (N);
586 Obj_Id : constant Entity_Id := Defining_Identifier (N);
587 Typ : constant Entity_Id := Etype (Obj_Id);
588
589 Call : Node_Id;
590
591 begin
592 -- If the object declaration denotes a variable without initialization
593 -- whose type is subject to pragma Default_Initial_Condition, create
594 -- and analyze a dummy call to the DIC procedure of the type in order
595 -- to detect potential elaboration issues.
596
597 if Comes_From_Source (Obj_Id)
598 and then Ekind (Obj_Id) = E_Variable
599 and then Has_DIC (Typ)
600 and then Present (DIC_Procedure (Typ))
601 and then not Has_Init_Expression (N)
602 then
603 Call := Build_DIC_Call (Loc, Obj_Id, Typ);
604
605 -- Partially insert the call into the tree by setting its parent
606 -- pointer.
607
608 Set_Parent (Call, N);
609 Analyze (Call);
610 end if;
611 end Expand_SPARK_N_Object_Declaration;
612
613 ------------------------------------------------
614 -- Expand_SPARK_N_Object_Renaming_Declaration --
615 ------------------------------------------------
616
617 procedure Expand_SPARK_N_Object_Renaming_Declaration (N : Node_Id) is
618 CFS : constant Boolean := Comes_From_Source (N);
619 Loc : constant Source_Ptr := Sloc (N);
620 Obj_Id : constant Entity_Id := Defining_Entity (N);
621 Nam : constant Node_Id := Name (N);
622 Typ : constant Entity_Id := Etype (Obj_Id);
623
624 begin
625 -- Transform a renaming of the form
626
627 -- Obj_Id : <subtype mark> renames <function call>;
628
629 -- into
630
631 -- Obj_Id : constant <subtype mark> := <function call>;
632
633 -- Invoking Evaluate_Name and ultimately Remove_Side_Effects introduces
634 -- a temporary to capture the function result. Once potential renamings
635 -- are rewritten for SPARK, the temporary may be leaked out into source
636 -- constructs and lead to confusing error diagnostics. Using an object
637 -- declaration prevents this unwanted side effect.
638
639 if Nkind (Nam) = N_Function_Call then
640 Rewrite (N,
641 Make_Object_Declaration (Loc,
642 Defining_Identifier => Obj_Id,
643 Constant_Present => True,
644 Object_Definition => New_Occurrence_Of (Typ, Loc),
645 Expression => Nam));
646
647 -- Inherit the original Comes_From_Source status of the renaming
648
649 Set_Comes_From_Source (N, CFS);
650
651 -- Sever the link to the renamed function result because the entity
652 -- will no longer alias anything.
653
654 Set_Renamed_Object (Obj_Id, Empty);
655
656 -- Remove the entity of the renaming declaration from visibility as
657 -- the analysis of the object declaration will reintroduce it again.
658
659 Remove_Entity_And_Homonym (Obj_Id);
660 Analyze (N);
661
662 -- Otherwise unconditionally remove all side effects from the name
663
664 else
665 Evaluate_Name (Nam);
666 end if;
667 end Expand_SPARK_N_Object_Renaming_Declaration;
668
669 --------------------------
670 -- Expand_SPARK_N_Op_Ne --
671 --------------------------
672
673 procedure Expand_SPARK_N_Op_Ne (N : Node_Id) is
674 Typ : constant Entity_Id := Etype (Left_Opnd (N));
675
676 begin
677 -- Case of elementary type with standard operator
678
679 if Is_Elementary_Type (Typ)
680 and then Sloc (Entity (N)) = Standard_Location
681 then
682 null;
683
684 else
685 Exp_Ch4.Expand_N_Op_Ne (N);
686 end if;
687 end Expand_SPARK_N_Op_Ne;
688
689 -------------------------------------
690 -- Expand_SPARK_Potential_Renaming --
691 -------------------------------------
692
693 procedure Expand_SPARK_Potential_Renaming (N : Node_Id) is
694 function In_Insignificant_Pragma (Nod : Node_Id) return Boolean;
695 -- Determine whether arbitrary node Nod appears within a significant
696 -- pragma for SPARK.
697
698 -----------------------------
699 -- In_Insignificant_Pragma --
700 -----------------------------
701
702 function In_Insignificant_Pragma (Nod : Node_Id) return Boolean is
703 Par : Node_Id;
704
705 begin
706 -- Climb the parent chain looking for an enclosing pragma
707
708 Par := Nod;
709 while Present (Par) loop
710 if Nkind (Par) = N_Pragma then
711 return not Pragma_Significant_In_SPARK (Get_Pragma_Id (Par));
712
713 -- Prevent the search from going too far
714
715 elsif Is_Body_Or_Package_Declaration (Par) then
716 exit;
717 end if;
718
719 Par := Parent (Par);
720 end loop;
721
722 return False;
723 end In_Insignificant_Pragma;
724
725 -- Local variables
726
727 Loc : constant Source_Ptr := Sloc (N);
728 Obj_Id : constant Entity_Id := Entity (N);
729 Typ : constant Entity_Id := Etype (N);
730 Ren : Node_Id;
731
732 -- Start of processing for Expand_SPARK_Potential_Renaming
733
734 begin
735 -- Replace a reference to a renaming with the actual renamed object
736
737 if Is_Object (Obj_Id) then
738 Ren := Renamed_Object (Obj_Id);
739
740 if Present (Ren) then
741
742 -- Do not process a reference when it appears within a pragma of
743 -- no significance to SPARK. It is assumed that the replacement
744 -- will violate the semantics of the pragma and cause a spurious
745 -- error.
746
747 if In_Insignificant_Pragma (N) then
748 return;
749
750 -- Instantiations and inlining of subprograms employ "prologues"
751 -- which map actual to formal parameters by means of renamings.
752 -- Replace a reference to a formal by the corresponding actual
753 -- parameter.
754
755 elsif Nkind (Ren) in N_Entity then
756 Rewrite (N, New_Occurrence_Of (Ren, Loc));
757
758 -- Otherwise the renamed object denotes a name
759
760 else
761 Rewrite (N, New_Copy_Tree (Ren, New_Sloc => Loc));
762 Reset_Analyzed_Flags (N);
763 end if;
764
765 Analyze_And_Resolve (N, Typ);
766 end if;
767 end if;
768 end Expand_SPARK_Potential_Renaming;
769
770 end Exp_SPARK;