File : 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-2016, 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 Einfo; use Einfo;
28 with Exp_Ch5; use Exp_Ch5;
29 with Exp_Dbug; use Exp_Dbug;
30 with Exp_Util; use Exp_Util;
31 with Sem_Res; use Sem_Res;
32 with Sem_Util; use Sem_Util;
33 with Sinfo; use Sinfo;
34 with Tbuild; use Tbuild;
35
36 package body Exp_SPARK is
37
38 -----------------------
39 -- Local Subprograms --
40 -----------------------
41
42 procedure Expand_SPARK_N_Object_Renaming_Declaration (N : Node_Id);
43 -- Perform name evaluation for a renamed object
44
45 ------------------
46 -- Expand_SPARK --
47 ------------------
48
49 procedure Expand_SPARK (N : Node_Id) is
50 begin
51 case Nkind (N) is
52
53 -- Qualification of entity names in formal verification mode
54 -- is limited to the addition of a suffix for homonyms (see
55 -- Exp_Dbug.Qualify_Entity_Name). We used to qualify entity names
56 -- as full expansion does, but this was removed as this prevents the
57 -- verification back-end from using a short name for debugging and
58 -- user interaction. The verification back-end already takes care
59 -- of qualifying names when needed.
60
61 when N_Block_Statement |
62 N_Entry_Declaration |
63 N_Package_Body |
64 N_Package_Declaration |
65 N_Protected_Type_Declaration |
66 N_Subprogram_Body |
67 N_Task_Type_Declaration =>
68 Qualify_Entity_Names (N);
69
70 when N_Expanded_Name |
71 N_Identifier =>
72 Expand_SPARK_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_SPARK_Potential_Renaming --
117 -------------------------------------
118
119 procedure Expand_SPARK_Potential_Renaming (N : Node_Id) is
120 Loc : constant Source_Ptr := Sloc (N);
121 Ren_Id : constant Entity_Id := Entity (N);
122 Typ : constant Entity_Id := Etype (N);
123 Obj_Id : Node_Id;
124
125 begin
126 -- Replace a reference to a renaming with the actual renamed object
127
128 if Ekind (Ren_Id) in Object_Kind then
129 Obj_Id := Renamed_Object (Ren_Id);
130
131 if Present (Obj_Id) then
132
133 -- The renamed object is an entity when instantiating generics
134 -- or inlining bodies. In this case the renaming is part of the
135 -- mapping "prologue" which links actuals to formals.
136
137 if Nkind (Obj_Id) in N_Entity then
138 Rewrite (N, New_Occurrence_Of (Obj_Id, Loc));
139
140 -- Otherwise the renamed object denotes a name
141
142 else
143 Rewrite (N, New_Copy_Tree (Obj_Id));
144 Reset_Analyzed_Flags (N);
145 end if;
146
147 Analyze_And_Resolve (N, Typ);
148 end if;
149 end if;
150 end Expand_SPARK_Potential_Renaming;
151
152 end Exp_SPARK;