]>
Commit | Line | Data |
---|---|---|
996ae0b0 RK |
1 | ------------------------------------------------------------------------------ |
2 | -- -- | |
3 | -- GNAT COMPILER COMPONENTS -- | |
4 | -- -- | |
5 | -- S E M _ P R A G -- | |
6 | -- -- | |
7 | -- S p e c -- | |
8 | -- -- | |
9420f51f | 9 | -- Copyright (C) 1992-2014, Free Software Foundation, Inc. -- |
996ae0b0 RK |
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- -- | |
b5c84c3c | 13 | -- ware Foundation; either version 3, or (at your option) any later ver- -- |
996ae0b0 RK |
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 -- | |
b5c84c3c RD |
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. -- | |
996ae0b0 RK |
20 | -- -- |
21 | -- GNAT was originally developed by the GNAT team at New York University. -- | |
71ff80dc | 22 | -- Extensive contributions were provided by Ada Core Technologies Inc. -- |
996ae0b0 RK |
23 | -- -- |
24 | ------------------------------------------------------------------------------ | |
25 | ||
26 | -- Pragma handling is isolated in a separate package | |
27 | -- (logically this processing belongs in chapter 4) | |
28 | ||
e28072cd | 29 | with Namet; use Namet; |
43417b90 | 30 | with Opt; use Opt; |
e28072cd AC |
31 | with Snames; use Snames; |
32 | with Types; use Types; | |
f02b8bb8 | 33 | |
996ae0b0 RK |
34 | package Sem_Prag is |
35 | ||
2c9f8c0a AC |
36 | -- The following table lists all pragmas that act as an assertion |
37 | -- expression. | |
38 | ||
39 | Assertion_Expression_Pragma : constant array (Pragma_Id) of Boolean := | |
40 | (Pragma_Assert => True, | |
41 | Pragma_Assert_And_Cut => True, | |
42 | Pragma_Assume => True, | |
43 | Pragma_Check => True, | |
44 | Pragma_Contract_Cases => True, | |
45 | Pragma_Initial_Condition => True, | |
46 | Pragma_Invariant => True, | |
47 | Pragma_Loop_Invariant => True, | |
48 | Pragma_Loop_Variant => True, | |
49 | Pragma_Post => True, | |
50 | Pragma_Post_Class => True, | |
51 | Pragma_Postcondition => True, | |
52 | Pragma_Pre => True, | |
53 | Pragma_Pre_Class => True, | |
54 | Pragma_Precondition => True, | |
55 | Pragma_Predicate => True, | |
56 | Pragma_Refined_Post => True, | |
57 | Pragma_Test_Case => True, | |
58 | Pragma_Type_Invariant => True, | |
59 | Pragma_Type_Invariant_Class => True, | |
60 | others => False); | |
61 | ||
15918371 | 62 | -- The following table lists all the implementation-defined pragmas that |
e7f23f06 AC |
63 | -- may apply to a body stub (no language defined pragmas apply). The table |
64 | -- should be synchronized with Aspect_On_Body_Or_Stub_OK in unit Aspects if | |
65 | -- the pragmas below implement an aspect. | |
e28072cd | 66 | |
e7f23f06 | 67 | Pragma_On_Body_Or_Stub_OK : constant array (Pragma_Id) of Boolean := |
ea3c0651 AC |
68 | (Pragma_Refined_Depends => True, |
69 | Pragma_Refined_Global => True, | |
70 | Pragma_Refined_Post => True, | |
ea3c0651 AC |
71 | Pragma_SPARK_Mode => True, |
72 | Pragma_Warnings => True, | |
73 | others => False); | |
e28072cd | 74 | |
21d27997 RD |
75 | ----------------- |
76 | -- Subprograms -- | |
77 | ----------------- | |
78 | ||
996ae0b0 RK |
79 | procedure Analyze_Pragma (N : Node_Id); |
80 | -- Analyze procedure for pragma reference node N | |
81 | ||
5afe5d2d HK |
82 | procedure Analyze_Contract_Cases_In_Decl_Part (N : Node_Id); |
83 | -- Perform full analysis and expansion of delayed pragma Contract_Cases | |
dac3bede | 84 | |
d6095153 | 85 | procedure Analyze_Depends_In_Decl_Part (N : Node_Id); |
39d3009f AC |
86 | -- Perform full analysis of delayed pragma Depends. This routine is also |
87 | -- capable of performing basic analysis of pragma Refined_Depends. | |
d6095153 | 88 | |
f1bd0415 | 89 | procedure Analyze_External_Property_In_Decl_Part |
6c3c671e AC |
90 | (N : Node_Id; |
91 | Expr_Val : out Boolean); | |
92 | -- Perform full analysis of delayed pragmas Async_Readers, Async_Writers, | |
93 | -- Effective_Reads and Effective_Writes. Flag Expr_Val contains the Boolean | |
94 | -- argument of the pragma or a default True if no argument is present. | |
95 | ||
d6095153 | 96 | procedure Analyze_Global_In_Decl_Part (N : Node_Id); |
39d3009f AC |
97 | -- Perform full analysis of delayed pragma Global. This routine is also |
98 | -- capable of performing basic analysis of pragma Refind_Global. | |
d6095153 | 99 | |
9b2451e5 AC |
100 | procedure Analyze_Initial_Condition_In_Decl_Part (N : Node_Id); |
101 | -- Perform full analysis of delayed pragma Initial_Condition | |
102 | ||
54e28df2 HK |
103 | procedure Analyze_Initializes_In_Decl_Part (N : Node_Id); |
104 | -- Perform full analysis of delayed pragma Initializes | |
105 | ||
ea3c0651 AC |
106 | procedure Analyze_Pre_Post_Condition_In_Decl_Part |
107 | (Prag : Node_Id; | |
108 | Subp_Id : Entity_Id); | |
109 | -- Perform preanalysis of a [refined] precondition or postcondition that | |
110 | -- appears on a subprogram declaration or body [stub]. Prag denotes the | |
111 | -- pragma, Subp_Id is the entity of the related subprogram. The preanalysis | |
112 | -- of the expression is done as "spec expression" (see section "Handling | |
113 | -- of Default and Per-Object Expressions in Sem). | |
114 | ||
115 | procedure Analyze_Refined_Depends_In_Decl_Part (N : Node_Id); | |
39d3009f AC |
116 | -- Preform full analysis of delayed pragma Refined_Depends. This routine |
117 | -- uses Analyze_Depends_In_Decl_Part as a starting point, then performs | |
118 | -- various consistency checks between Depends and Refined_Depends. | |
ea3c0651 AC |
119 | |
120 | procedure Analyze_Refined_Global_In_Decl_Part (N : Node_Id); | |
39d3009f AC |
121 | -- Perform full analysis of delayed pragma Refined_Global. This routine |
122 | -- uses Analyze_Global_In_Decl_Part as a starting point, then performs | |
123 | -- various consistency checks between Global and Refined_Global. | |
b285815e | 124 | |
39af2bac AC |
125 | procedure Analyze_Refined_State_In_Decl_Part (N : Node_Id); |
126 | -- Perform full analysis of delayed pragma Refined_State | |
127 | ||
5afe5d2d | 128 | procedure Analyze_Test_Case_In_Decl_Part (N : Node_Id; S : Entity_Id); |
ea3c0651 AC |
129 | -- Perform preanalysis of pragma Test_Case that applies to a subprogram |
130 | -- declaration. Parameter N denotes the pragma, S is the entity of the | |
131 | -- related subprogram. The preanalysis of the expression is done as "spec | |
132 | -- expression" (see section "Handling of Default and Per-Object Expressions | |
133 | -- in Sem). | |
5afe5d2d | 134 | |
aab45d22 AC |
135 | procedure Check_Applicable_Policy (N : Node_Id); |
136 | -- N is either an N_Aspect or an N_Pragma node. There are two cases. If | |
16d3a853 AC |
137 | -- the name of the aspect or pragma is not one of those recognized as |
138 | -- an assertion kind by an Assertion_Policy pragma, then the call has | |
139 | -- no effect. Note that in the case of a pragma derived from an aspect, | |
140 | -- the name we use for the purpose of this procedure is the aspect name, | |
141 | -- which may be different from the pragma name (e.g. Precondition for | |
142 | -- Pre aspect). In addition, 'Class aspects are recognized (and the | |
143 | -- corresponding special names used in the processing). | |
aab45d22 | 144 | -- |
16d3a853 | 145 | -- If the name is a valid assertion kind name, then the Check_Policy pragma |
aab45d22 AC |
146 | -- chain is checked for a matching entry (or for an Assertion entry which |
147 | -- matches all possibilities). If a matching entry is found then the policy | |
3699edc4 AC |
148 | -- is checked. If it is On or Check, then the Is_Checked flag is set in |
149 | -- the aspect or pragma node. If it is Off, Ignore, or Disable, then the | |
150 | -- Is_Ignored flag is set in the aspect or pragma node. Additionally for | |
151 | -- policy Disable, the Is_Disabled flag is set. | |
aab45d22 AC |
152 | -- |
153 | -- If no matching Check_Policy pragma is found then the effect depends on | |
154 | -- whether -gnata was used, if so, then the call has no effect, otherwise | |
155 | -- Is_Ignored (but not Is_Disabled) is set True. | |
21d27997 | 156 | |
6c3c671e AC |
157 | procedure Check_External_Properties |
158 | (Item : Node_Id; | |
159 | AR : Boolean; | |
160 | AW : Boolean; | |
161 | ER : Boolean; | |
162 | EW : Boolean); | |
163 | -- Flags AR, AW, ER and EW denote the static values of external properties | |
164 | -- Async_Readers, Async_Writers, Effective_Reads and Effective_Writes. Item | |
84f80f5b AC |
165 | -- is the related variable or state. Ensure legality of the combination and |
166 | -- issue an error for an illegal combination. | |
6c3c671e | 167 | |
d7af5ea5 HK |
168 | procedure Check_Missing_Part_Of (Item_Id : Entity_Id); |
169 | -- Determine whether the placement within the state space of an abstract | |
170 | -- state, variable or package instantiation denoted by Item_Id requires the | |
171 | -- use of indicator/option Part_Of. If this is the case, emit an error. | |
172 | ||
9420f51f YM |
173 | procedure Collect_Subprogram_Inputs_Outputs |
174 | (Subp_Id : Entity_Id; | |
175 | Subp_Inputs : in out Elist_Id; | |
176 | Subp_Outputs : in out Elist_Id; | |
177 | Global_Seen : out Boolean); | |
178 | -- Used during the analysis of pragmas Depends, Global, Refined_Depends, | |
179 | -- and Refined_Global. Also used by GNATprove. Gathers all inputs and | |
180 | -- outputs of subprogram Subp_Id in lists Subp_Inputs and Subp_Outputs. | |
181 | -- If subprogram has no inputs and/or outputs, then the returned list | |
182 | -- is No_Elist. Global_Seen is set when the related subprogram has | |
183 | -- pragma [Refined_]Global. | |
184 | ||
fbf5a39b | 185 | function Delay_Config_Pragma_Analyze (N : Node_Id) return Boolean; |
f02b8bb8 RD |
186 | -- N is a pragma appearing in a configuration pragma file. Most such |
187 | -- pragmas are analyzed when the file is read, before parsing and analyzing | |
188 | -- the main unit. However, the analysis of certain pragmas results in | |
189 | -- adding information to the compiled main unit, and this cannot be done | |
190 | -- till the main unit is processed. Such pragmas return True from this | |
191 | -- function and in Frontend pragmas where Delay_Config_Pragma_Analyze is | |
192 | -- True have their analysis delayed until after the main program is parsed | |
193 | -- and analyzed. | |
fbf5a39b | 194 | |
43417b90 AC |
195 | function Get_SPARK_Mode_From_Pragma (N : Node_Id) return SPARK_Mode_Type; |
196 | -- Given a pragma SPARK_Mode node, return corresponding mode id | |
1c6269d3 | 197 | |
21d27997 RD |
198 | procedure Initialize; |
199 | -- Initializes data structures used for pragma processing. Must be called | |
200 | -- before analyzing each new main source program. | |
201 | ||
20a65dcb RD |
202 | function Is_Config_Static_String (Arg : Node_Id) return Boolean; |
203 | -- This is called for a configuration pragma that requires either string | |
204 | -- literal or a concatenation of string literals. We cannot use normal | |
205 | -- static string processing because it is too early in the case of the | |
206 | -- pragma appearing in a configuration pragmas file. If Arg is of an | |
207 | -- appropriate form, then this call obtains the string (doing any necessary | |
208 | -- concatenations) and places it in Name_Buffer, setting Name_Len to its | |
209 | -- length, and then returns True. If it is not of the correct form, then an | |
210 | -- appropriate error message is posted, and False is returned. | |
211 | ||
1c6269d3 HK |
212 | function Is_Elaboration_SPARK_Mode (N : Node_Id) return Boolean; |
213 | -- Determine whether pragma SPARK_Mode appears in the statement part of a | |
214 | -- package body. | |
215 | ||
fbf5a39b AC |
216 | function Is_Non_Significant_Pragma_Reference (N : Node_Id) return Boolean; |
217 | -- The node N is a node for an entity and the issue is whether the | |
f02b8bb8 RD |
218 | -- occurrence is a reference for the purposes of giving warnings about |
219 | -- unreferenced variables. This function returns True if the reference is | |
220 | -- not a reference from this point of view (e.g. the occurrence in a pragma | |
f3d57416 | 221 | -- Pack) and False if it is a real reference (e.g. the occurrence in a |
f02b8bb8 | 222 | -- pragma Export); |
fbf5a39b | 223 | |
996ae0b0 | 224 | function Is_Pragma_String_Literal (Par : Node_Id) return Boolean; |
f02b8bb8 RD |
225 | -- Given an N_Pragma_Argument_Association node, Par, which has the form of |
226 | -- an operator symbol, determines whether or not it should be treated as an | |
227 | -- string literal. This is called by Sem_Ch6.Analyze_Operator_Symbol. If | |
228 | -- True is returned, the argument is converted to a string literal. If | |
996ae0b0 RK |
229 | -- False is returned, then the argument is treated as an entity reference |
230 | -- to the operator. | |
231 | ||
1c6269d3 HK |
232 | function Is_Private_SPARK_Mode (N : Node_Id) return Boolean; |
233 | -- Determine whether pragma SPARK_Mode appears in the private part of a | |
234 | -- package. | |
235 | ||
20a65dcb RD |
236 | function Is_Valid_Assertion_Kind (Nam : Name_Id) return Boolean; |
237 | -- Returns True if Nam is one of the names recognized as a valid assertion | |
238 | -- kind by the Assertion_Policy pragma. Note that the 'Class cases are | |
239 | -- represented by the corresponding special names Name_uPre, Name_uPost, | |
240 | -- Name_uInviarnat, and Name_uType_Invariant (_Pre, _Post, _Invariant, | |
241 | -- and _Type_Invariant). | |
5950a3ac | 242 | |
f6834394 VP |
243 | procedure Make_Aspect_For_PPC_In_Gen_Sub_Decl (Decl : Node_Id); |
244 | -- This routine makes aspects from precondition or postcondition pragmas | |
245 | -- that appear within a generic subprogram declaration. Decl is the generic | |
dd91386d AC |
246 | -- subprogram declaration node. Note that the aspects are attached to the |
247 | -- generic copy and also to the orginal tree. | |
f6834394 | 248 | |
996ae0b0 | 249 | procedure Process_Compilation_Unit_Pragmas (N : Node_Id); |
f02b8bb8 RD |
250 | -- Called at the start of processing compilation unit N to deal with any |
251 | -- special issues regarding pragmas. In particular, we have to deal with | |
c775c209 AC |
252 | -- Suppress_All at this stage, since it can appear after the unit instead |
253 | -- of before (actually we allow it to appear anywhere). | |
996ae0b0 | 254 | |
e7f23f06 AC |
255 | procedure Relocate_Pragmas_To_Body |
256 | (Subp_Body : Node_Id; | |
257 | Target_Body : Node_Id := Empty); | |
258 | -- Resocate all pragmas that follow and apply to subprogram body Subp_Body | |
259 | -- to its own declaration list. Candidate pragmas are classified in table | |
260 | -- Pragma_On_Body_Or_Stub_OK. If Target_Body is set, the pragma are moved | |
261 | -- to the declarations of Target_Body. This formal should be set when | |
262 | -- dealing with subprogram body stubs or expression functions. | |
263 | ||
996ae0b0 | 264 | procedure Set_Encoded_Interface_Name (E : Entity_Id; S : Node_Id); |
21c51f53 RD |
265 | -- This routine is used to set an encoded interface name. The node S is |
266 | -- an N_String_Literal node for the external name to be set, and E is an | |
f02b8bb8 RD |
267 | -- entity whose Interface_Name field is to be set. In the normal case where |
268 | -- S contains a name that is a valid C identifier, then S is simply set as | |
21c51f53 RD |
269 | -- the value of the Interface_Name. Otherwise it is encoded as needed by |
270 | -- particular operating systems. See the body for details of the encoding. | |
996ae0b0 RK |
271 | |
272 | end Sem_Prag; |