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_Ch4; use Exp_Ch4;
29 with Exp_Dbug; use Exp_Dbug;
30 with Exp_Util; use Exp_Util;
31 with Sem_Aux; use Sem_Aux;
32 with Sem_Res; use Sem_Res;
33 with Sem_Util; use Sem_Util;
34 with Sinfo; use Sinfo;
35 with Stand; use Stand;
37 package body Exp_SPARK is
39 -----------------------
40 -- Local Subprograms --
41 -----------------------
43 procedure Expand_SPARK_Call (N : Node_Id);
44 -- This procedure contains common processing for function and procedure
45 -- calls: replacement of renaming by subprogram renamed
47 procedure Expand_SPARK_N_Object_Renaming_Declaration (N : Node_Id);
48 -- Perform name evaluation for a renamed object
50 procedure Expand_Potential_Renaming (N : Node_Id);
51 -- N denotes a N_Identifier or N_Expanded_Name. If N references a renaming,
52 -- replace N with the renamed object.
58 procedure Expand_SPARK (N : Node_Id) is
62 -- Qualification of entity names in formal verification mode
63 -- is limited to the addition of a suffix for homonyms (see
64 -- Exp_Dbug.Qualify_Entity_Name). We used to qualify entity names
65 -- as full expansion does, but this was removed as this prevents the
66 -- verification back-end from using a short name for debugging and
67 -- user interaction. The verification back-end already takes care
68 -- of qualifying names when needed.
70 when N_Block_Statement |
72 N_Package_Declaration |
74 Qualify_Entity_Names (N);
76 when N_Subprogram_Call =>
77 Expand_SPARK_Call (N);
79 when N_Expanded_Name |
81 Expand_Potential_Renaming (N);
83 -- A NOT IN B gets transformed to NOT (A IN B). This is the same
84 -- expansion used in the normal case, so shared the code.
89 when N_Object_Renaming_Declaration =>
90 Expand_SPARK_N_Object_Renaming_Declaration (N);
92 -- In SPARK mode, no other constructs require expansion
99 -----------------------
100 -- Expand_SPARK_Call --
101 -----------------------
103 procedure Expand_SPARK_Call (N : Node_Id) is
104 Call_Node : constant Node_Id := N;
105 Parent_Subp : Entity_Id;
108 -- Ignore if previous error
110 if Nkind (Call_Node) in N_Has_Etype
111 and then Etype (Call_Node) = Any_Type
116 -- Call using access to subprogram with explicit dereference
118 if Nkind (Name (Call_Node)) = N_Explicit_Dereference then
119 Parent_Subp := Empty;
121 -- Case of call to simple entry, where the Name is a selected component
122 -- whose prefix is the task, and whose selector name is the entry name
124 elsif Nkind (Name (Call_Node)) = N_Selected_Component then
125 Parent_Subp := Empty;
127 -- Case of call to member of entry family, where Name is an indexed
128 -- component, with the prefix being a selected component giving the
129 -- task and entry family name, and the index being the entry index.
131 elsif Nkind (Name (Call_Node)) = N_Indexed_Component then
132 Parent_Subp := Empty;
137 Parent_Subp := Alias (Entity (Name (Call_Node)));
140 -- If the subprogram is a renaming, replace it in the call with the name
141 -- of the actual subprogram being called.
143 if Present (Parent_Subp) then
144 Parent_Subp := Ultimate_Alias (Parent_Subp);
146 -- The below setting of Entity is suspect, see F109-018 discussion???
148 Set_Entity (Name (Call_Node), Parent_Subp);
150 end Expand_SPARK_Call;
152 ------------------------------------------------
153 -- Expand_SPARK_N_Object_Renaming_Declaration --
154 ------------------------------------------------
156 procedure Expand_SPARK_N_Object_Renaming_Declaration (N : Node_Id) is
158 -- Unconditionally remove all side effects from the name
160 Evaluate_Name (Name (N));
161 end Expand_SPARK_N_Object_Renaming_Declaration;
163 -------------------------------
164 -- Expand_Potential_Renaming --
165 -------------------------------
167 procedure Expand_Potential_Renaming (N : Node_Id) is
168 E : constant Entity_Id := Entity (N);
169 T : constant Entity_Id := Etype (N);
172 -- Replace a reference to a renaming with the actual renamed object
174 if Ekind (E) in Object_Kind and then Present (Renamed_Object (E)) then
175 Rewrite (N, New_Copy_Tree (Renamed_Object (E)));
176 Reset_Analyzed_Flags (N);
177 Analyze_And_Resolve (N, T);
179 end Expand_Potential_Renaming;