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-2015, 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
26with Atree;    use Atree;
27with Einfo;    use Einfo;
28with Exp_Ch5;  use Exp_Ch5;
29with Exp_Dbug; use Exp_Dbug;
30with Exp_Util; use Exp_Util;
31with Sem_Res;  use Sem_Res;
32with Sem_Util; use Sem_Util;
33with Sinfo;    use Sinfo;
34
35package body Exp_SPARK is
36
37   -----------------------
38   -- Local Subprograms --
39   -----------------------
40
41   procedure Expand_SPARK_N_Object_Renaming_Declaration (N : Node_Id);
42   --  Perform name evaluation for a renamed object
43
44   procedure Expand_Potential_Renaming (N : Node_Id);
45   --  N denotes a N_Identifier or N_Expanded_Name. If N references a renaming,
46   --  replace N with the renamed object.
47
48   ------------------
49   -- Expand_SPARK --
50   ------------------
51
52   procedure Expand_SPARK (N : Node_Id) is
53   begin
54      case Nkind (N) is
55
56         --  Qualification of entity names in formal verification mode
57         --  is limited to the addition of a suffix for homonyms (see
58         --  Exp_Dbug.Qualify_Entity_Name). We used to qualify entity names
59         --  as full expansion does, but this was removed as this prevents the
60         --  verification back-end from using a short name for debugging and
61         --  user interaction. The verification back-end already takes care
62         --  of qualifying names when needed.
63
64         when N_Block_Statement     |
65              N_Package_Body        |
66              N_Package_Declaration |
67              N_Subprogram_Body     =>
68            Qualify_Entity_Names (N);
69
70         when N_Expanded_Name |
71              N_Identifier    =>
72            Expand_Potential_Renaming (N);
73
74         when N_Object_Renaming_Declaration =>
75            Expand_SPARK_N_Object_Renaming_Declaration (N);
76
77         --  Loop iterations over arrays need to be expanded, to avoid getting
78         --  two names referring to the same object in memory (the array and
79         --  the iterator) in GNATprove, especially since both can be written
80         --  (thus possibly leading to interferences due to aliasing). No such
81         --  problem arises with quantified expressions over arrays, which are
82         --  dealt with specially in GNATprove.
83
84         when N_Loop_Statement =>
85            declare
86               Scheme : constant Node_Id := Iteration_Scheme (N);
87            begin
88               if Present (Scheme)
89                 and then Present (Iterator_Specification (Scheme))
90                 and then
91                   Is_Iterator_Over_Array (Iterator_Specification (Scheme))
92               then
93                  Expand_Iterator_Loop_Over_Array (N);
94               end if;
95            end;
96
97         --  In SPARK mode, no other constructs require expansion
98
99         when others =>
100            null;
101      end case;
102   end Expand_SPARK;
103
104   ------------------------------------------------
105   -- Expand_SPARK_N_Object_Renaming_Declaration --
106   ------------------------------------------------
107
108   procedure Expand_SPARK_N_Object_Renaming_Declaration (N : Node_Id) is
109   begin
110      --  Unconditionally remove all side effects from the name
111
112      Evaluate_Name (Name (N));
113   end Expand_SPARK_N_Object_Renaming_Declaration;
114
115   -------------------------------
116   -- Expand_Potential_Renaming --
117   -------------------------------
118
119   procedure Expand_Potential_Renaming (N : Node_Id) is
120      E : constant Entity_Id := Entity (N);
121      T : constant Entity_Id := Etype (N);
122
123   begin
124      --  Replace a reference to a renaming with the actual renamed object
125
126      if Ekind (E) in Object_Kind and then Present (Renamed_Object (E)) then
127         Rewrite (N, New_Copy_Tree (Renamed_Object (E)));
128         Reset_Analyzed_Flags (N);
129         Analyze_And_Resolve (N, T);
130      end if;
131   end Expand_Potential_Renaming;
132
133end Exp_SPARK;
134