1 ------------------------------------------------------------------------------
3 -- GNAT COMPILER COMPONENTS --
5 -- E X P _ S P A R K --
9 -- Copyright (C) 1992-2022, 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 Atree
; use Atree
;
27 with Checks
; use Checks
;
28 with Einfo
; use Einfo
;
29 with Einfo
.Entities
; use Einfo
.Entities
;
30 with Einfo
.Utils
; use Einfo
.Utils
;
34 with Exp_Ch5
; use Exp_Ch5
;
35 with Exp_Dbug
; use Exp_Dbug
;
36 with Exp_Util
; use Exp_Util
;
37 with Ghost
; use Ghost
;
38 with Namet
; use Namet
;
39 with Nlists
; use Nlists
;
40 with Nmake
; use Nmake
;
42 with Restrict
; use Restrict
;
43 with Rident
; use Rident
;
44 with Rtsfind
; use Rtsfind
;
46 with Sem_Aux
; use Sem_Aux
;
47 with Sem_Ch7
; use Sem_Ch7
;
48 with Sem_Ch8
; use Sem_Ch8
;
49 with Sem_Prag
; use Sem_Prag
;
50 with Sem_Res
; use Sem_Res
;
51 with Sem_Util
; use Sem_Util
;
52 with Sinfo
; use Sinfo
;
53 with Sinfo
.Nodes
; use Sinfo
.Nodes
;
54 with Sinfo
.Utils
; use Sinfo
.Utils
;
55 with Snames
; use Snames
;
56 with Stand
; use Stand
;
57 with Tbuild
; use Tbuild
;
58 with Uintp
; use Uintp
;
60 package body Exp_SPARK
is
62 -----------------------
63 -- Local Subprograms --
64 -----------------------
66 procedure Expand_SPARK_N_Attribute_Reference
(N
: Node_Id
);
67 -- Perform attribute-reference-specific expansion
69 procedure Expand_SPARK_N_Delta_Aggregate
(N
: Node_Id
);
70 -- Perform delta-aggregate-specific expansion
72 procedure Expand_SPARK_N_Freeze_Entity
(N
: Node_Id
);
73 -- Do a minimal expansion of freeze entities required by GNATprove. It is
74 -- a subset of what is done for GNAT in Exp_Ch13.Expand_N_Freeze_Entity.
75 -- Those two routines should be kept in sync.
77 procedure Expand_SPARK_N_Loop_Statement
(N
: Node_Id
);
78 -- Perform loop-statement-specific expansion
80 procedure Expand_SPARK_N_Object_Declaration
(N
: Node_Id
);
81 -- Perform object-declaration-specific expansion
83 procedure Expand_SPARK_N_Object_Renaming_Declaration
(N
: Node_Id
);
84 -- Perform name evaluation for a renamed object
86 procedure Expand_SPARK_N_Op_Ne
(N
: Node_Id
);
87 -- Rewrite operator /= based on operator = when defined explicitly
89 procedure Expand_SPARK_Delta_Or_Update
(Typ
: Entity_Id
; Aggr
: Node_Id
);
90 -- Common expansion for attribute Update and delta aggregates
92 procedure SPARK_Freeze_Type
(N
: Node_Id
);
93 -- Do a minimal type freezing required by GNATprove. It is a subset of what
94 -- is done for GNAT in Exp_Ch3.Freeze_Type. Those two routines should be
97 -- Currently in freezing we build the spec of dispatching equality. This
98 -- spec is needed to properly resolve references to the equality operator.
99 -- The body is not needed, because proof knows how to directly synthesize a
100 -- logical meaning for it. Also, for tagged types with extension the
101 -- expanded body would compare the _parent component, which is
102 -- intentionally not generated in the GNATprove mode.
104 -- We build the DIC procedure body here as well.
110 procedure Expand_SPARK
(N
: Node_Id
) is
114 -- Qualification of entity names in formal verification mode
115 -- is limited to the addition of a suffix for homonyms (see
116 -- Exp_Dbug.Qualify_Entity_Name). We used to qualify entity names
117 -- as full expansion does, but this was removed as this prevents the
118 -- verification back-end from using a short name for debugging and
119 -- user interaction. The verification back-end already takes care
120 -- of qualifying names when needed.
122 when N_Block_Statement
123 | N_Entry_Declaration
125 | N_Package_Declaration
126 | N_Protected_Type_Declaration
128 | N_Task_Type_Declaration
130 Qualify_Entity_Names
(N
);
132 -- Replace occurrences of System'To_Address by calls to
133 -- System.Storage_Elements.To_Address.
135 when N_Attribute_Reference
=>
136 Expand_SPARK_N_Attribute_Reference
(N
);
138 when N_Delta_Aggregate
=>
139 Expand_SPARK_N_Delta_Aggregate
(N
);
144 Expand_SPARK_Potential_Renaming
(N
);
146 -- Loop iterations over arrays need to be expanded, to avoid getting
147 -- two names referring to the same object in memory (the array and
148 -- the iterator) in GNATprove, especially since both can be written
149 -- (thus possibly leading to interferences due to aliasing). No such
150 -- problem arises with quantified expressions over arrays, which are
151 -- dealt with specially in GNATprove.
153 when N_Loop_Statement
=>
154 Expand_SPARK_N_Loop_Statement
(N
);
156 when N_Object_Declaration
=>
157 Expand_SPARK_N_Object_Declaration
(N
);
159 when N_Object_Renaming_Declaration
=>
160 Expand_SPARK_N_Object_Renaming_Declaration
(N
);
163 Expand_SPARK_N_Op_Ne
(N
);
165 when N_Freeze_Entity
=>
166 -- Currently we only expand type freeze entities, so ignore other
167 -- freeze entites, because it is expensive to create a suitable
168 -- freezing environment.
170 if Is_Type
(Entity
(N
)) then
171 Expand_SPARK_N_Freeze_Entity
(N
);
174 -- In SPARK mode, no other constructs require expansion
181 ----------------------------------
182 -- Expand_SPARK_Delta_Or_Update --
183 ----------------------------------
185 procedure Expand_SPARK_Delta_Or_Update
192 Comp_Type
: Entity_Id
;
195 Index_Typ
: Entity_Id
;
199 -- Apply scalar range checks on the updated components, if needed
201 if Is_Array_Type
(Typ
) then
203 -- Multidimensional arrays
205 if Present
(Next_Index
(First_Index
(Typ
))) then
206 Assoc
:= First
(Component_Associations
(Aggr
));
208 while Present
(Assoc
) loop
209 Expr
:= Expression
(Assoc
);
210 Comp_Type
:= Component_Type
(Typ
);
212 if Is_Scalar_Type
(Comp_Type
) then
213 Apply_Scalar_Range_Check
(Expr
, Comp_Type
);
216 -- The current association contains a sequence of indexes
217 -- denoting an element of a multidimensional array:
219 -- (Index_1, ..., Index_N)
221 Expr
:= First
(Choices
(Assoc
));
223 pragma Assert
(Nkind
(Aggr
) = N_Aggregate
);
225 while Present
(Expr
) loop
226 Index
:= First
(Expressions
(Expr
));
227 Index_Typ
:= First_Index
(Typ
);
229 while Present
(Index_Typ
) loop
230 Apply_Scalar_Range_Check
(Index
, Etype
(Index_Typ
));
232 Next_Index
(Index_Typ
);
241 -- One-dimensional arrays
244 Assoc
:= First
(Component_Associations
(Aggr
));
246 while Present
(Assoc
) loop
247 Expr
:= Expression
(Assoc
);
248 Comp_Type
:= Component_Type
(Typ
);
250 -- Analyze expression of the iterated_component_association
251 -- with its index parameter in scope.
253 if Nkind
(Assoc
) = N_Iterated_Component_Association
then
254 Push_Scope
(Scope
(Defining_Identifier
(Assoc
)));
255 Enter_Name
(Defining_Identifier
(Assoc
));
256 Analyze_And_Resolve
(Expr
, Comp_Type
);
259 if Is_Scalar_Type
(Comp_Type
) then
260 Apply_Scalar_Range_Check
(Expr
, Comp_Type
);
263 -- Restore scope of the iterated_component_association
265 if Nkind
(Assoc
) = N_Iterated_Component_Association
then
269 Index
:= First
(Choice_List
(Assoc
));
270 Index_Typ
:= First_Index
(Typ
);
272 while Present
(Index
) loop
273 -- If the index denotes a range of elements or a constrained
274 -- subtype indication, then their low and high bounds
275 -- already have range checks applied.
277 if Nkind
(Index
) in N_Range | N_Subtype_Indication
then
280 -- Otherwise the index denotes a single expression where
281 -- range checks need to be applied or a subtype name
282 -- (without range constraints) where applying checks is
285 -- In delta_aggregate and Update attribute on array the
286 -- others_choice is not allowed.
288 else pragma Assert
(Nkind
(Index
) in N_Subexpr
);
289 Apply_Scalar_Range_Check
(Index
, Etype
(Index_Typ
));
299 else pragma Assert
(Is_Record_Type
(Typ
));
301 -- If the aggregate has multiple component choices, e.g.:
303 -- X'Update (A | B | C => 123)
305 -- then each component might be of a different type and might or
306 -- might not require a range check. We first rewrite associations
307 -- into single-component choices, e.g.:
309 -- X'Update (A => 123, B => 123, C => 123)
311 -- and then apply range checks to individual copies of the
312 -- expressions. We do the same for delta aggregates, accordingly.
314 -- Iterate over associations of the original aggregate
316 Assoc
:= First
(Component_Associations
(Aggr
));
318 -- Rewrite into a new aggregate and decorate
325 (Sloc
=> Sloc
(Aggr
),
326 Component_Associations
=> New_List
));
328 when N_Delta_Aggregate
=>
332 (Sloc
=> Sloc
(Aggr
),
333 Expression
=> Expression
(Aggr
),
334 Component_Associations
=> New_List
));
340 Set_Etype
(Aggr
, Typ
);
342 -- Populate the new aggregate with component associations
344 while Present
(Assoc
) loop
345 Expr
:= Expression
(Assoc
);
346 Comp
:= First
(Choices
(Assoc
));
348 while Present
(Comp
) loop
349 Comp_Id
:= Entity
(Comp
);
350 Comp_Type
:= Etype
(Comp_Id
);
353 Make_Component_Association
354 (Sloc
=> Sloc
(Assoc
),
357 (New_Occurrence_Of
(Comp_Id
, Sloc
(Comp
))),
358 Expression
=> New_Copy_Tree
(Expr
));
360 -- New association must be attached to the aggregate before we
363 Append
(New_Assoc
, Component_Associations
(Aggr
));
365 Analyze_And_Resolve
(Expression
(New_Assoc
), Comp_Type
);
367 if Is_Scalar_Type
(Comp_Type
) then
368 Apply_Scalar_Range_Check
369 (Expression
(New_Assoc
), Comp_Type
);
378 end Expand_SPARK_Delta_Or_Update
;
380 ----------------------------------
381 -- Expand_SPARK_N_Freeze_Entity --
382 ----------------------------------
384 procedure Expand_SPARK_N_Freeze_Entity
(N
: Entity_Id
) is
385 E
: constant Entity_Id
:= Entity
(N
);
389 In_Other_Scope
: Boolean;
390 In_Outer_Scope
: Boolean;
393 -- Here E is a type or a subprogram
395 E_Scope
:= Scope
(E
);
397 -- This is an error protection against previous errors
400 Check_Error_Detected
;
404 -- The entity may be a subtype declared for a constrained record
405 -- component, in which case the relevant scope is the scope of
406 -- the record. This happens for class-wide subtypes created for
407 -- a constrained type extension with inherited discriminants.
410 and then not Is_Concurrent_Type
(E_Scope
)
412 E_Scope
:= Scope
(E_Scope
);
414 -- The entity may be a subtype declared for an iterator
416 elsif Ekind
(E_Scope
) = E_Loop
then
417 E_Scope
:= Scope
(E_Scope
);
420 -- If we are freezing entities defined in protected types, they belong
421 -- in the enclosing scope, given that the original type has been
422 -- expanded away. The same is true for entities in task types, in
423 -- particular the parameter records of entries (Entities in bodies are
424 -- all frozen within the body). If we are in the task body, this is a
425 -- proper scope. If we are within a subprogram body, the proper scope
426 -- is the corresponding spec. This may happen for itypes generated in
427 -- the bodies of protected operations.
429 if Ekind
(E_Scope
) = E_Protected_Type
430 or else (Ekind
(E_Scope
) = E_Task_Type
431 and then not Has_Completion
(E_Scope
))
433 E_Scope
:= Scope
(E_Scope
);
435 elsif Ekind
(E_Scope
) = E_Subprogram_Body
then
436 E_Scope
:= Corresponding_Spec
(Unit_Declaration_Node
(E_Scope
));
439 -- If the scope of the entity is in open scopes, it is the current one
440 -- or an enclosing one, including a loop, a block, or a subprogram.
442 if In_Open_Scopes
(E_Scope
) then
443 In_Other_Scope
:= False;
444 In_Outer_Scope
:= E_Scope
/= Current_Scope
;
446 -- Otherwise it is a local package or a different compilation unit
449 In_Other_Scope
:= True;
450 In_Outer_Scope
:= False;
453 -- If the entity being frozen is defined in a scope that is not
454 -- currently on the scope stack, we must establish the proper
455 -- visibility before freezing the entity and related subprograms.
457 if In_Other_Scope
then
458 Push_Scope
(E_Scope
);
460 -- Finalizers are little odd in terms of freezing. The spec of the
461 -- procedure appears in the declarations while the body appears in
462 -- the statement part of a single construct. Since the finalizer must
463 -- be called by the At_End handler of the construct, the spec is
464 -- manually frozen right after its declaration. The only side effect
465 -- of this action appears in contexts where the construct is not in
466 -- its final resting place. These contexts are:
468 -- * Entry bodies - The declarations and statements are moved to
469 -- the procedure equivalen of the entry.
470 -- * Protected subprograms - The declarations and statements are
471 -- moved to the non-protected version of the subprogram.
472 -- * Task bodies - The declarations and statements are moved to the
473 -- task body procedure.
474 -- * Blocks that will be rewritten as subprograms when unnesting
477 -- Visible declarations do not need to be installed in these three
478 -- cases since it does not make semantic sense to do so. All entities
479 -- referenced by a finalizer are visible and already resolved, plus
480 -- the enclosing scope may not have visible declarations at all.
482 if Ekind
(E
) = E_Procedure
483 and then Is_Finalizer
(E
)
486 or else (Is_Subprogram
(E_Scope
)
487 and then Is_Protected_Type
(Scope
(E_Scope
)))
488 or else Is_Task_Type
(E_Scope
)
489 or else Ekind
(E_Scope
) = E_Block
)
493 Install_Visible_Declarations
(E_Scope
);
496 if Is_Concurrent_Type
(E_Scope
)
497 or else Is_Package_Or_Generic_Package
(E_Scope
)
499 Install_Private_Declarations
(E_Scope
);
502 -- If the entity is in an outer scope, then that scope needs to
503 -- temporarily become the current scope so that operations created
504 -- during type freezing will be declared in the right scope and
505 -- can properly override any corresponding inherited operations.
507 elsif In_Outer_Scope
then
508 Push_Scope
(E_Scope
);
511 -- Remember that we are processing a freezing entity and its freezing
512 -- nodes. This flag (non-zero = set) is used to avoid the need of
513 -- climbing through the tree while processing the freezing actions (ie.
514 -- to avoid generating spurious warnings or to avoid killing constant
515 -- indications while processing the code associated with freezing
516 -- actions). We use a counter to deal with nesting.
518 Inside_Freezing_Actions
:= Inside_Freezing_Actions
+ 1;
520 -- Currently only types require freezing in SPARK
522 SPARK_Freeze_Type
(N
);
524 -- Analyze actions in freeze node, if any
526 Action
:= First
(Actions
(N
));
527 while Present
(Action
) loop
532 -- Pop scope if we installed one for the analysis
534 if In_Other_Scope
then
535 if Ekind
(Current_Scope
) = E_Package
then
536 End_Package_Scope
(E_Scope
);
541 elsif In_Outer_Scope
then
545 -- Restore previous value of the nesting-level counter that records
546 -- whether we are inside a (possibly nested) call to this procedure.
548 Inside_Freezing_Actions
:= Inside_Freezing_Actions
- 1;
549 end Expand_SPARK_N_Freeze_Entity
;
551 ----------------------------------------
552 -- Expand_SPARK_N_Attribute_Reference --
553 ----------------------------------------
555 procedure Expand_SPARK_N_Attribute_Reference
(N
: Node_Id
) is
556 Aname
: constant Name_Id
:= Attribute_Name
(N
);
557 Attr_Id
: constant Attribute_Id
:= Get_Attribute_Id
(Aname
);
558 Loc
: constant Source_Ptr
:= Sloc
(N
);
559 Pref
: constant Node_Id
:= Prefix
(N
);
560 Typ
: constant Entity_Id
:= Etype
(N
);
565 when Attribute_To_Address
=>
567 -- Extract and convert argument to expected type for call
570 Make_Type_Conversion
(Loc
,
572 New_Occurrence_Of
(RTE
(RE_Integer_Address
), Loc
),
573 Expression
=> Relocate_Node
(First
(Expressions
(N
))));
575 -- Replace attribute reference with call
579 Make_Function_Call
(Loc
,
581 New_Occurrence_Of
(RTE
(RE_To_Address
), Loc
),
582 Parameter_Associations
=> New_List
(Expr
)));
583 Analyze_And_Resolve
(N
, Typ
);
585 when Attribute_Object_Size
587 | Attribute_Value_Size
588 | Attribute_VADS_Size
590 Exp_Attr
.Expand_Size_Attribute
(N
);
592 -- For attributes which return Universal_Integer, introduce a
593 -- conversion to the expected type with the appropriate check flags
597 | Attribute_Alignment
599 | Attribute_Bit_Position
600 | Attribute_Descriptor_Size
601 | Attribute_First_Bit
604 | Attribute_Max_Alignment_For_Allocation
605 | Attribute_Max_Size_In_Storage_Elements
608 | Attribute_Range_Length
610 -- If the expected type is Long_Long_Integer, there will be no
611 -- check flag as the compiler assumes attributes always fit in
612 -- this type. Since in SPARK_Mode we do not take Storage_Error
613 -- into account, we cannot make this assumption and need to
614 -- produce a check. ??? It should be enough to add this check for
615 -- attributes 'Length, 'Range_Length and 'Pos when the type is as
616 -- big as Long_Long_Integer.
621 if Attr_Id
in Attribute_Pos | Attribute_Range_Length
then
622 Typ
:= Etype
(Prefix
(N
));
624 elsif Attr_Id
= Attribute_Length
then
625 Typ
:= Get_Index_Subtype
(N
);
631 Apply_Universal_Integer_Attribute_Checks
(N
);
634 and then Known_RM_Size
(Typ
)
635 and then RM_Size
(Typ
) = RM_Size
(Standard_Long_Long_Integer
)
637 -- ??? This should rather be a range check, but this would
638 -- crash GNATprove which somehow recovers the proper kind
640 Set_Do_Overflow_Check
(N
);
644 when Attribute_Constrained
=>
646 -- If the prefix is an access to object, the attribute applies to
647 -- the designated object, so rewrite with an explicit dereference.
649 if Is_Access_Type
(Etype
(Pref
))
651 (not Is_Entity_Name
(Pref
) or else Is_Object
(Entity
(Pref
)))
654 Make_Explicit_Dereference
(Loc
, Relocate_Node
(Pref
)));
655 Analyze_And_Resolve
(N
, Standard_Boolean
);
658 when Attribute_Update
=>
659 Expand_SPARK_Delta_Or_Update
(Typ
, First
(Expressions
(N
)));
664 end Expand_SPARK_N_Attribute_Reference
;
666 ------------------------------------
667 -- Expand_SPARK_N_Delta_Aggregate --
668 ------------------------------------
670 procedure Expand_SPARK_N_Delta_Aggregate
(N
: Node_Id
) is
672 Expand_SPARK_Delta_Or_Update
(Etype
(N
), N
);
673 end Expand_SPARK_N_Delta_Aggregate
;
675 -----------------------------------
676 -- Expand_SPARK_N_Loop_Statement --
677 -----------------------------------
679 procedure Expand_SPARK_N_Loop_Statement
(N
: Node_Id
) is
680 Scheme
: constant Node_Id
:= Iteration_Scheme
(N
);
683 -- Loop iterations over arrays need to be expanded, to avoid getting
684 -- two names referring to the same object in memory (the array and the
685 -- iterator) in GNATprove, especially since both can be written (thus
686 -- possibly leading to interferences due to aliasing). No such problem
687 -- arises with quantified expressions over arrays, which are dealt with
688 -- specially in GNATprove.
691 and then Present
(Iterator_Specification
(Scheme
))
692 and then Is_Iterator_Over_Array
(Iterator_Specification
(Scheme
))
694 Expand_Iterator_Loop_Over_Array
(N
);
696 end Expand_SPARK_N_Loop_Statement
;
698 ---------------------------------------
699 -- Expand_SPARK_N_Object_Declaration --
700 ---------------------------------------
702 procedure Expand_SPARK_N_Object_Declaration
(N
: Node_Id
) is
703 Loc
: constant Source_Ptr
:= Sloc
(N
);
704 Obj_Id
: constant Entity_Id
:= Defining_Identifier
(N
);
705 Typ
: constant Entity_Id
:= Etype
(Obj_Id
);
710 -- If the object declaration denotes a variable without initialization
711 -- whose type is subject to pragma Default_Initial_Condition, create
712 -- and analyze a dummy call to the DIC procedure of the type in order
713 -- to detect potential elaboration issues.
715 if Comes_From_Source
(Obj_Id
)
716 and then Ekind
(Obj_Id
) = E_Variable
717 and then Has_DIC
(Typ
)
718 and then Present
(DIC_Procedure
(Typ
))
719 and then not Has_Init_Expression
(N
)
721 Call
:= Build_DIC_Call
(Loc
, New_Occurrence_Of
(Obj_Id
, Loc
), Typ
);
723 -- Partially insert the call into the tree by setting its parent
726 Set_Parent
(Call
, N
);
729 end Expand_SPARK_N_Object_Declaration
;
731 ------------------------------------------------
732 -- Expand_SPARK_N_Object_Renaming_Declaration --
733 ------------------------------------------------
735 procedure Expand_SPARK_N_Object_Renaming_Declaration
(N
: Node_Id
) is
736 CFS
: constant Boolean := Comes_From_Source
(N
);
737 Loc
: constant Source_Ptr
:= Sloc
(N
);
738 Obj_Id
: constant Entity_Id
:= Defining_Entity
(N
);
739 Nam
: constant Node_Id
:= Name
(N
);
740 Typ
: constant Entity_Id
:= Etype
(Obj_Id
);
743 -- Transform a renaming of the form
745 -- Obj_Id : <subtype mark> renames <function call>;
749 -- Obj_Id : constant <subtype mark> := <function call>;
751 -- Invoking Evaluate_Name and ultimately Remove_Side_Effects introduces
752 -- a temporary to capture the function result. Once potential renamings
753 -- are rewritten for SPARK, the temporary may be leaked out into source
754 -- constructs and lead to confusing error diagnostics. Using an object
755 -- declaration prevents this unwanted side effect.
757 if Nkind
(Nam
) = N_Function_Call
then
759 Make_Object_Declaration
(Loc
,
760 Defining_Identifier
=> Obj_Id
,
761 Constant_Present
=> True,
762 Object_Definition
=> New_Occurrence_Of
(Typ
, Loc
),
765 -- Inherit the original Comes_From_Source status of the renaming
767 Set_Comes_From_Source
(N
, CFS
);
769 -- Sever the link to the renamed function result because the entity
770 -- will no longer alias anything.
772 Set_Renamed_Object
(Obj_Id
, Empty
);
774 -- Remove the entity of the renaming declaration from visibility as
775 -- the analysis of the object declaration will reintroduce it again.
777 Remove_Entity_And_Homonym
(Obj_Id
);
780 -- Otherwise unconditionally remove all side effects from the name
785 end Expand_SPARK_N_Object_Renaming_Declaration
;
787 --------------------------
788 -- Expand_SPARK_N_Op_Ne --
789 --------------------------
791 procedure Expand_SPARK_N_Op_Ne
(N
: Node_Id
) is
792 Typ
: constant Entity_Id
:= Etype
(Left_Opnd
(N
));
795 -- Case of elementary type with standard operator
797 if Is_Elementary_Type
(Typ
)
798 and then Sloc
(Entity
(N
)) = Standard_Location
803 Exp_Ch4
.Expand_N_Op_Ne
(N
);
805 end Expand_SPARK_N_Op_Ne
;
807 -------------------------------------
808 -- Expand_SPARK_Potential_Renaming --
809 -------------------------------------
811 procedure Expand_SPARK_Potential_Renaming
(N
: Node_Id
) is
812 function In_Insignificant_Pragma
(Nod
: Node_Id
) return Boolean;
813 -- Determine whether arbitrary node Nod appears within a significant
816 -----------------------------
817 -- In_Insignificant_Pragma --
818 -----------------------------
820 function In_Insignificant_Pragma
(Nod
: Node_Id
) return Boolean is
824 -- Climb the parent chain looking for an enclosing pragma
827 while Present
(Par
) loop
828 if Nkind
(Par
) = N_Pragma
then
829 return not Pragma_Significant_In_SPARK
(Get_Pragma_Id
(Par
));
831 -- Prevent the search from going too far
833 elsif Is_Body_Or_Package_Declaration
(Par
) then
841 end In_Insignificant_Pragma
;
845 Loc
: constant Source_Ptr
:= Sloc
(N
);
846 Obj_Id
: constant Entity_Id
:= Entity
(N
);
847 Typ
: constant Entity_Id
:= Etype
(N
);
850 -- Start of processing for Expand_SPARK_Potential_Renaming
853 -- Replace a reference to a renaming with the actual renamed object.
854 -- Protect against previous errors leaving no entity in N.
857 and then Is_Object
(Obj_Id
)
859 Ren
:= Renamed_Object
(Obj_Id
);
861 if Present
(Ren
) then
863 -- Do not process a reference when it appears within a pragma of
864 -- no significance to SPARK. It is assumed that the replacement
865 -- will violate the semantics of the pragma and cause a spurious
868 if In_Insignificant_Pragma
(N
) then
871 -- Instantiations and inlining of subprograms employ "prologues"
872 -- which map actual to formal parameters by means of renamings.
873 -- Replace a reference to a formal by the corresponding actual
876 elsif Nkind
(Ren
) in N_Entity
then
877 Rewrite
(N
, New_Occurrence_Of
(Ren
, Loc
));
879 -- Otherwise the renamed object denotes a name
882 Rewrite
(N
, New_Copy_Tree
(Ren
, New_Sloc
=> Loc
));
883 Reset_Analyzed_Flags
(N
);
886 Analyze_And_Resolve
(N
, Typ
);
889 end Expand_SPARK_Potential_Renaming
;
891 -----------------------
892 -- SPARK_Freeze_Type --
893 -----------------------
895 procedure SPARK_Freeze_Type
(N
: Entity_Id
) is
896 Typ
: constant Entity_Id
:= Entity
(N
);
898 Renamed_Eq
: Node_Id
;
899 -- Defining unit name for the predefined equality function in the case
900 -- where the type has a primitive operation that is a renaming of
901 -- predefined equality (but only if there is also an overriding
902 -- user-defined equality function). Used to pass this entity from
903 -- Make_Predefined_Primitive_Specs to Predefined_Primitive_Bodies.
906 Eq_Spec
: Node_Id
:= Empty
;
907 Predef_List
: List_Id
;
909 Wrapper_Decl_List
: List_Id
;
910 Wrapper_Body_List
: List_Id
:= No_List
;
912 Saved_GM
: constant Ghost_Mode_Type
:= Ghost_Mode
;
913 Saved_IGR
: constant Node_Id
:= Ignored_Ghost_Region
;
914 -- Save the Ghost-related attributes to restore on exit
917 -- The type being frozen may be subject to pragma Ghost. Set the mode
918 -- now to ensure that any nodes generated during freezing are properly
921 Set_Ghost_Mode
(Typ
);
923 -- When a DIC is inherited by a tagged type, it may need to be
924 -- specialized to the descendant type, hence build a separate DIC
925 -- procedure for it as done during regular expansion for compilation.
927 if Has_DIC
(Typ
) and then Is_Tagged_Type
(Typ
) then
928 -- Why is this needed for DIC, but not for other aspects (such as
929 -- Type_Invariant)???
931 Build_DIC_Procedure_Body
(Typ
);
934 if Ekind
(Typ
) = E_Record_Type
935 and then Is_Tagged_Type
(Typ
)
936 and then not Is_Interface
(Typ
)
937 and then not Is_Limited_Type
(Typ
)
939 if Is_CPP_Class
(Root_Type
(Typ
))
940 and then Convention
(Typ
) = Convention_CPP
944 -- Do not add the spec of the predefined primitives if we are
945 -- compiling under restriction No_Dispatching_Calls.
947 elsif not Restriction_Active
(No_Dispatching_Calls
) then
948 Set_Is_Frozen
(Typ
, False);
950 Predef_List
:= New_List
;
951 Exp_Ch3
.Make_Predefined_Primitive_Eq_Spec
952 (Typ
, Predef_List
, Renamed_Eq
);
953 Eq_Spec
:= First
(Predef_List
);
954 Insert_List_Before_And_Analyze
(N
, Predef_List
);
958 -- Remove link from the parent list to the spec and body of
959 -- the dispatching equality, but keep the link in the opposite
960 -- direction, to allow up-traversal of the AST.
962 if Present
(Eq_Spec
) then
963 Decl
:= Parent
(Eq_Spec
);
965 Set_Parent
(Eq_Spec
, Decl
);
970 if Ekind
(Typ
) = E_Record_Type
971 and then Is_Tagged_Type
(Typ
)
972 and then not Is_CPP_Class
(Typ
)
974 -- Ada 2005 (AI-391): For a nonabstract null extension, create
975 -- wrapper functions for each nonoverridden inherited function
976 -- with a controlling result of the type. The wrapper for such
977 -- a function returns an extension aggregate that invokes the
980 if Ada_Version
>= Ada_2005
981 and then not Is_Abstract_Type
(Typ
)
982 and then Is_Null_Extension
(Typ
)
984 Exp_Ch3
.Make_Controlling_Function_Wrappers
985 (Typ
, Wrapper_Decl_List
, Wrapper_Body_List
);
986 Insert_List_Before_And_Analyze
(N
, Wrapper_Decl_List
);
989 -- Ada 2005 (AI-391): If any wrappers were created for nonoverridden
990 -- inherited functions, then add their bodies to the AST, so they
991 -- will be processed like ordinary subprogram bodies (even though the
992 -- compiler adds them into the freezing action).
994 if not Is_Interface
(Typ
) then
995 Insert_List_Before_And_Analyze
(N
, Wrapper_Body_List
);
999 Restore_Ghost_Region
(Saved_GM
, Saved_IGR
);
1000 end SPARK_Freeze_Type
;