1 ------------------------------------------------------------------------------
3 -- GNAT COMPILER COMPONENTS --
5 -- E X P _ S P A R K --
9 -- Copyright (C) 1992-2013, 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 Einfo
; use Einfo
;
28 with Exp_Dbug
; use Exp_Dbug
;
29 with Exp_Util
; use Exp_Util
;
30 with Sem_Aux
; use Sem_Aux
;
31 with Sem_Res
; use Sem_Res
;
32 with Sem_Util
; use Sem_Util
;
33 with Sinfo
; use Sinfo
;
34 with Stand
; use Stand
;
36 package body Exp_SPARK
is
38 -----------------------
39 -- Local Subprograms --
40 -----------------------
42 procedure Expand_SPARK_Call
(N
: Node_Id
);
43 -- This procedure contains common processing for function and procedure
44 -- calls: replacement of renaming by subprogram renamed
46 procedure Expand_SPARK_N_Object_Renaming_Declaration
(N
: Node_Id
);
47 -- Perform name evaluation for a renamed object
49 procedure Expand_Potential_Renaming
(N
: Node_Id
);
50 -- N denotes a N_Identifier or N_Expanded_Name. If N references a renaming,
51 -- replace N with the renamed object.
57 procedure Expand_SPARK
(N
: Node_Id
) is
61 -- Qualification of entity names in formal verification mode
62 -- is limited to the addition of a suffix for homonyms (see
63 -- Exp_Dbug.Qualify_Entity_Name). We used to qualify entity names
64 -- as full expansion does, but this was removed as this prevents the
65 -- verification back-end from using a short name for debugging and
66 -- user interaction. The verification back-end already takes care
67 -- of qualifying names when needed.
69 when N_Block_Statement |
71 N_Package_Declaration |
73 Qualify_Entity_Names
(N
);
75 when N_Subprogram_Call
=>
76 Expand_SPARK_Call
(N
);
78 when N_Expanded_Name |
80 Expand_Potential_Renaming
(N
);
82 when N_Object_Renaming_Declaration
=>
83 Expand_SPARK_N_Object_Renaming_Declaration
(N
);
85 -- In SPARK mode, no other constructs require expansion
92 -----------------------
93 -- Expand_SPARK_Call --
94 -----------------------
96 procedure Expand_SPARK_Call
(N
: Node_Id
) is
97 Call_Node
: constant Node_Id
:= N
;
98 Parent_Subp
: Entity_Id
;
101 -- Ignore if previous error
103 if Nkind
(Call_Node
) in N_Has_Etype
104 and then Etype
(Call_Node
) = Any_Type
109 -- Call using access to subprogram with explicit dereference
111 if Nkind
(Name
(Call_Node
)) = N_Explicit_Dereference
then
112 Parent_Subp
:= Empty
;
114 -- Case of call to simple entry, where the Name is a selected component
115 -- whose prefix is the task, and whose selector name is the entry name
117 elsif Nkind
(Name
(Call_Node
)) = N_Selected_Component
then
118 Parent_Subp
:= Empty
;
120 -- Case of call to member of entry family, where Name is an indexed
121 -- component, with the prefix being a selected component giving the
122 -- task and entry family name, and the index being the entry index.
124 elsif Nkind
(Name
(Call_Node
)) = N_Indexed_Component
then
125 Parent_Subp
:= Empty
;
130 Parent_Subp
:= Alias
(Entity
(Name
(Call_Node
)));
133 -- If the subprogram is a renaming, replace it in the call with the name
134 -- of the actual subprogram being called.
136 if Present
(Parent_Subp
) then
137 Parent_Subp
:= Ultimate_Alias
(Parent_Subp
);
139 -- The below setting of Entity is suspect, see F109-018 discussion???
141 Set_Entity
(Name
(Call_Node
), Parent_Subp
);
143 end Expand_SPARK_Call
;
145 ------------------------------------------------
146 -- Expand_SPARK_N_Object_Renaming_Declaration --
147 ------------------------------------------------
149 procedure Expand_SPARK_N_Object_Renaming_Declaration
(N
: Node_Id
) is
151 -- Unconditionally remove all side effects from the name
153 Evaluate_Name
(Name
(N
));
154 end Expand_SPARK_N_Object_Renaming_Declaration
;
156 -------------------------------
157 -- Expand_Potential_Renaming --
158 -------------------------------
160 procedure Expand_Potential_Renaming
(N
: Node_Id
) is
161 E
: constant Entity_Id
:= Entity
(N
);
162 T
: constant Entity_Id
:= Etype
(N
);
165 -- Replace a reference to a renaming with the actual renamed object
167 if Ekind
(E
) in Object_Kind
and then Present
(Renamed_Object
(E
)) then
168 Rewrite
(N
, New_Copy_Tree
(Renamed_Object
(E
)));
169 Reset_Analyzed_Flags
(N
);
170 Analyze_And_Resolve
(N
, T
);
172 end Expand_Potential_Renaming
;