]>
Commit | Line | Data |
---|---|---|
879ac954 AC |
1 | ------------------------------------------------------------------------------ |
2 | -- -- | |
3 | -- GNAT COMPILER COMPONENTS -- | |
4 | -- -- | |
5 | -- C O N T R A C T S -- | |
6 | -- -- | |
7 | -- B o d y -- | |
8 | -- -- | |
4dfba737 | 9 | -- Copyright (C) 2015-2018, Free Software Foundation, Inc. -- |
879ac954 AC |
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 Aspects; use Aspects; | |
27 | with Atree; use Atree; | |
5f325af2 | 28 | with Debug; use Debug; |
879ac954 AC |
29 | with Einfo; use Einfo; |
30 | with Elists; use Elists; | |
31 | with Errout; use Errout; | |
32 | with Exp_Prag; use Exp_Prag; | |
33 | with Exp_Tss; use Exp_Tss; | |
34 | with Exp_Util; use Exp_Util; | |
35 | with Namet; use Namet; | |
36 | with Nlists; use Nlists; | |
37 | with Nmake; use Nmake; | |
38 | with Opt; use Opt; | |
39 | with Sem; use Sem; | |
40 | with Sem_Aux; use Sem_Aux; | |
41 | with Sem_Ch6; use Sem_Ch6; | |
42 | with Sem_Ch8; use Sem_Ch8; | |
43 | with Sem_Ch12; use Sem_Ch12; | |
05662a06 | 44 | with Sem_Ch13; use Sem_Ch13; |
879ac954 AC |
45 | with Sem_Disp; use Sem_Disp; |
46 | with Sem_Prag; use Sem_Prag; | |
47 | with Sem_Util; use Sem_Util; | |
48 | with Sinfo; use Sinfo; | |
49 | with Snames; use Snames; | |
50 | with Stringt; use Stringt; | |
5f325af2 | 51 | with SCIL_LL; use SCIL_LL; |
879ac954 AC |
52 | with Tbuild; use Tbuild; |
53 | ||
54 | package body Contracts is | |
55 | ||
96e4fda5 HK |
56 | procedure Analyze_Package_Instantiation_Contract (Inst_Id : Entity_Id); |
57 | -- Analyze all delayed pragmas chained on the contract of package | |
58 | -- instantiation Inst_Id as if they appear at the end of a declarative | |
59 | -- region. The pragmas in question are: | |
60 | -- | |
61 | -- Part_Of | |
62 | ||
82e5c243 AC |
63 | procedure Build_And_Analyze_Contract_Only_Subprograms (L : List_Id); |
64 | -- (CodePeer): Subsidiary procedure to Analyze_Contracts which builds the | |
65 | -- contract-only subprogram body of eligible subprograms found in L, adds | |
66 | -- them to their corresponding list of declarations, and analyzes them. | |
67 | ||
879ac954 AC |
68 | procedure Expand_Subprogram_Contract (Body_Id : Entity_Id); |
69 | -- Expand the contracts of a subprogram body and its correspoding spec (if | |
70 | -- any). This routine processes all [refined] pre- and postconditions as | |
71 | -- well as Contract_Cases, invariants and predicates. Body_Id denotes the | |
72 | -- entity of the subprogram body. | |
73 | ||
74 | ----------------------- | |
75 | -- Add_Contract_Item -- | |
76 | ----------------------- | |
77 | ||
78 | procedure Add_Contract_Item (Prag : Node_Id; Id : Entity_Id) is | |
79 | Items : Node_Id := Contract (Id); | |
80 | ||
81 | procedure Add_Classification; | |
82 | -- Prepend Prag to the list of classifications | |
83 | ||
84 | procedure Add_Contract_Test_Case; | |
85 | -- Prepend Prag to the list of contract and test cases | |
86 | ||
87 | procedure Add_Pre_Post_Condition; | |
88 | -- Prepend Prag to the list of pre- and postconditions | |
89 | ||
90 | ------------------------ | |
91 | -- Add_Classification -- | |
92 | ------------------------ | |
93 | ||
94 | procedure Add_Classification is | |
95 | begin | |
96 | Set_Next_Pragma (Prag, Classifications (Items)); | |
97 | Set_Classifications (Items, Prag); | |
98 | end Add_Classification; | |
99 | ||
100 | ---------------------------- | |
101 | -- Add_Contract_Test_Case -- | |
102 | ---------------------------- | |
103 | ||
104 | procedure Add_Contract_Test_Case is | |
105 | begin | |
106 | Set_Next_Pragma (Prag, Contract_Test_Cases (Items)); | |
107 | Set_Contract_Test_Cases (Items, Prag); | |
108 | end Add_Contract_Test_Case; | |
109 | ||
110 | ---------------------------- | |
111 | -- Add_Pre_Post_Condition -- | |
112 | ---------------------------- | |
113 | ||
114 | procedure Add_Pre_Post_Condition is | |
115 | begin | |
116 | Set_Next_Pragma (Prag, Pre_Post_Conditions (Items)); | |
117 | Set_Pre_Post_Conditions (Items, Prag); | |
118 | end Add_Pre_Post_Condition; | |
119 | ||
120 | -- Local variables | |
121 | ||
879ac954 AC |
122 | -- A contract must contain only pragmas |
123 | ||
124 | pragma Assert (Nkind (Prag) = N_Pragma); | |
6e759c2a | 125 | Prag_Nam : constant Name_Id := Pragma_Name (Prag); |
533e3abc BD |
126 | |
127 | -- Start of processing for Add_Contract_Item | |
879ac954 | 128 | |
533e3abc | 129 | begin |
879ac954 AC |
130 | -- Create a new contract when adding the first item |
131 | ||
132 | if No (Items) then | |
133 | Items := Make_Contract (Sloc (Id)); | |
134 | Set_Contract (Id, Items); | |
135 | end if; | |
136 | ||
f99ff327 | 137 | -- Constants, the applicable pragmas are: |
879ac954 AC |
138 | -- Part_Of |
139 | ||
140 | if Ekind (Id) = E_Constant then | |
141 | if Prag_Nam = Name_Part_Of then | |
142 | Add_Classification; | |
143 | ||
144 | -- The pragma is not a proper contract item | |
145 | ||
146 | else | |
147 | raise Program_Error; | |
148 | end if; | |
149 | ||
f99ff327 AC |
150 | -- Entry bodies, the applicable pragmas are: |
151 | -- Refined_Depends | |
152 | -- Refined_Global | |
153 | -- Refined_Post | |
879ac954 | 154 | |
f99ff327 AC |
155 | elsif Is_Entry_Body (Id) then |
156 | if Nam_In (Prag_Nam, Name_Refined_Depends, Name_Refined_Global) then | |
879ac954 AC |
157 | Add_Classification; |
158 | ||
f99ff327 AC |
159 | elsif Prag_Nam = Name_Refined_Post then |
160 | Add_Pre_Post_Condition; | |
879ac954 AC |
161 | |
162 | -- The pragma is not a proper contract item | |
163 | ||
164 | else | |
165 | raise Program_Error; | |
166 | end if; | |
167 | ||
f99ff327 | 168 | -- Entry or subprogram declarations, the applicable pragmas are: |
c0dd5b38 | 169 | -- Attach_Handler |
879ac954 AC |
170 | -- Contract_Cases |
171 | -- Depends | |
172 | -- Extensions_Visible | |
173 | -- Global | |
c0dd5b38 | 174 | -- Interrupt_Handler |
879ac954 AC |
175 | -- Postcondition |
176 | -- Precondition | |
177 | -- Test_Case | |
178 | -- Volatile_Function | |
179 | ||
f99ff327 AC |
180 | elsif Is_Entry_Declaration (Id) |
181 | or else Ekind_In (Id, E_Function, | |
182 | E_Generic_Function, | |
183 | E_Generic_Procedure, | |
184 | E_Procedure) | |
879ac954 | 185 | then |
c0dd5b38 AC |
186 | if Nam_In (Prag_Nam, Name_Attach_Handler, Name_Interrupt_Handler) |
187 | and then Ekind_In (Id, E_Generic_Procedure, E_Procedure) | |
188 | then | |
189 | Add_Classification; | |
879ac954 AC |
190 | |
191 | elsif Nam_In (Prag_Nam, Name_Depends, | |
192 | Name_Extensions_Visible, | |
193 | Name_Global) | |
194 | then | |
195 | Add_Classification; | |
196 | ||
197 | elsif Prag_Nam = Name_Volatile_Function | |
198 | and then Ekind_In (Id, E_Function, E_Generic_Function) | |
199 | then | |
200 | Add_Classification; | |
201 | ||
c0dd5b38 AC |
202 | elsif Nam_In (Prag_Nam, Name_Contract_Cases, Name_Test_Case) then |
203 | Add_Contract_Test_Case; | |
204 | ||
205 | elsif Nam_In (Prag_Nam, Name_Postcondition, Name_Precondition) then | |
206 | Add_Pre_Post_Condition; | |
207 | ||
879ac954 AC |
208 | -- The pragma is not a proper contract item |
209 | ||
210 | else | |
211 | raise Program_Error; | |
212 | end if; | |
213 | ||
f99ff327 AC |
214 | -- Packages or instantiations, the applicable pragmas are: |
215 | -- Abstract_States | |
216 | -- Initial_Condition | |
217 | -- Initializes | |
218 | -- Part_Of (instantiation only) | |
219 | ||
220 | elsif Ekind_In (Id, E_Generic_Package, E_Package) then | |
221 | if Nam_In (Prag_Nam, Name_Abstract_State, | |
222 | Name_Initial_Condition, | |
223 | Name_Initializes) | |
224 | then | |
225 | Add_Classification; | |
226 | ||
227 | -- Indicator Part_Of must be associated with a package instantiation | |
228 | ||
229 | elsif Prag_Nam = Name_Part_Of and then Is_Generic_Instance (Id) then | |
230 | Add_Classification; | |
231 | ||
232 | -- The pragma is not a proper contract item | |
233 | ||
234 | else | |
235 | raise Program_Error; | |
236 | end if; | |
237 | ||
238 | -- Package bodies, the applicable pragmas are: | |
239 | -- Refined_States | |
240 | ||
241 | elsif Ekind (Id) = E_Package_Body then | |
242 | if Prag_Nam = Name_Refined_State then | |
243 | Add_Classification; | |
244 | ||
245 | -- The pragma is not a proper contract item | |
246 | ||
247 | else | |
248 | raise Program_Error; | |
249 | end if; | |
250 | ||
75b87c16 AC |
251 | -- Protected units, the applicable pragmas are: |
252 | -- Part_Of | |
253 | ||
254 | elsif Ekind (Id) = E_Protected_Type then | |
255 | if Prag_Nam = Name_Part_Of then | |
256 | Add_Classification; | |
257 | ||
258 | -- The pragma is not a proper contract item | |
259 | ||
260 | else | |
261 | raise Program_Error; | |
262 | end if; | |
263 | ||
f99ff327 | 264 | -- Subprogram bodies, the applicable pragmas are: |
879ac954 AC |
265 | -- Postcondition |
266 | -- Precondition | |
267 | -- Refined_Depends | |
268 | -- Refined_Global | |
269 | -- Refined_Post | |
270 | ||
271 | elsif Ekind (Id) = E_Subprogram_Body then | |
272 | if Nam_In (Prag_Nam, Name_Refined_Depends, Name_Refined_Global) then | |
273 | Add_Classification; | |
274 | ||
275 | elsif Nam_In (Prag_Nam, Name_Postcondition, | |
276 | Name_Precondition, | |
277 | Name_Refined_Post) | |
278 | then | |
279 | Add_Pre_Post_Condition; | |
280 | ||
281 | -- The pragma is not a proper contract item | |
282 | ||
283 | else | |
284 | raise Program_Error; | |
285 | end if; | |
286 | ||
f99ff327 AC |
287 | -- Task bodies, the applicable pragmas are: |
288 | -- Refined_Depends | |
289 | -- Refined_Global | |
290 | ||
291 | elsif Ekind (Id) = E_Task_Body then | |
292 | if Nam_In (Prag_Nam, Name_Refined_Depends, Name_Refined_Global) then | |
293 | Add_Classification; | |
294 | ||
295 | -- The pragma is not a proper contract item | |
296 | ||
297 | else | |
298 | raise Program_Error; | |
299 | end if; | |
300 | ||
301 | -- Task units, the applicable pragmas are: | |
302 | -- Depends | |
303 | -- Global | |
75b87c16 | 304 | -- Part_Of |
f99ff327 AC |
305 | |
306 | elsif Ekind (Id) = E_Task_Type then | |
75b87c16 | 307 | if Nam_In (Prag_Nam, Name_Depends, Name_Global, Name_Part_Of) then |
f99ff327 AC |
308 | Add_Classification; |
309 | ||
310 | -- The pragma is not a proper contract item | |
311 | ||
312 | else | |
313 | raise Program_Error; | |
314 | end if; | |
315 | ||
316 | -- Variables, the applicable pragmas are: | |
879ac954 AC |
317 | -- Async_Readers |
318 | -- Async_Writers | |
319 | -- Constant_After_Elaboration | |
75b87c16 | 320 | -- Depends |
879ac954 AC |
321 | -- Effective_Reads |
322 | -- Effective_Writes | |
75b87c16 | 323 | -- Global |
879ac954 AC |
324 | -- Part_Of |
325 | ||
326 | elsif Ekind (Id) = E_Variable then | |
327 | if Nam_In (Prag_Nam, Name_Async_Readers, | |
328 | Name_Async_Writers, | |
329 | Name_Constant_After_Elaboration, | |
75b87c16 | 330 | Name_Depends, |
879ac954 AC |
331 | Name_Effective_Reads, |
332 | Name_Effective_Writes, | |
75b87c16 | 333 | Name_Global, |
879ac954 AC |
334 | Name_Part_Of) |
335 | then | |
336 | Add_Classification; | |
337 | ||
338 | -- The pragma is not a proper contract item | |
339 | ||
340 | else | |
341 | raise Program_Error; | |
342 | end if; | |
343 | end if; | |
344 | end Add_Contract_Item; | |
345 | ||
e645cb39 AC |
346 | ----------------------- |
347 | -- Analyze_Contracts -- | |
348 | ----------------------- | |
349 | ||
350 | procedure Analyze_Contracts (L : List_Id) is | |
65e5747e PMR |
351 | Decl : Node_Id; |
352 | ||
e645cb39 | 353 | begin |
5f325af2 AC |
354 | if CodePeer_Mode and then Debug_Flag_Dot_KK then |
355 | Build_And_Analyze_Contract_Only_Subprograms (L); | |
356 | end if; | |
357 | ||
e645cb39 AC |
358 | Decl := First (L); |
359 | while Present (Decl) loop | |
879ac954 | 360 | |
e645cb39 AC |
361 | -- Entry or subprogram declarations |
362 | ||
363 | if Nkind_In (Decl, N_Abstract_Subprogram_Declaration, | |
364 | N_Entry_Declaration, | |
365 | N_Generic_Subprogram_Declaration, | |
366 | N_Subprogram_Declaration) | |
367 | then | |
aaa0a838 ES |
368 | declare |
369 | Subp_Id : constant Entity_Id := Defining_Entity (Decl); | |
370 | ||
371 | begin | |
65e5747e | 372 | Analyze_Entry_Or_Subprogram_Contract (Subp_Id); |
aaa0a838 | 373 | |
02848684 | 374 | -- If analysis of a class-wide pre/postcondition indicates |
aaa0a838 | 375 | -- that a class-wide clone is needed, analyze its declaration |
02848684 | 376 | -- now. Its body is created when the body of the original |
aaa0a838 ES |
377 | -- operation is analyzed (and rewritten). |
378 | ||
379 | if Is_Subprogram (Subp_Id) | |
380 | and then Present (Class_Wide_Clone (Subp_Id)) | |
381 | then | |
382 | Analyze (Unit_Declaration_Node (Class_Wide_Clone (Subp_Id))); | |
383 | end if; | |
384 | end; | |
e645cb39 AC |
385 | |
386 | -- Entry or subprogram bodies | |
387 | ||
388 | elsif Nkind_In (Decl, N_Entry_Body, N_Subprogram_Body) then | |
389 | Analyze_Entry_Or_Subprogram_Body_Contract (Defining_Entity (Decl)); | |
390 | ||
391 | -- Objects | |
392 | ||
393 | elsif Nkind (Decl) = N_Object_Declaration then | |
65e5747e | 394 | Analyze_Object_Contract (Defining_Entity (Decl)); |
e645cb39 | 395 | |
96e4fda5 HK |
396 | -- Package instantiation |
397 | ||
398 | elsif Nkind (Decl) = N_Package_Instantiation then | |
399 | Analyze_Package_Instantiation_Contract (Defining_Entity (Decl)); | |
400 | ||
5f325af2 | 401 | -- Protected units |
e645cb39 AC |
402 | |
403 | elsif Nkind_In (Decl, N_Protected_Type_Declaration, | |
404 | N_Single_Protected_Declaration) | |
405 | then | |
406 | Analyze_Protected_Contract (Defining_Entity (Decl)); | |
407 | ||
408 | -- Subprogram body stubs | |
409 | ||
410 | elsif Nkind (Decl) = N_Subprogram_Body_Stub then | |
411 | Analyze_Subprogram_Body_Stub_Contract (Defining_Entity (Decl)); | |
412 | ||
413 | -- Task units | |
414 | ||
415 | elsif Nkind_In (Decl, N_Single_Task_Declaration, | |
416 | N_Task_Type_Declaration) | |
417 | then | |
418 | Analyze_Task_Contract (Defining_Entity (Decl)); | |
05662a06 | 419 | |
812e6118 | 420 | -- For type declarations, we need to do the preanalysis of Iterable |
65e5747e PMR |
421 | -- aspect specifications. |
422 | ||
05662a06 ES |
423 | -- Other type aspects need to be resolved here??? |
424 | ||
425 | elsif Nkind (Decl) = N_Private_Type_Declaration | |
426 | and then Present (Aspect_Specifications (Decl)) | |
427 | then | |
428 | declare | |
429 | E : constant Entity_Id := Defining_Identifier (Decl); | |
430 | It : constant Node_Id := Find_Aspect (E, Aspect_Iterable); | |
65e5747e | 431 | |
05662a06 ES |
432 | begin |
433 | if Present (It) then | |
434 | Validate_Iterable_Aspect (E, It); | |
435 | end if; | |
436 | end; | |
e645cb39 AC |
437 | end if; |
438 | ||
439 | Next (Decl); | |
879ac954 | 440 | end loop; |
e645cb39 | 441 | end Analyze_Contracts; |
879ac954 | 442 | |
f99ff327 AC |
443 | ----------------------------------------------- |
444 | -- Analyze_Entry_Or_Subprogram_Body_Contract -- | |
445 | ----------------------------------------------- | |
446 | ||
f9a8f910 HK |
447 | -- WARNING: This routine manages SPARK regions. Return statements must be |
448 | -- replaced by gotos which jump to the end of the routine and restore the | |
449 | -- SPARK mode. | |
450 | ||
f99ff327 AC |
451 | procedure Analyze_Entry_Or_Subprogram_Body_Contract (Body_Id : Entity_Id) is |
452 | Body_Decl : constant Node_Id := Unit_Declaration_Node (Body_Id); | |
453 | Items : constant Node_Id := Contract (Body_Id); | |
454 | Spec_Id : constant Entity_Id := Unique_Defining_Entity (Body_Decl); | |
f9a8f910 HK |
455 | |
456 | Saved_SM : constant SPARK_Mode_Type := SPARK_Mode; | |
457 | Saved_SMP : constant Node_Id := SPARK_Mode_Pragma; | |
458 | -- Save the SPARK_Mode-related data to restore on exit | |
f99ff327 AC |
459 | |
460 | begin | |
461 | -- When a subprogram body declaration is illegal, its defining entity is | |
462 | -- left unanalyzed. There is nothing left to do in this case because the | |
463 | -- body lacks a contract, or even a proper Ekind. | |
464 | ||
465 | if Ekind (Body_Id) = E_Void then | |
466 | return; | |
467 | ||
f99ff327 AC |
468 | -- Do not analyze a contract multiple times |
469 | ||
470 | elsif Present (Items) then | |
471 | if Analyzed (Items) then | |
472 | return; | |
473 | else | |
474 | Set_Analyzed (Items); | |
475 | end if; | |
476 | end if; | |
477 | ||
478 | -- Due to the timing of contract analysis, delayed pragmas may be | |
479 | -- subject to the wrong SPARK_Mode, usually that of the enclosing | |
480 | -- context. To remedy this, restore the original SPARK_Mode of the | |
481 | -- related subprogram body. | |
482 | ||
f9a8f910 | 483 | Set_SPARK_Mode (Body_Id); |
f99ff327 AC |
484 | |
485 | -- Ensure that the contract cases or postconditions mention 'Result or | |
486 | -- define a post-state. | |
487 | ||
488 | Check_Result_And_Post_State (Body_Id); | |
489 | ||
490 | -- A stand-alone nonvolatile function body cannot have an effectively | |
491 | -- volatile formal parameter or return type (SPARK RM 7.1.3(9)). This | |
492 | -- check is relevant only when SPARK_Mode is on, as it is not a standard | |
493 | -- legality rule. The check is performed here because Volatile_Function | |
332429c8 AC |
494 | -- is processed after the analysis of the related subprogram body. The |
495 | -- check only applies to source subprograms and not to generated TSS | |
496 | -- subprograms. | |
f99ff327 AC |
497 | |
498 | if SPARK_Mode = On | |
499 | and then Ekind_In (Body_Id, E_Function, E_Generic_Function) | |
332429c8 | 500 | and then Comes_From_Source (Spec_Id) |
f99ff327 AC |
501 | and then not Is_Volatile_Function (Body_Id) |
502 | then | |
503 | Check_Nonvolatile_Function_Profile (Body_Id); | |
504 | end if; | |
505 | ||
506 | -- Restore the SPARK_Mode of the enclosing context after all delayed | |
507 | -- pragmas have been analyzed. | |
508 | ||
f9a8f910 | 509 | Restore_SPARK_Mode (Saved_SM, Saved_SMP); |
f99ff327 AC |
510 | |
511 | -- Capture all global references in a generic subprogram body now that | |
512 | -- the contract has been analyzed. | |
513 | ||
514 | if Is_Generic_Declaration_Or_Body (Body_Decl) then | |
515 | Save_Global_References_In_Contract | |
516 | (Templ => Original_Node (Body_Decl), | |
517 | Gen_Id => Spec_Id); | |
518 | end if; | |
519 | ||
520 | -- Deal with preconditions, [refined] postconditions, Contract_Cases, | |
521 | -- invariants and predicates associated with body and its spec. Do not | |
522 | -- expand the contract of subprogram body stubs. | |
523 | ||
524 | if Nkind (Body_Decl) = N_Subprogram_Body then | |
525 | Expand_Subprogram_Contract (Body_Id); | |
526 | end if; | |
527 | end Analyze_Entry_Or_Subprogram_Body_Contract; | |
528 | ||
529 | ------------------------------------------ | |
530 | -- Analyze_Entry_Or_Subprogram_Contract -- | |
531 | ------------------------------------------ | |
532 | ||
f9a8f910 HK |
533 | -- WARNING: This routine manages SPARK regions. Return statements must be |
534 | -- replaced by gotos which jump to the end of the routine and restore the | |
535 | -- SPARK mode. | |
536 | ||
e645cb39 AC |
537 | procedure Analyze_Entry_Or_Subprogram_Contract |
538 | (Subp_Id : Entity_Id; | |
539 | Freeze_Id : Entity_Id := Empty) | |
540 | is | |
f99ff327 AC |
541 | Items : constant Node_Id := Contract (Subp_Id); |
542 | Subp_Decl : constant Node_Id := Unit_Declaration_Node (Subp_Id); | |
8a0183fd | 543 | |
f9a8f910 HK |
544 | Saved_SM : constant SPARK_Mode_Type := SPARK_Mode; |
545 | Saved_SMP : constant Node_Id := SPARK_Mode_Pragma; | |
546 | -- Save the SPARK_Mode-related data to restore on exit | |
547 | ||
8a0183fd HK |
548 | Skip_Assert_Exprs : constant Boolean := |
549 | Ekind_In (Subp_Id, E_Entry, E_Entry_Family) | |
550 | and then not ASIS_Mode | |
551 | and then not GNATprove_Mode; | |
552 | ||
553 | Depends : Node_Id := Empty; | |
554 | Global : Node_Id := Empty; | |
8a0183fd HK |
555 | Prag : Node_Id; |
556 | Prag_Nam : Name_Id; | |
f99ff327 AC |
557 | |
558 | begin | |
f99ff327 AC |
559 | -- Do not analyze a contract multiple times |
560 | ||
e310115e | 561 | if Present (Items) then |
f99ff327 AC |
562 | if Analyzed (Items) then |
563 | return; | |
564 | else | |
565 | Set_Analyzed (Items); | |
566 | end if; | |
567 | end if; | |
568 | ||
569 | -- Due to the timing of contract analysis, delayed pragmas may be | |
570 | -- subject to the wrong SPARK_Mode, usually that of the enclosing | |
571 | -- context. To remedy this, restore the original SPARK_Mode of the | |
572 | -- related subprogram body. | |
573 | ||
f9a8f910 | 574 | Set_SPARK_Mode (Subp_Id); |
f99ff327 AC |
575 | |
576 | -- All subprograms carry a contract, but for some it is not significant | |
577 | -- and should not be processed. | |
578 | ||
579 | if not Has_Significant_Contract (Subp_Id) then | |
580 | null; | |
581 | ||
582 | elsif Present (Items) then | |
583 | ||
e310115e | 584 | -- Do not analyze the pre/postconditions of an entry declaration |
8a0183fd HK |
585 | -- unless annotating the original tree for ASIS or GNATprove. The |
586 | -- real analysis occurs when the pre/postconditons are relocated to | |
587 | -- the contract wrapper procedure (see Build_Contract_Wrapper). | |
f99ff327 | 588 | |
8a0183fd | 589 | if Skip_Assert_Exprs then |
e310115e AC |
590 | null; |
591 | ||
592 | -- Otherwise analyze the pre/postconditions | |
593 | ||
594 | else | |
595 | Prag := Pre_Post_Conditions (Items); | |
596 | while Present (Prag) loop | |
e645cb39 | 597 | Analyze_Pre_Post_Condition_In_Decl_Part (Prag, Freeze_Id); |
e310115e AC |
598 | Prag := Next_Pragma (Prag); |
599 | end loop; | |
600 | end if; | |
f99ff327 AC |
601 | |
602 | -- Analyze contract-cases and test-cases | |
603 | ||
604 | Prag := Contract_Test_Cases (Items); | |
605 | while Present (Prag) loop | |
6e759c2a | 606 | Prag_Nam := Pragma_Name (Prag); |
f99ff327 AC |
607 | |
608 | if Prag_Nam = Name_Contract_Cases then | |
8a0183fd HK |
609 | |
610 | -- Do not analyze the contract cases of an entry declaration | |
611 | -- unless annotating the original tree for ASIS or GNATprove. | |
612 | -- The real analysis occurs when the contract cases are moved | |
613 | -- to the contract wrapper procedure (Build_Contract_Wrapper). | |
614 | ||
615 | if Skip_Assert_Exprs then | |
616 | null; | |
617 | ||
618 | -- Otherwise analyze the contract cases | |
619 | ||
620 | else | |
e645cb39 | 621 | Analyze_Contract_Cases_In_Decl_Part (Prag, Freeze_Id); |
8a0183fd | 622 | end if; |
f99ff327 AC |
623 | else |
624 | pragma Assert (Prag_Nam = Name_Test_Case); | |
625 | Analyze_Test_Case_In_Decl_Part (Prag); | |
626 | end if; | |
627 | ||
628 | Prag := Next_Pragma (Prag); | |
629 | end loop; | |
630 | ||
631 | -- Analyze classification pragmas | |
632 | ||
633 | Prag := Classifications (Items); | |
634 | while Present (Prag) loop | |
6e759c2a | 635 | Prag_Nam := Pragma_Name (Prag); |
f99ff327 AC |
636 | |
637 | if Prag_Nam = Name_Depends then | |
638 | Depends := Prag; | |
639 | ||
640 | elsif Prag_Nam = Name_Global then | |
641 | Global := Prag; | |
642 | end if; | |
643 | ||
644 | Prag := Next_Pragma (Prag); | |
645 | end loop; | |
646 | ||
647 | -- Analyze Global first, as Depends may mention items classified in | |
648 | -- the global categorization. | |
649 | ||
650 | if Present (Global) then | |
651 | Analyze_Global_In_Decl_Part (Global); | |
652 | end if; | |
653 | ||
654 | -- Depends must be analyzed after Global in order to see the modes of | |
655 | -- all global items. | |
656 | ||
657 | if Present (Depends) then | |
658 | Analyze_Depends_In_Decl_Part (Depends); | |
659 | end if; | |
660 | ||
661 | -- Ensure that the contract cases or postconditions mention 'Result | |
662 | -- or define a post-state. | |
663 | ||
664 | Check_Result_And_Post_State (Subp_Id); | |
665 | end if; | |
666 | ||
667 | -- A nonvolatile function cannot have an effectively volatile formal | |
668 | -- parameter or return type (SPARK RM 7.1.3(9)). This check is relevant | |
669 | -- only when SPARK_Mode is on, as it is not a standard legality rule. | |
670 | -- The check is performed here because pragma Volatile_Function is | |
671 | -- processed after the analysis of the related subprogram declaration. | |
672 | ||
673 | if SPARK_Mode = On | |
674 | and then Ekind_In (Subp_Id, E_Function, E_Generic_Function) | |
884f97cc | 675 | and then Comes_From_Source (Subp_Id) |
f99ff327 AC |
676 | and then not Is_Volatile_Function (Subp_Id) |
677 | then | |
678 | Check_Nonvolatile_Function_Profile (Subp_Id); | |
679 | end if; | |
680 | ||
681 | -- Restore the SPARK_Mode of the enclosing context after all delayed | |
682 | -- pragmas have been analyzed. | |
683 | ||
f9a8f910 | 684 | Restore_SPARK_Mode (Saved_SM, Saved_SMP); |
f99ff327 AC |
685 | |
686 | -- Capture all global references in a generic subprogram now that the | |
687 | -- contract has been analyzed. | |
688 | ||
689 | if Is_Generic_Declaration_Or_Body (Subp_Decl) then | |
690 | Save_Global_References_In_Contract | |
691 | (Templ => Original_Node (Subp_Decl), | |
692 | Gen_Id => Subp_Id); | |
693 | end if; | |
694 | end Analyze_Entry_Or_Subprogram_Contract; | |
695 | ||
879ac954 AC |
696 | ----------------------------- |
697 | -- Analyze_Object_Contract -- | |
698 | ----------------------------- | |
699 | ||
f9a8f910 HK |
700 | -- WARNING: This routine manages SPARK regions. Return statements must be |
701 | -- replaced by gotos which jump to the end of the routine and restore the | |
702 | -- SPARK mode. | |
703 | ||
e645cb39 AC |
704 | procedure Analyze_Object_Contract |
705 | (Obj_Id : Entity_Id; | |
706 | Freeze_Id : Entity_Id := Empty) | |
707 | is | |
f9a8f910 HK |
708 | Obj_Typ : constant Entity_Id := Etype (Obj_Id); |
709 | ||
710 | Saved_SM : constant SPARK_Mode_Type := SPARK_Mode; | |
711 | Saved_SMP : constant Node_Id := SPARK_Mode_Pragma; | |
712 | -- Save the SPARK_Mode-related data to restore on exit | |
713 | ||
714 | AR_Val : Boolean := False; | |
715 | AW_Val : Boolean := False; | |
716 | ER_Val : Boolean := False; | |
717 | EW_Val : Boolean := False; | |
718 | Items : Node_Id; | |
719 | Prag : Node_Id; | |
720 | Ref_Elmt : Elmt_Id; | |
721 | Seen : Boolean := False; | |
879ac954 AC |
722 | |
723 | begin | |
724 | -- The loop parameter in an element iterator over a formal container | |
e96b7045 | 725 | -- is declared with an object declaration, but no contracts apply. |
879ac954 AC |
726 | |
727 | if Ekind (Obj_Id) = E_Loop_Parameter then | |
728 | return; | |
729 | end if; | |
730 | ||
e96b7045 | 731 | -- Do not analyze a contract multiple times |
879ac954 AC |
732 | |
733 | Items := Contract (Obj_Id); | |
734 | ||
735 | if Present (Items) then | |
736 | if Analyzed (Items) then | |
737 | return; | |
738 | else | |
739 | Set_Analyzed (Items); | |
740 | end if; | |
741 | end if; | |
742 | ||
58996b09 HK |
743 | -- The anonymous object created for a single concurrent type inherits |
744 | -- the SPARK_Mode from the type. Due to the timing of contract analysis, | |
745 | -- delayed pragmas may be subject to the wrong SPARK_Mode, usually that | |
746 | -- of the enclosing context. To remedy this, restore the original mode | |
747 | -- of the related anonymous object. | |
748 | ||
749 | if Is_Single_Concurrent_Object (Obj_Id) | |
750 | and then Present (SPARK_Pragma (Obj_Id)) | |
751 | then | |
f9a8f910 | 752 | Set_SPARK_Mode (Obj_Id); |
58996b09 HK |
753 | end if; |
754 | ||
e96b7045 | 755 | -- Constant-related checks |
879ac954 AC |
756 | |
757 | if Ekind (Obj_Id) = E_Constant then | |
758 | ||
58996b09 HK |
759 | -- Analyze indicator Part_Of |
760 | ||
761 | Prag := Get_Pragma (Obj_Id, Pragma_Part_Of); | |
762 | ||
763 | -- Check whether the lack of indicator Part_Of agrees with the | |
764 | -- placement of the constant with respect to the state space. | |
765 | ||
766 | if No (Prag) then | |
767 | Check_Missing_Part_Of (Obj_Id); | |
768 | end if; | |
769 | ||
879ac954 | 770 | -- A constant cannot be effectively volatile (SPARK RM 7.1.3(4)). |
e96b7045 AC |
771 | -- This check is relevant only when SPARK_Mode is on, as it is not |
772 | -- a standard Ada legality rule. Internally-generated constants that | |
879ac954 AC |
773 | -- map generic formals to actuals in instantiations are allowed to |
774 | -- be volatile. | |
775 | ||
776 | if SPARK_Mode = On | |
777 | and then Comes_From_Source (Obj_Id) | |
778 | and then Is_Effectively_Volatile (Obj_Id) | |
779 | and then No (Corresponding_Generic_Association (Parent (Obj_Id))) | |
780 | then | |
781 | Error_Msg_N ("constant cannot be volatile", Obj_Id); | |
782 | end if; | |
783 | ||
e96b7045 | 784 | -- Variable-related checks |
879ac954 AC |
785 | |
786 | else pragma Assert (Ekind (Obj_Id) = E_Variable); | |
787 | ||
75b87c16 AC |
788 | -- Analyze all external properties |
789 | ||
790 | Prag := Get_Pragma (Obj_Id, Pragma_Async_Readers); | |
791 | ||
792 | if Present (Prag) then | |
793 | Analyze_External_Property_In_Decl_Part (Prag, AR_Val); | |
794 | Seen := True; | |
795 | end if; | |
796 | ||
797 | Prag := Get_Pragma (Obj_Id, Pragma_Async_Writers); | |
798 | ||
799 | if Present (Prag) then | |
800 | Analyze_External_Property_In_Decl_Part (Prag, AW_Val); | |
801 | Seen := True; | |
802 | end if; | |
803 | ||
804 | Prag := Get_Pragma (Obj_Id, Pragma_Effective_Reads); | |
805 | ||
806 | if Present (Prag) then | |
807 | Analyze_External_Property_In_Decl_Part (Prag, ER_Val); | |
808 | Seen := True; | |
809 | end if; | |
810 | ||
811 | Prag := Get_Pragma (Obj_Id, Pragma_Effective_Writes); | |
812 | ||
813 | if Present (Prag) then | |
814 | Analyze_External_Property_In_Decl_Part (Prag, EW_Val); | |
815 | Seen := True; | |
816 | end if; | |
817 | ||
818 | -- Verify the mutual interaction of the various external properties | |
819 | ||
820 | if Seen then | |
821 | Check_External_Properties (Obj_Id, AR_Val, AW_Val, ER_Val, EW_Val); | |
822 | end if; | |
823 | ||
824 | -- The anonymous object created for a single concurrent type carries | |
825 | -- pragmas Depends and Globat of the type. | |
826 | ||
827 | if Is_Single_Concurrent_Object (Obj_Id) then | |
828 | ||
829 | -- Analyze Global first, as Depends may mention items classified | |
830 | -- in the global categorization. | |
831 | ||
832 | Prag := Get_Pragma (Obj_Id, Pragma_Global); | |
833 | ||
834 | if Present (Prag) then | |
835 | Analyze_Global_In_Decl_Part (Prag); | |
836 | end if; | |
837 | ||
838 | -- Depends must be analyzed after Global in order to see the modes | |
839 | -- of all global items. | |
840 | ||
841 | Prag := Get_Pragma (Obj_Id, Pragma_Depends); | |
842 | ||
843 | if Present (Prag) then | |
844 | Analyze_Depends_In_Decl_Part (Prag); | |
845 | end if; | |
846 | end if; | |
847 | ||
848 | Prag := Get_Pragma (Obj_Id, Pragma_Part_Of); | |
849 | ||
850 | -- Analyze indicator Part_Of | |
851 | ||
852 | if Present (Prag) then | |
e645cb39 | 853 | Analyze_Part_Of_In_Decl_Part (Prag, Freeze_Id); |
75b87c16 | 854 | |
fdc54be6 AC |
855 | -- The variable is a constituent of a single protected/task type |
856 | -- and behaves as a component of the type. Verify that references | |
857 | -- to the variable occur within the definition or body of the type | |
858 | -- (SPARK RM 9.3). | |
859 | ||
860 | if Present (Encapsulating_State (Obj_Id)) | |
861 | and then Is_Single_Concurrent_Object | |
862 | (Encapsulating_State (Obj_Id)) | |
863 | and then Present (Part_Of_References (Obj_Id)) | |
864 | then | |
865 | Ref_Elmt := First_Elmt (Part_Of_References (Obj_Id)); | |
866 | while Present (Ref_Elmt) loop | |
867 | Check_Part_Of_Reference (Obj_Id, Node (Ref_Elmt)); | |
868 | Next_Elmt (Ref_Elmt); | |
869 | end loop; | |
870 | end if; | |
871 | ||
75b87c16 AC |
872 | -- Otherwise check whether the lack of indicator Part_Of agrees with |
873 | -- the placement of the variable with respect to the state space. | |
874 | ||
875 | else | |
876 | Check_Missing_Part_Of (Obj_Id); | |
877 | end if; | |
878 | ||
e96b7045 | 879 | -- The following checks are relevant only when SPARK_Mode is on, as |
879ac954 AC |
880 | -- they are not standard Ada legality rules. Internally generated |
881 | -- temporaries are ignored. | |
882 | ||
883 | if SPARK_Mode = On and then Comes_From_Source (Obj_Id) then | |
884 | if Is_Effectively_Volatile (Obj_Id) then | |
885 | ||
886 | -- The declaration of an effectively volatile object must | |
887 | -- appear at the library level (SPARK RM 7.1.3(3), C.6(6)). | |
888 | ||
889 | if not Is_Library_Level_Entity (Obj_Id) then | |
890 | Error_Msg_N | |
891 | ("volatile variable & must be declared at library level", | |
892 | Obj_Id); | |
893 | ||
894 | -- An object of a discriminated type cannot be effectively | |
895 | -- volatile except for protected objects (SPARK RM 7.1.3(5)). | |
896 | ||
897 | elsif Has_Discriminants (Obj_Typ) | |
898 | and then not Is_Protected_Type (Obj_Typ) | |
899 | then | |
900 | Error_Msg_N | |
901 | ("discriminated object & cannot be volatile", Obj_Id); | |
879ac954 AC |
902 | end if; |
903 | ||
904 | -- The object is not effectively volatile | |
905 | ||
906 | else | |
907 | -- A non-effectively volatile object cannot have effectively | |
908 | -- volatile components (SPARK RM 7.1.3(6)). | |
909 | ||
910 | if not Is_Effectively_Volatile (Obj_Id) | |
911 | and then Has_Volatile_Component (Obj_Typ) | |
912 | then | |
913 | Error_Msg_N | |
914 | ("non-volatile object & cannot have volatile components", | |
915 | Obj_Id); | |
916 | end if; | |
917 | end if; | |
918 | end if; | |
58996b09 | 919 | end if; |
879ac954 | 920 | |
58996b09 | 921 | -- Common checks |
879ac954 | 922 | |
58996b09 | 923 | if Comes_From_Source (Obj_Id) and then Is_Ghost_Entity (Obj_Id) then |
879ac954 | 924 | |
58996b09 HK |
925 | -- A Ghost object cannot be of a type that yields a synchronized |
926 | -- object (SPARK RM 6.9(19)). | |
879ac954 | 927 | |
58996b09 HK |
928 | if Yields_Synchronized_Object (Obj_Typ) then |
929 | Error_Msg_N ("ghost object & cannot be synchronized", Obj_Id); | |
879ac954 | 930 | |
4179af27 | 931 | -- A Ghost object cannot be effectively volatile (SPARK RM 6.9(7) and |
58996b09 | 932 | -- SPARK RM 6.9(19)). |
879ac954 | 933 | |
58996b09 HK |
934 | elsif Is_Effectively_Volatile (Obj_Id) then |
935 | Error_Msg_N ("ghost object & cannot be volatile", Obj_Id); | |
879ac954 | 936 | |
4179af27 | 937 | -- A Ghost object cannot be imported or exported (SPARK RM 6.9(7)). |
58996b09 HK |
938 | -- One exception to this is the object that represents the dispatch |
939 | -- table of a Ghost tagged type, as the symbol needs to be exported. | |
879ac954 | 940 | |
58996b09 | 941 | elsif Is_Exported (Obj_Id) then |
879ac954 AC |
942 | Error_Msg_N ("ghost object & cannot be exported", Obj_Id); |
943 | ||
944 | elsif Is_Imported (Obj_Id) then | |
945 | Error_Msg_N ("ghost object & cannot be imported", Obj_Id); | |
946 | end if; | |
947 | end if; | |
58996b09 HK |
948 | |
949 | -- Restore the SPARK_Mode of the enclosing context after all delayed | |
950 | -- pragmas have been analyzed. | |
951 | ||
f9a8f910 | 952 | Restore_SPARK_Mode (Saved_SM, Saved_SMP); |
879ac954 AC |
953 | end Analyze_Object_Contract; |
954 | ||
955 | ----------------------------------- | |
956 | -- Analyze_Package_Body_Contract -- | |
957 | ----------------------------------- | |
958 | ||
f9a8f910 HK |
959 | -- WARNING: This routine manages SPARK regions. Return statements must be |
960 | -- replaced by gotos which jump to the end of the routine and restore the | |
961 | -- SPARK mode. | |
962 | ||
879ac954 AC |
963 | procedure Analyze_Package_Body_Contract |
964 | (Body_Id : Entity_Id; | |
965 | Freeze_Id : Entity_Id := Empty) | |
966 | is | |
967 | Body_Decl : constant Node_Id := Unit_Declaration_Node (Body_Id); | |
968 | Items : constant Node_Id := Contract (Body_Id); | |
969 | Spec_Id : constant Entity_Id := Spec_Entity (Body_Id); | |
f9a8f910 HK |
970 | |
971 | Saved_SM : constant SPARK_Mode_Type := SPARK_Mode; | |
972 | Saved_SMP : constant Node_Id := SPARK_Mode_Pragma; | |
973 | -- Save the SPARK_Mode-related data to restore on exit | |
974 | ||
879ac954 AC |
975 | Ref_State : Node_Id; |
976 | ||
977 | begin | |
e96b7045 | 978 | -- Do not analyze a contract multiple times |
879ac954 AC |
979 | |
980 | if Present (Items) then | |
981 | if Analyzed (Items) then | |
982 | return; | |
983 | else | |
984 | Set_Analyzed (Items); | |
985 | end if; | |
986 | end if; | |
987 | ||
988 | -- Due to the timing of contract analysis, delayed pragmas may be | |
989 | -- subject to the wrong SPARK_Mode, usually that of the enclosing | |
990 | -- context. To remedy this, restore the original SPARK_Mode of the | |
991 | -- related package body. | |
992 | ||
f9a8f910 | 993 | Set_SPARK_Mode (Body_Id); |
879ac954 AC |
994 | |
995 | Ref_State := Get_Pragma (Body_Id, Pragma_Refined_State); | |
996 | ||
997 | -- The analysis of pragma Refined_State detects whether the spec has | |
998 | -- abstract states available for refinement. | |
999 | ||
1000 | if Present (Ref_State) then | |
1001 | Analyze_Refined_State_In_Decl_Part (Ref_State, Freeze_Id); | |
879ac954 AC |
1002 | end if; |
1003 | ||
1004 | -- Restore the SPARK_Mode of the enclosing context after all delayed | |
1005 | -- pragmas have been analyzed. | |
1006 | ||
f9a8f910 | 1007 | Restore_SPARK_Mode (Saved_SM, Saved_SMP); |
879ac954 AC |
1008 | |
1009 | -- Capture all global references in a generic package body now that the | |
1010 | -- contract has been analyzed. | |
1011 | ||
1012 | if Is_Generic_Declaration_Or_Body (Body_Decl) then | |
1013 | Save_Global_References_In_Contract | |
1014 | (Templ => Original_Node (Body_Decl), | |
1015 | Gen_Id => Spec_Id); | |
1016 | end if; | |
1017 | end Analyze_Package_Body_Contract; | |
1018 | ||
1019 | ------------------------------ | |
1020 | -- Analyze_Package_Contract -- | |
1021 | ------------------------------ | |
1022 | ||
f9a8f910 HK |
1023 | -- WARNING: This routine manages SPARK regions. Return statements must be |
1024 | -- replaced by gotos which jump to the end of the routine and restore the | |
1025 | -- SPARK mode. | |
1026 | ||
879ac954 AC |
1027 | procedure Analyze_Package_Contract (Pack_Id : Entity_Id) is |
1028 | Items : constant Node_Id := Contract (Pack_Id); | |
1029 | Pack_Decl : constant Node_Id := Unit_Declaration_Node (Pack_Id); | |
f9a8f910 HK |
1030 | |
1031 | Saved_SM : constant SPARK_Mode_Type := SPARK_Mode; | |
1032 | Saved_SMP : constant Node_Id := SPARK_Mode_Pragma; | |
1033 | -- Save the SPARK_Mode-related data to restore on exit | |
1034 | ||
879ac954 AC |
1035 | Init : Node_Id := Empty; |
1036 | Init_Cond : Node_Id := Empty; | |
879ac954 AC |
1037 | Prag : Node_Id; |
1038 | Prag_Nam : Name_Id; | |
1039 | ||
1040 | begin | |
e96b7045 | 1041 | -- Do not analyze a contract multiple times |
879ac954 AC |
1042 | |
1043 | if Present (Items) then | |
1044 | if Analyzed (Items) then | |
1045 | return; | |
1046 | else | |
1047 | Set_Analyzed (Items); | |
1048 | end if; | |
1049 | end if; | |
1050 | ||
1051 | -- Due to the timing of contract analysis, delayed pragmas may be | |
1052 | -- subject to the wrong SPARK_Mode, usually that of the enclosing | |
1053 | -- context. To remedy this, restore the original SPARK_Mode of the | |
1054 | -- related package. | |
1055 | ||
f9a8f910 | 1056 | Set_SPARK_Mode (Pack_Id); |
879ac954 AC |
1057 | |
1058 | if Present (Items) then | |
1059 | ||
e96b7045 | 1060 | -- Locate and store pragmas Initial_Condition and Initializes, since |
879ac954 AC |
1061 | -- their order of analysis matters. |
1062 | ||
1063 | Prag := Classifications (Items); | |
1064 | while Present (Prag) loop | |
6e759c2a | 1065 | Prag_Nam := Pragma_Name (Prag); |
879ac954 AC |
1066 | |
1067 | if Prag_Nam = Name_Initial_Condition then | |
1068 | Init_Cond := Prag; | |
1069 | ||
1070 | elsif Prag_Nam = Name_Initializes then | |
1071 | Init := Prag; | |
1072 | end if; | |
1073 | ||
1074 | Prag := Next_Pragma (Prag); | |
1075 | end loop; | |
1076 | ||
e96b7045 | 1077 | -- Analyze the initialization-related pragmas. Initializes must come |
879ac954 AC |
1078 | -- before Initial_Condition due to item dependencies. |
1079 | ||
1080 | if Present (Init) then | |
1081 | Analyze_Initializes_In_Decl_Part (Init); | |
1082 | end if; | |
1083 | ||
1084 | if Present (Init_Cond) then | |
1085 | Analyze_Initial_Condition_In_Decl_Part (Init_Cond); | |
1086 | end if; | |
1087 | end if; | |
1088 | ||
879ac954 AC |
1089 | -- Restore the SPARK_Mode of the enclosing context after all delayed |
1090 | -- pragmas have been analyzed. | |
1091 | ||
f9a8f910 | 1092 | Restore_SPARK_Mode (Saved_SM, Saved_SMP); |
879ac954 AC |
1093 | |
1094 | -- Capture all global references in a generic package now that the | |
1095 | -- contract has been analyzed. | |
1096 | ||
1097 | if Is_Generic_Declaration_Or_Body (Pack_Decl) then | |
1098 | Save_Global_References_In_Contract | |
1099 | (Templ => Original_Node (Pack_Decl), | |
1100 | Gen_Id => Pack_Id); | |
1101 | end if; | |
1102 | end Analyze_Package_Contract; | |
96e4fda5 HK |
1103 | |
1104 | -------------------------------------------- | |
1105 | -- Analyze_Package_Instantiation_Contract -- | |
1106 | -------------------------------------------- | |
1107 | ||
1108 | -- WARNING: This routine manages SPARK regions. Return statements must be | |
1109 | -- replaced by gotos which jump to the end of the routine and restore the | |
1110 | -- SPARK mode. | |
1111 | ||
1112 | procedure Analyze_Package_Instantiation_Contract (Inst_Id : Entity_Id) is | |
1113 | Inst_Spec : constant Node_Id := | |
1114 | Instance_Spec (Unit_Declaration_Node (Inst_Id)); | |
1115 | ||
1116 | Saved_SM : constant SPARK_Mode_Type := SPARK_Mode; | |
1117 | Saved_SMP : constant Node_Id := SPARK_Mode_Pragma; | |
1118 | -- Save the SPARK_Mode-related data to restore on exit | |
1119 | ||
1120 | Pack_Id : Entity_Id; | |
1121 | Prag : Node_Id; | |
1122 | ||
1123 | begin | |
1124 | -- Nothing to do when the package instantiation is erroneous or left | |
1125 | -- partially decorated. | |
1126 | ||
1127 | if No (Inst_Spec) then | |
1128 | return; | |
1129 | end if; | |
1130 | ||
1131 | Pack_Id := Defining_Entity (Inst_Spec); | |
1132 | Prag := Get_Pragma (Pack_Id, Pragma_Part_Of); | |
1133 | ||
1134 | -- Due to the timing of contract analysis, delayed pragmas may be | |
1135 | -- subject to the wrong SPARK_Mode, usually that of the enclosing | |
1136 | -- context. To remedy this, restore the original SPARK_Mode of the | |
1137 | -- related package. | |
1138 | ||
1139 | Set_SPARK_Mode (Pack_Id); | |
1140 | ||
1141 | -- Check whether the lack of indicator Part_Of agrees with the placement | |
1142 | -- of the package instantiation with respect to the state space. Nested | |
1143 | -- package instantiations do not need to be checked because they inherit | |
1144 | -- Part_Of indicator of the outermost package instantiation (see routine | |
1145 | -- Propagate_Part_Of in Sem_Prag). | |
1146 | ||
1147 | if In_Instance then | |
1148 | null; | |
1149 | ||
1150 | elsif No (Prag) then | |
1151 | Check_Missing_Part_Of (Pack_Id); | |
1152 | end if; | |
1153 | ||
1154 | -- Restore the SPARK_Mode of the enclosing context after all delayed | |
1155 | -- pragmas have been analyzed. | |
1156 | ||
1157 | Restore_SPARK_Mode (Saved_SM, Saved_SMP); | |
1158 | end Analyze_Package_Instantiation_Contract; | |
879ac954 | 1159 | |
75b87c16 AC |
1160 | -------------------------------- |
1161 | -- Analyze_Protected_Contract -- | |
1162 | -------------------------------- | |
1163 | ||
1164 | procedure Analyze_Protected_Contract (Prot_Id : Entity_Id) is | |
1165 | Items : constant Node_Id := Contract (Prot_Id); | |
75b87c16 AC |
1166 | |
1167 | begin | |
1168 | -- Do not analyze a contract multiple times | |
1169 | ||
1170 | if Present (Items) then | |
1171 | if Analyzed (Items) then | |
1172 | return; | |
1173 | else | |
1174 | Set_Analyzed (Items); | |
1175 | end if; | |
1176 | end if; | |
75b87c16 AC |
1177 | end Analyze_Protected_Contract; |
1178 | ||
f99ff327 AC |
1179 | ------------------------------------------- |
1180 | -- Analyze_Subprogram_Body_Stub_Contract -- | |
1181 | ------------------------------------------- | |
879ac954 | 1182 | |
f99ff327 AC |
1183 | procedure Analyze_Subprogram_Body_Stub_Contract (Stub_Id : Entity_Id) is |
1184 | Stub_Decl : constant Node_Id := Parent (Parent (Stub_Id)); | |
1185 | Spec_Id : constant Entity_Id := Corresponding_Spec_Of_Stub (Stub_Decl); | |
879ac954 AC |
1186 | |
1187 | begin | |
f99ff327 AC |
1188 | -- A subprogram body stub may act as its own spec or as the completion |
1189 | -- of a previous declaration. Depending on the context, the contract of | |
1190 | -- the stub may contain two sets of pragmas. | |
879ac954 | 1191 | |
f99ff327 AC |
1192 | -- The stub is a completion, the applicable pragmas are: |
1193 | -- Refined_Depends | |
1194 | -- Refined_Global | |
879ac954 | 1195 | |
f99ff327 AC |
1196 | if Present (Spec_Id) then |
1197 | Analyze_Entry_Or_Subprogram_Body_Contract (Stub_Id); | |
879ac954 | 1198 | |
f99ff327 AC |
1199 | -- The stub acts as its own spec, the applicable pragmas are: |
1200 | -- Contract_Cases | |
1201 | -- Depends | |
1202 | -- Global | |
1203 | -- Postcondition | |
1204 | -- Precondition | |
1205 | -- Test_Case | |
879ac954 | 1206 | |
f99ff327 AC |
1207 | else |
1208 | Analyze_Entry_Or_Subprogram_Contract (Stub_Id); | |
879ac954 | 1209 | end if; |
f99ff327 | 1210 | end Analyze_Subprogram_Body_Stub_Contract; |
879ac954 | 1211 | |
f99ff327 AC |
1212 | --------------------------- |
1213 | -- Analyze_Task_Contract -- | |
1214 | --------------------------- | |
879ac954 | 1215 | |
f9a8f910 HK |
1216 | -- WARNING: This routine manages SPARK regions. Return statements must be |
1217 | -- replaced by gotos which jump to the end of the routine and restore the | |
1218 | -- SPARK mode. | |
1219 | ||
f99ff327 AC |
1220 | procedure Analyze_Task_Contract (Task_Id : Entity_Id) is |
1221 | Items : constant Node_Id := Contract (Task_Id); | |
f9a8f910 HK |
1222 | |
1223 | Saved_SM : constant SPARK_Mode_Type := SPARK_Mode; | |
1224 | Saved_SMP : constant Node_Id := SPARK_Mode_Pragma; | |
1225 | -- Save the SPARK_Mode-related data to restore on exit | |
1226 | ||
1227 | Prag : Node_Id; | |
879ac954 AC |
1228 | |
1229 | begin | |
e96b7045 | 1230 | -- Do not analyze a contract multiple times |
879ac954 AC |
1231 | |
1232 | if Present (Items) then | |
1233 | if Analyzed (Items) then | |
1234 | return; | |
1235 | else | |
1236 | Set_Analyzed (Items); | |
1237 | end if; | |
1238 | end if; | |
1239 | ||
1240 | -- Due to the timing of contract analysis, delayed pragmas may be | |
1241 | -- subject to the wrong SPARK_Mode, usually that of the enclosing | |
1242 | -- context. To remedy this, restore the original SPARK_Mode of the | |
75b87c16 | 1243 | -- related task unit. |
879ac954 | 1244 | |
f9a8f910 | 1245 | Set_SPARK_Mode (Task_Id); |
879ac954 | 1246 | |
f99ff327 AC |
1247 | -- Analyze Global first, as Depends may mention items classified in the |
1248 | -- global categorization. | |
879ac954 | 1249 | |
f99ff327 | 1250 | Prag := Get_Pragma (Task_Id, Pragma_Global); |
879ac954 | 1251 | |
f99ff327 AC |
1252 | if Present (Prag) then |
1253 | Analyze_Global_In_Decl_Part (Prag); | |
879ac954 AC |
1254 | end if; |
1255 | ||
f99ff327 AC |
1256 | -- Depends must be analyzed after Global in order to see the modes of |
1257 | -- all global items. | |
879ac954 | 1258 | |
f99ff327 AC |
1259 | Prag := Get_Pragma (Task_Id, Pragma_Depends); |
1260 | ||
1261 | if Present (Prag) then | |
1262 | Analyze_Depends_In_Decl_Part (Prag); | |
879ac954 AC |
1263 | end if; |
1264 | ||
1265 | -- Restore the SPARK_Mode of the enclosing context after all delayed | |
1266 | -- pragmas have been analyzed. | |
1267 | ||
f9a8f910 | 1268 | Restore_SPARK_Mode (Saved_SM, Saved_SMP); |
f99ff327 | 1269 | end Analyze_Task_Contract; |
879ac954 | 1270 | |
82e5c243 AC |
1271 | ------------------------------------------------- |
1272 | -- Build_And_Analyze_Contract_Only_Subprograms -- | |
1273 | ------------------------------------------------- | |
879ac954 | 1274 | |
82e5c243 AC |
1275 | procedure Build_And_Analyze_Contract_Only_Subprograms (L : List_Id) is |
1276 | procedure Analyze_Contract_Only_Subprograms; | |
1277 | -- Analyze the contract-only subprograms of L | |
879ac954 | 1278 | |
82e5c243 AC |
1279 | procedure Append_Contract_Only_Subprograms (Subp_List : List_Id); |
1280 | -- Append the contract-only bodies of Subp_List to its declarations list | |
879ac954 | 1281 | |
82e5c243 AC |
1282 | function Build_Contract_Only_Subprogram (E : Entity_Id) return Node_Id; |
1283 | -- If E is an entity for a non-imported subprogram specification with | |
1284 | -- pre/postconditions and we are compiling with CodePeer mode, then | |
1285 | -- this procedure will create a wrapper to help Gnat2scil process its | |
1286 | -- contracts. Return Empty if the wrapper cannot be built. | |
879ac954 | 1287 | |
82e5c243 AC |
1288 | function Build_Contract_Only_Subprograms (L : List_Id) return List_Id; |
1289 | -- Build the contract-only subprograms of all eligible subprograms found | |
1290 | -- in list L. | |
879ac954 | 1291 | |
82e5c243 AC |
1292 | function Has_Private_Declarations (N : Node_Id) return Boolean; |
1293 | -- Return True for package specs, task definitions, and protected type | |
1294 | -- definitions whose list of private declarations is not empty. | |
879ac954 | 1295 | |
82e5c243 AC |
1296 | --------------------------------------- |
1297 | -- Analyze_Contract_Only_Subprograms -- | |
1298 | --------------------------------------- | |
879ac954 | 1299 | |
82e5c243 AC |
1300 | procedure Analyze_Contract_Only_Subprograms is |
1301 | procedure Analyze_Contract_Only_Bodies; | |
1302 | -- Analyze all the contract-only bodies of L | |
879ac954 | 1303 | |
82e5c243 AC |
1304 | ---------------------------------- |
1305 | -- Analyze_Contract_Only_Bodies -- | |
1306 | ---------------------------------- | |
879ac954 | 1307 | |
82e5c243 AC |
1308 | procedure Analyze_Contract_Only_Bodies is |
1309 | Decl : Node_Id; | |
879ac954 | 1310 | |
82e5c243 AC |
1311 | begin |
1312 | Decl := First (L); | |
1313 | while Present (Decl) loop | |
1314 | if Nkind (Decl) = N_Subprogram_Body | |
1315 | and then Is_Contract_Only_Body | |
1316 | (Defining_Unit_Name (Specification (Decl))) | |
1317 | then | |
1318 | Analyze (Decl); | |
1319 | end if; | |
879ac954 | 1320 | |
82e5c243 AC |
1321 | Next (Decl); |
1322 | end loop; | |
1323 | end Analyze_Contract_Only_Bodies; | |
879ac954 | 1324 | |
82e5c243 AC |
1325 | -- Start of processing for Analyze_Contract_Only_Subprograms |
1326 | ||
1327 | begin | |
1328 | if Ekind (Current_Scope) /= E_Package then | |
1329 | Analyze_Contract_Only_Bodies; | |
879ac954 AC |
1330 | |
1331 | else | |
82e5c243 AC |
1332 | declare |
1333 | Pkg_Spec : constant Node_Id := | |
1334 | Package_Specification (Current_Scope); | |
879ac954 | 1335 | |
82e5c243 AC |
1336 | begin |
1337 | if not Has_Private_Declarations (Pkg_Spec) then | |
1338 | Analyze_Contract_Only_Bodies; | |
879ac954 | 1339 | |
82e5c243 AC |
1340 | -- For packages with private declarations, the contract-only |
1341 | -- bodies of subprograms defined in the visible part of the | |
1342 | -- package are added to its private declarations (to ensure | |
1343 | -- that they do not cause premature freezing of types and also | |
1344 | -- that they are analyzed with proper visibility). Hence they | |
1345 | -- will be analyzed later. | |
879ac954 | 1346 | |
82e5c243 AC |
1347 | elsif Visible_Declarations (Pkg_Spec) = L then |
1348 | null; | |
879ac954 | 1349 | |
82e5c243 AC |
1350 | elsif Private_Declarations (Pkg_Spec) = L then |
1351 | Analyze_Contract_Only_Bodies; | |
1352 | end if; | |
1353 | end; | |
1354 | end if; | |
1355 | end Analyze_Contract_Only_Subprograms; | |
879ac954 | 1356 | |
82e5c243 AC |
1357 | -------------------------------------- |
1358 | -- Append_Contract_Only_Subprograms -- | |
1359 | -------------------------------------- | |
879ac954 | 1360 | |
82e5c243 AC |
1361 | procedure Append_Contract_Only_Subprograms (Subp_List : List_Id) is |
1362 | begin | |
1363 | if No (Subp_List) then | |
1364 | return; | |
879ac954 AC |
1365 | end if; |
1366 | ||
82e5c243 AC |
1367 | if Ekind (Current_Scope) /= E_Package then |
1368 | Append_List (Subp_List, To => L); | |
879ac954 | 1369 | |
82e5c243 AC |
1370 | else |
1371 | declare | |
1372 | Pkg_Spec : constant Node_Id := | |
1373 | Package_Specification (Current_Scope); | |
879ac954 | 1374 | |
82e5c243 AC |
1375 | begin |
1376 | if not Has_Private_Declarations (Pkg_Spec) then | |
1377 | Append_List (Subp_List, To => L); | |
879ac954 | 1378 | |
82e5c243 AC |
1379 | -- If the package has private declarations then append them to |
1380 | -- its private declarations; they will be analyzed when the | |
1381 | -- contracts of its private declarations are analyzed. | |
879ac954 | 1382 | |
82e5c243 AC |
1383 | else |
1384 | Append_List | |
1385 | (List => Subp_List, | |
1386 | To => Private_Declarations (Pkg_Spec)); | |
1387 | end if; | |
1388 | end; | |
879ac954 | 1389 | end if; |
82e5c243 | 1390 | end Append_Contract_Only_Subprograms; |
879ac954 | 1391 | |
82e5c243 AC |
1392 | ------------------------------------ |
1393 | -- Build_Contract_Only_Subprogram -- | |
1394 | ------------------------------------ | |
879ac954 | 1395 | |
82e5c243 AC |
1396 | -- This procedure takes care of building a wrapper to generate better |
1397 | -- analysis results in the case of a call to a subprogram whose body | |
1398 | -- is unavailable to CodePeer but whose specification includes Pre/Post | |
1399 | -- conditions. The body might be unavailable for any of a number or | |
1400 | -- reasons (it is imported, the .adb file is simply missing, or the | |
1401 | -- subprogram might be subject to an Annotate (CodePeer, Skip_Analysis) | |
1402 | -- pragma). The built subprogram has the following contents: | |
1403 | -- * check preconditions | |
1404 | -- * call the subprogram | |
1405 | -- * check postconditions | |
879ac954 | 1406 | |
82e5c243 AC |
1407 | function Build_Contract_Only_Subprogram (E : Entity_Id) return Node_Id is |
1408 | Loc : constant Source_Ptr := Sloc (E); | |
879ac954 | 1409 | |
82e5c243 AC |
1410 | Missing_Body_Name : constant Name_Id := |
1411 | New_External_Name (Chars (E), "__missing_body"); | |
879ac954 | 1412 | |
82e5c243 AC |
1413 | function Build_Missing_Body_Decls return List_Id; |
1414 | -- Build the declaration of the missing body subprogram and its | |
1415 | -- corresponding pragma Import. | |
879ac954 | 1416 | |
82e5c243 AC |
1417 | function Build_Missing_Body_Subprogram_Call return Node_Id; |
1418 | -- Build the call to the missing body subprogram | |
879ac954 | 1419 | |
82e5c243 AC |
1420 | function Skip_Contract_Only_Subprogram (E : Entity_Id) return Boolean; |
1421 | -- Return True for cases where the wrapper is not needed or we cannot | |
1422 | -- build it. | |
879ac954 | 1423 | |
82e5c243 AC |
1424 | ------------------------------ |
1425 | -- Build_Missing_Body_Decls -- | |
1426 | ------------------------------ | |
879ac954 | 1427 | |
82e5c243 AC |
1428 | function Build_Missing_Body_Decls return List_Id is |
1429 | Spec : constant Node_Id := Declaration_Node (E); | |
1430 | Decl : Node_Id; | |
1431 | Prag : Node_Id; | |
879ac954 | 1432 | |
82e5c243 AC |
1433 | begin |
1434 | Decl := | |
1435 | Make_Subprogram_Declaration (Loc, Copy_Subprogram_Spec (Spec)); | |
1436 | Set_Chars (Defining_Entity (Decl), Missing_Body_Name); | |
879ac954 | 1437 | |
82e5c243 AC |
1438 | Prag := |
1439 | Make_Pragma (Loc, | |
1440 | Chars => Name_Import, | |
1441 | Pragma_Argument_Associations => New_List ( | |
1442 | Make_Pragma_Argument_Association (Loc, | |
1443 | Expression => Make_Identifier (Loc, Name_Ada)), | |
879ac954 | 1444 | |
82e5c243 AC |
1445 | Make_Pragma_Argument_Association (Loc, |
1446 | Expression => Make_Identifier (Loc, Missing_Body_Name)))); | |
879ac954 | 1447 | |
82e5c243 AC |
1448 | return New_List (Decl, Prag); |
1449 | end Build_Missing_Body_Decls; | |
879ac954 | 1450 | |
82e5c243 AC |
1451 | ---------------------------------------- |
1452 | -- Build_Missing_Body_Subprogram_Call -- | |
1453 | ---------------------------------------- | |
879ac954 | 1454 | |
82e5c243 AC |
1455 | function Build_Missing_Body_Subprogram_Call return Node_Id is |
1456 | Forml : Entity_Id; | |
1457 | Parms : List_Id; | |
879ac954 | 1458 | |
82e5c243 AC |
1459 | begin |
1460 | Parms := New_List; | |
879ac954 | 1461 | |
82e5c243 | 1462 | -- Build parameter list that we need |
879ac954 | 1463 | |
82e5c243 AC |
1464 | Forml := First_Formal (E); |
1465 | while Present (Forml) loop | |
1466 | Append_To (Parms, Make_Identifier (Loc, Chars (Forml))); | |
1467 | Next_Formal (Forml); | |
1468 | end loop; | |
879ac954 | 1469 | |
82e5c243 | 1470 | -- Build the call to the missing body subprogram |
879ac954 | 1471 | |
82e5c243 AC |
1472 | if Ekind_In (E, E_Function, E_Generic_Function) then |
1473 | return | |
1474 | Make_Simple_Return_Statement (Loc, | |
1475 | Expression => | |
1476 | Make_Function_Call (Loc, | |
1477 | Name => | |
1478 | Make_Identifier (Loc, Missing_Body_Name), | |
1479 | Parameter_Associations => Parms)); | |
879ac954 | 1480 | |
82e5c243 AC |
1481 | else |
1482 | return | |
1483 | Make_Procedure_Call_Statement (Loc, | |
1484 | Name => | |
1485 | Make_Identifier (Loc, Missing_Body_Name), | |
1486 | Parameter_Associations => Parms); | |
1487 | end if; | |
1488 | end Build_Missing_Body_Subprogram_Call; | |
879ac954 | 1489 | |
82e5c243 AC |
1490 | ----------------------------------- |
1491 | -- Skip_Contract_Only_Subprogram -- | |
1492 | ----------------------------------- | |
879ac954 | 1493 | |
82e5c243 AC |
1494 | function Skip_Contract_Only_Subprogram |
1495 | (E : Entity_Id) return Boolean | |
1496 | is | |
1497 | function Depends_On_Enclosing_Private_Type return Boolean; | |
1498 | -- Return True if some formal of E (or its return type) are | |
1499 | -- private types defined in an enclosing package. | |
879ac954 | 1500 | |
82e5c243 AC |
1501 | function Some_Enclosing_Package_Has_Private_Decls return Boolean; |
1502 | -- Return True if some enclosing package of the current scope has | |
1503 | -- private declarations. | |
879ac954 | 1504 | |
82e5c243 AC |
1505 | --------------------------------------- |
1506 | -- Depends_On_Enclosing_Private_Type -- | |
1507 | --------------------------------------- | |
879ac954 | 1508 | |
82e5c243 AC |
1509 | function Depends_On_Enclosing_Private_Type return Boolean is |
1510 | function Defined_In_Enclosing_Package | |
1511 | (Typ : Entity_Id) return Boolean; | |
1512 | -- Return True if Typ is an entity defined in an enclosing | |
1513 | -- package of the current scope. | |
879ac954 | 1514 | |
82e5c243 AC |
1515 | ---------------------------------- |
1516 | -- Defined_In_Enclosing_Package -- | |
1517 | ---------------------------------- | |
879ac954 | 1518 | |
82e5c243 AC |
1519 | function Defined_In_Enclosing_Package |
1520 | (Typ : Entity_Id) return Boolean | |
1521 | is | |
1522 | Scop : Entity_Id := Scope (Current_Scope); | |
879ac954 | 1523 | |
82e5c243 AC |
1524 | begin |
1525 | while Scop /= Scope (Typ) | |
1526 | and then not Is_Compilation_Unit (Scop) | |
1527 | loop | |
1528 | Scop := Scope (Scop); | |
1529 | end loop; | |
879ac954 | 1530 | |
82e5c243 AC |
1531 | return Scop = Scope (Typ); |
1532 | end Defined_In_Enclosing_Package; | |
879ac954 | 1533 | |
82e5c243 | 1534 | -- Local variables |
879ac954 | 1535 | |
82e5c243 AC |
1536 | Param_E : Entity_Id; |
1537 | Typ : Entity_Id; | |
879ac954 | 1538 | |
82e5c243 | 1539 | -- Start of processing for Depends_On_Enclosing_Private_Type |
879ac954 | 1540 | |
82e5c243 AC |
1541 | begin |
1542 | Param_E := First_Entity (E); | |
1543 | while Present (Param_E) loop | |
1544 | Typ := Etype (Param_E); | |
879ac954 | 1545 | |
82e5c243 AC |
1546 | if Is_Private_Type (Typ) |
1547 | and then Defined_In_Enclosing_Package (Typ) | |
1548 | then | |
1549 | return True; | |
1550 | end if; | |
879ac954 | 1551 | |
82e5c243 AC |
1552 | Next_Entity (Param_E); |
1553 | end loop; | |
879ac954 | 1554 | |
82e5c243 AC |
1555 | return |
1556 | Ekind (E) = E_Function | |
1557 | and then Is_Private_Type (Etype (E)) | |
1558 | and then Defined_In_Enclosing_Package (Etype (E)); | |
1559 | end Depends_On_Enclosing_Private_Type; | |
879ac954 | 1560 | |
82e5c243 AC |
1561 | ---------------------------------------------- |
1562 | -- Some_Enclosing_Package_Has_Private_Decls -- | |
1563 | ---------------------------------------------- | |
879ac954 | 1564 | |
82e5c243 AC |
1565 | function Some_Enclosing_Package_Has_Private_Decls return Boolean is |
1566 | Scop : Entity_Id := Current_Scope; | |
1567 | Pkg_Spec : Node_Id := Package_Specification (Scop); | |
879ac954 | 1568 | |
82e5c243 AC |
1569 | begin |
1570 | loop | |
1571 | if Ekind (Scop) = E_Package | |
1572 | and then Has_Private_Declarations | |
1573 | (Package_Specification (Scop)) | |
1574 | then | |
1575 | Pkg_Spec := Package_Specification (Scop); | |
1576 | end if; | |
879ac954 | 1577 | |
82e5c243 AC |
1578 | exit when Is_Compilation_Unit (Scop); |
1579 | Scop := Scope (Scop); | |
1580 | end loop; | |
879ac954 | 1581 | |
82e5c243 AC |
1582 | return Pkg_Spec /= Package_Specification (Current_Scope); |
1583 | end Some_Enclosing_Package_Has_Private_Decls; | |
879ac954 | 1584 | |
82e5c243 | 1585 | -- Start of processing for Skip_Contract_Only_Subprogram |
879ac954 AC |
1586 | |
1587 | begin | |
82e5c243 AC |
1588 | if not CodePeer_Mode |
1589 | or else Inside_A_Generic | |
1590 | or else not Is_Subprogram (E) | |
1591 | or else Is_Abstract_Subprogram (E) | |
1592 | or else Is_Imported (E) | |
1593 | or else No (Contract (E)) | |
1594 | or else No (Pre_Post_Conditions (Contract (E))) | |
1595 | or else Is_Contract_Only_Body (E) | |
1596 | or else Convention (E) = Convention_Protected | |
1597 | then | |
1598 | return True; | |
879ac954 | 1599 | |
82e5c243 AC |
1600 | -- We do not support building the contract-only subprogram if E |
1601 | -- is a subprogram declared in a nested package that has some | |
1602 | -- formal or return type depending on a private type defined in | |
1603 | -- an enclosing package. | |
879ac954 | 1604 | |
82e5c243 AC |
1605 | elsif Ekind (Current_Scope) = E_Package |
1606 | and then Some_Enclosing_Package_Has_Private_Decls | |
1607 | and then Depends_On_Enclosing_Private_Type | |
1608 | then | |
1609 | if Debug_Flag_Dot_KK then | |
1610 | declare | |
1611 | Saved_Mode : constant Warning_Mode_Type := Warning_Mode; | |
879ac954 | 1612 | |
82e5c243 AC |
1613 | begin |
1614 | -- Warnings are disabled by default under CodePeer_Mode | |
1615 | -- (see switch-c). Enable them temporarily. | |
879ac954 | 1616 | |
82e5c243 AC |
1617 | Warning_Mode := Normal; |
1618 | Error_Msg_N | |
1619 | ("cannot generate contract-only subprogram?", E); | |
1620 | Warning_Mode := Saved_Mode; | |
1621 | end; | |
1622 | end if; | |
879ac954 | 1623 | |
82e5c243 AC |
1624 | return True; |
1625 | end if; | |
879ac954 | 1626 | |
82e5c243 AC |
1627 | return False; |
1628 | end Skip_Contract_Only_Subprogram; | |
879ac954 | 1629 | |
82e5c243 | 1630 | -- Start of processing for Build_Contract_Only_Subprogram |
879ac954 | 1631 | |
82e5c243 AC |
1632 | begin |
1633 | -- Test cases where the wrapper is not needed and cases where we | |
1634 | -- cannot build it. | |
879ac954 | 1635 | |
82e5c243 AC |
1636 | if Skip_Contract_Only_Subprogram (E) then |
1637 | return Empty; | |
1638 | end if; | |
879ac954 | 1639 | |
82e5c243 AC |
1640 | -- Note on calls to Copy_Separate_Tree. The trees we are copying |
1641 | -- here are fully analyzed, but we definitely want fully syntactic | |
1642 | -- unanalyzed trees in the body we construct, so that the analysis | |
1643 | -- generates the right visibility, and that is exactly what the | |
1644 | -- calls to Copy_Separate_Tree give us. | |
879ac954 | 1645 | |
82e5c243 AC |
1646 | declare |
1647 | Name : constant Name_Id := | |
1648 | New_External_Name (Chars (E), "__contract_only"); | |
1649 | Id : Entity_Id; | |
1650 | Bod : Node_Id; | |
879ac954 | 1651 | |
82e5c243 AC |
1652 | begin |
1653 | Bod := | |
1654 | Make_Subprogram_Body (Loc, | |
1655 | Specification => | |
1656 | Copy_Subprogram_Spec (Declaration_Node (E)), | |
1657 | Declarations => | |
1658 | Build_Missing_Body_Decls, | |
1659 | Handled_Statement_Sequence => | |
1660 | Make_Handled_Sequence_Of_Statements (Loc, | |
1661 | Statements => New_List ( | |
1662 | Build_Missing_Body_Subprogram_Call), | |
1663 | End_Label => Make_Identifier (Loc, Name))); | |
879ac954 | 1664 | |
82e5c243 | 1665 | Id := Defining_Unit_Name (Specification (Bod)); |
879ac954 | 1666 | |
82e5c243 AC |
1667 | -- Copy only the pre/postconditions of the original contract |
1668 | -- since it is what we need, but also because pragmas stored in | |
1669 | -- the other fields have N_Pragmas with N_Aspect_Specifications | |
1670 | -- that reference their associated pragma (thus causing an endless | |
1671 | -- loop when trying to copy the subtree). | |
879ac954 | 1672 | |
82e5c243 AC |
1673 | declare |
1674 | New_Contract : constant Node_Id := Make_Contract (Sloc (E)); | |
879ac954 | 1675 | |
82e5c243 AC |
1676 | begin |
1677 | Set_Pre_Post_Conditions (New_Contract, | |
1678 | Copy_Separate_Tree (Pre_Post_Conditions (Contract (E)))); | |
1679 | Set_Contract (Id, New_Contract); | |
1680 | end; | |
879ac954 | 1681 | |
82e5c243 AC |
1682 | -- Fix the name of this new subprogram and link the original |
1683 | -- subprogram with its Contract_Only_Body subprogram. | |
879ac954 | 1684 | |
82e5c243 AC |
1685 | Set_Chars (Id, Name); |
1686 | Set_Is_Contract_Only_Body (Id); | |
1687 | Set_Contract_Only_Body (E, Id); | |
879ac954 | 1688 | |
82e5c243 AC |
1689 | return Bod; |
1690 | end; | |
1691 | end Build_Contract_Only_Subprogram; | |
879ac954 | 1692 | |
82e5c243 AC |
1693 | ------------------------------------- |
1694 | -- Build_Contract_Only_Subprograms -- | |
1695 | ------------------------------------- | |
879ac954 | 1696 | |
82e5c243 AC |
1697 | function Build_Contract_Only_Subprograms (L : List_Id) return List_Id is |
1698 | Decl : Node_Id; | |
1699 | New_Subp : Node_Id; | |
1700 | Result : List_Id := No_List; | |
1701 | Subp_Id : Entity_Id; | |
879ac954 | 1702 | |
879ac954 | 1703 | begin |
82e5c243 AC |
1704 | Decl := First (L); |
1705 | while Present (Decl) loop | |
1706 | if Nkind (Decl) = N_Subprogram_Declaration then | |
1707 | Subp_Id := Defining_Unit_Name (Specification (Decl)); | |
1708 | New_Subp := Build_Contract_Only_Subprogram (Subp_Id); | |
879ac954 | 1709 | |
82e5c243 AC |
1710 | if Present (New_Subp) then |
1711 | if No (Result) then | |
1712 | Result := New_List; | |
1713 | end if; | |
879ac954 | 1714 | |
82e5c243 AC |
1715 | Append_To (Result, New_Subp); |
1716 | end if; | |
879ac954 AC |
1717 | end if; |
1718 | ||
82e5c243 AC |
1719 | Next (Decl); |
1720 | end loop; | |
879ac954 | 1721 | |
82e5c243 AC |
1722 | return Result; |
1723 | end Build_Contract_Only_Subprograms; | |
879ac954 | 1724 | |
82e5c243 AC |
1725 | ------------------------------ |
1726 | -- Has_Private_Declarations -- | |
1727 | ------------------------------ | |
879ac954 | 1728 | |
82e5c243 AC |
1729 | function Has_Private_Declarations (N : Node_Id) return Boolean is |
1730 | begin | |
1731 | if not Nkind_In (N, N_Package_Specification, | |
1732 | N_Protected_Definition, | |
1733 | N_Task_Definition) | |
1734 | then | |
1735 | return False; | |
1736 | else | |
1737 | return | |
1738 | Present (Private_Declarations (N)) | |
1739 | and then Is_Non_Empty_List (Private_Declarations (N)); | |
1740 | end if; | |
1741 | end Has_Private_Declarations; | |
879ac954 | 1742 | |
82e5c243 | 1743 | -- Local variables |
879ac954 | 1744 | |
82e5c243 | 1745 | Subp_List : List_Id; |
879ac954 | 1746 | |
82e5c243 | 1747 | -- Start of processing for Build_And_Analyze_Contract_Only_Subprograms |
879ac954 | 1748 | |
82e5c243 AC |
1749 | begin |
1750 | Subp_List := Build_Contract_Only_Subprograms (L); | |
1751 | Append_Contract_Only_Subprograms (Subp_List); | |
1752 | Analyze_Contract_Only_Subprograms; | |
1753 | end Build_And_Analyze_Contract_Only_Subprograms; | |
879ac954 | 1754 | |
82e5c243 AC |
1755 | ----------------------------- |
1756 | -- Create_Generic_Contract -- | |
1757 | ----------------------------- | |
879ac954 | 1758 | |
82e5c243 AC |
1759 | procedure Create_Generic_Contract (Unit : Node_Id) is |
1760 | Templ : constant Node_Id := Original_Node (Unit); | |
1761 | Templ_Id : constant Entity_Id := Defining_Entity (Templ); | |
879ac954 | 1762 | |
82e5c243 AC |
1763 | procedure Add_Generic_Contract_Pragma (Prag : Node_Id); |
1764 | -- Add a single contract-related source pragma Prag to the contract of | |
1765 | -- generic template Templ_Id. | |
879ac954 | 1766 | |
82e5c243 AC |
1767 | --------------------------------- |
1768 | -- Add_Generic_Contract_Pragma -- | |
1769 | --------------------------------- | |
879ac954 | 1770 | |
82e5c243 AC |
1771 | procedure Add_Generic_Contract_Pragma (Prag : Node_Id) is |
1772 | Prag_Templ : Node_Id; | |
879ac954 | 1773 | |
82e5c243 AC |
1774 | begin |
1775 | -- Mark the pragma to prevent the premature capture of global | |
1776 | -- references when capturing global references of the context | |
1777 | -- (see Save_References_In_Pragma). | |
879ac954 | 1778 | |
82e5c243 | 1779 | Set_Is_Generic_Contract_Pragma (Prag); |
879ac954 | 1780 | |
82e5c243 AC |
1781 | -- Pragmas that apply to a generic subprogram declaration are not |
1782 | -- part of the semantic structure of the generic template: | |
879ac954 | 1783 | |
82e5c243 AC |
1784 | -- generic |
1785 | -- procedure Example (Formal : Integer); | |
1786 | -- pragma Precondition (Formal > 0); | |
879ac954 | 1787 | |
82e5c243 AC |
1788 | -- Create a generic template for such pragmas and link the template |
1789 | -- of the pragma with the generic template. | |
879ac954 | 1790 | |
82e5c243 AC |
1791 | if Nkind (Templ) = N_Generic_Subprogram_Declaration then |
1792 | Rewrite | |
1793 | (Prag, Copy_Generic_Node (Prag, Empty, Instantiating => False)); | |
1794 | Prag_Templ := Original_Node (Prag); | |
c37e6613 | 1795 | |
82e5c243 AC |
1796 | Set_Is_Generic_Contract_Pragma (Prag_Templ); |
1797 | Add_Contract_Item (Prag_Templ, Templ_Id); | |
c37e6613 | 1798 | |
82e5c243 AC |
1799 | -- Otherwise link the pragma with the generic template |
1800 | ||
1801 | else | |
1802 | Add_Contract_Item (Prag, Templ_Id); | |
c37e6613 | 1803 | end if; |
82e5c243 | 1804 | end Add_Generic_Contract_Pragma; |
879ac954 | 1805 | |
82e5c243 | 1806 | -- Local variables |
879ac954 | 1807 | |
82e5c243 AC |
1808 | Context : constant Node_Id := Parent (Unit); |
1809 | Decl : Node_Id := Empty; | |
879ac954 | 1810 | |
82e5c243 | 1811 | -- Start of processing for Create_Generic_Contract |
c37e6613 | 1812 | |
82e5c243 AC |
1813 | begin |
1814 | -- A generic package declaration carries contract-related source pragmas | |
1815 | -- in its visible declarations. | |
c37e6613 | 1816 | |
82e5c243 AC |
1817 | if Nkind (Templ) = N_Generic_Package_Declaration then |
1818 | Set_Ekind (Templ_Id, E_Generic_Package); | |
879ac954 | 1819 | |
82e5c243 AC |
1820 | if Present (Visible_Declarations (Specification (Templ))) then |
1821 | Decl := First (Visible_Declarations (Specification (Templ))); | |
1822 | end if; | |
c37e6613 | 1823 | |
82e5c243 AC |
1824 | -- A generic package body carries contract-related source pragmas in its |
1825 | -- declarations. | |
879ac954 | 1826 | |
82e5c243 AC |
1827 | elsif Nkind (Templ) = N_Package_Body then |
1828 | Set_Ekind (Templ_Id, E_Package_Body); | |
c37e6613 | 1829 | |
82e5c243 AC |
1830 | if Present (Declarations (Templ)) then |
1831 | Decl := First (Declarations (Templ)); | |
1832 | end if; | |
879ac954 | 1833 | |
82e5c243 | 1834 | -- Generic subprogram declaration |
879ac954 | 1835 | |
82e5c243 AC |
1836 | elsif Nkind (Templ) = N_Generic_Subprogram_Declaration then |
1837 | if Nkind (Specification (Templ)) = N_Function_Specification then | |
1838 | Set_Ekind (Templ_Id, E_Generic_Function); | |
1839 | else | |
1840 | Set_Ekind (Templ_Id, E_Generic_Procedure); | |
1841 | end if; | |
879ac954 | 1842 | |
82e5c243 AC |
1843 | -- When the generic subprogram acts as a compilation unit, inspect |
1844 | -- the Pragmas_After list for contract-related source pragmas. | |
879ac954 | 1845 | |
82e5c243 AC |
1846 | if Nkind (Context) = N_Compilation_Unit then |
1847 | if Present (Aux_Decls_Node (Context)) | |
1848 | and then Present (Pragmas_After (Aux_Decls_Node (Context))) | |
1849 | then | |
1850 | Decl := First (Pragmas_After (Aux_Decls_Node (Context))); | |
1851 | end if; | |
879ac954 | 1852 | |
82e5c243 AC |
1853 | -- Otherwise inspect the successive declarations for contract-related |
1854 | -- source pragmas. | |
879ac954 | 1855 | |
82e5c243 AC |
1856 | else |
1857 | Decl := Next (Unit); | |
1858 | end if; | |
879ac954 | 1859 | |
82e5c243 AC |
1860 | -- A generic subprogram body carries contract-related source pragmas in |
1861 | -- its declarations. | |
879ac954 | 1862 | |
82e5c243 AC |
1863 | elsif Nkind (Templ) = N_Subprogram_Body then |
1864 | Set_Ekind (Templ_Id, E_Subprogram_Body); | |
879ac954 | 1865 | |
82e5c243 AC |
1866 | if Present (Declarations (Templ)) then |
1867 | Decl := First (Declarations (Templ)); | |
879ac954 | 1868 | end if; |
82e5c243 | 1869 | end if; |
879ac954 | 1870 | |
82e5c243 AC |
1871 | -- Inspect the relevant declarations looking for contract-related source |
1872 | -- pragmas and add them to the contract of the generic unit. | |
879ac954 | 1873 | |
82e5c243 AC |
1874 | while Present (Decl) loop |
1875 | if Comes_From_Source (Decl) then | |
1876 | if Nkind (Decl) = N_Pragma then | |
879ac954 | 1877 | |
82e5c243 | 1878 | -- The source pragma is a contract annotation |
879ac954 | 1879 | |
82e5c243 AC |
1880 | if Is_Contract_Annotation (Decl) then |
1881 | Add_Generic_Contract_Pragma (Decl); | |
1882 | end if; | |
879ac954 | 1883 | |
82e5c243 AC |
1884 | -- The region where a contract-related source pragma may appear |
1885 | -- ends with the first source non-pragma declaration or statement. | |
879ac954 | 1886 | |
82e5c243 AC |
1887 | else |
1888 | exit; | |
1889 | end if; | |
1890 | end if; | |
879ac954 | 1891 | |
82e5c243 AC |
1892 | Next (Decl); |
1893 | end loop; | |
1894 | end Create_Generic_Contract; | |
879ac954 | 1895 | |
82e5c243 AC |
1896 | -------------------------------- |
1897 | -- Expand_Subprogram_Contract -- | |
1898 | -------------------------------- | |
879ac954 | 1899 | |
82e5c243 AC |
1900 | procedure Expand_Subprogram_Contract (Body_Id : Entity_Id) is |
1901 | Body_Decl : constant Node_Id := Unit_Declaration_Node (Body_Id); | |
1902 | Spec_Id : constant Entity_Id := Corresponding_Spec (Body_Decl); | |
879ac954 | 1903 | |
82e5c243 AC |
1904 | procedure Add_Invariant_And_Predicate_Checks |
1905 | (Subp_Id : Entity_Id; | |
1906 | Stmts : in out List_Id; | |
1907 | Result : out Node_Id); | |
1908 | -- Process the result of function Subp_Id (if applicable) and all its | |
1909 | -- formals. Add invariant and predicate checks where applicable. The | |
1910 | -- routine appends all the checks to list Stmts. If Subp_Id denotes a | |
1911 | -- function, Result contains the entity of parameter _Result, to be | |
1912 | -- used in the creation of procedure _Postconditions. | |
879ac954 | 1913 | |
82e5c243 AC |
1914 | procedure Append_Enabled_Item (Item : Node_Id; List : in out List_Id); |
1915 | -- Append a node to a list. If there is no list, create a new one. When | |
1916 | -- the item denotes a pragma, it is added to the list only when it is | |
1917 | -- enabled. | |
879ac954 | 1918 | |
82e5c243 AC |
1919 | procedure Build_Postconditions_Procedure |
1920 | (Subp_Id : Entity_Id; | |
1921 | Stmts : List_Id; | |
1922 | Result : Entity_Id); | |
1923 | -- Create the body of procedure _Postconditions which handles various | |
1924 | -- assertion actions on exit from subprogram Subp_Id. Stmts is the list | |
1925 | -- of statements to be checked on exit. Parameter Result is the entity | |
1926 | -- of parameter _Result when Subp_Id denotes a function. | |
879ac954 | 1927 | |
82e5c243 AC |
1928 | procedure Process_Contract_Cases (Stmts : in out List_Id); |
1929 | -- Process pragma Contract_Cases. This routine prepends items to the | |
1930 | -- body declarations and appends items to list Stmts. | |
879ac954 | 1931 | |
82e5c243 AC |
1932 | procedure Process_Postconditions (Stmts : in out List_Id); |
1933 | -- Collect all [inherited] spec and body postconditions and accumulate | |
1934 | -- their pragma Check equivalents in list Stmts. | |
879ac954 | 1935 | |
82e5c243 AC |
1936 | procedure Process_Preconditions; |
1937 | -- Collect all [inherited] spec and body preconditions and prepend their | |
1938 | -- pragma Check equivalents to the declarations of the body. | |
879ac954 | 1939 | |
82e5c243 AC |
1940 | ---------------------------------------- |
1941 | -- Add_Invariant_And_Predicate_Checks -- | |
1942 | ---------------------------------------- | |
879ac954 | 1943 | |
82e5c243 AC |
1944 | procedure Add_Invariant_And_Predicate_Checks |
1945 | (Subp_Id : Entity_Id; | |
1946 | Stmts : in out List_Id; | |
1947 | Result : out Node_Id) | |
1948 | is | |
1949 | procedure Add_Invariant_Access_Checks (Id : Entity_Id); | |
1950 | -- Id denotes the return value of a function or a formal parameter. | |
1951 | -- Add an invariant check if the type of Id is access to a type with | |
1952 | -- invariants. The routine appends the generated code to Stmts. | |
1953 | ||
1954 | function Invariant_Checks_OK (Typ : Entity_Id) return Boolean; | |
1955 | -- Determine whether type Typ can benefit from invariant checks. To | |
1956 | -- qualify, the type must have a non-null invariant procedure and | |
1957 | -- subprogram Subp_Id must appear visible from the point of view of | |
1958 | -- the type. | |
879ac954 AC |
1959 | |
1960 | --------------------------------- | |
82e5c243 | 1961 | -- Add_Invariant_Access_Checks -- |
879ac954 AC |
1962 | --------------------------------- |
1963 | ||
82e5c243 AC |
1964 | procedure Add_Invariant_Access_Checks (Id : Entity_Id) is |
1965 | Loc : constant Source_Ptr := Sloc (Body_Decl); | |
1966 | Ref : Node_Id; | |
1967 | Typ : Entity_Id; | |
879ac954 AC |
1968 | |
1969 | begin | |
82e5c243 | 1970 | Typ := Etype (Id); |
879ac954 | 1971 | |
82e5c243 AC |
1972 | if Is_Access_Type (Typ) and then not Is_Access_Constant (Typ) then |
1973 | Typ := Designated_Type (Typ); | |
879ac954 | 1974 | |
82e5c243 AC |
1975 | if Invariant_Checks_OK (Typ) then |
1976 | Ref := | |
1977 | Make_Explicit_Dereference (Loc, | |
1978 | Prefix => New_Occurrence_Of (Id, Loc)); | |
1979 | Set_Etype (Ref, Typ); | |
1980 | ||
1981 | -- Generate: | |
1982 | -- if <Id> /= null then | |
1983 | -- <invariant_call (<Ref>)> | |
1984 | -- end if; | |
1985 | ||
1986 | Append_Enabled_Item | |
1987 | (Item => | |
1988 | Make_If_Statement (Loc, | |
1989 | Condition => | |
1990 | Make_Op_Ne (Loc, | |
1991 | Left_Opnd => New_Occurrence_Of (Id, Loc), | |
1992 | Right_Opnd => Make_Null (Loc)), | |
1993 | Then_Statements => New_List ( | |
1994 | Make_Invariant_Call (Ref))), | |
1995 | List => Stmts); | |
1996 | end if; | |
879ac954 | 1997 | end if; |
82e5c243 | 1998 | end Add_Invariant_Access_Checks; |
879ac954 | 1999 | |
82e5c243 AC |
2000 | ------------------------- |
2001 | -- Invariant_Checks_OK -- | |
2002 | ------------------------- | |
879ac954 | 2003 | |
82e5c243 AC |
2004 | function Invariant_Checks_OK (Typ : Entity_Id) return Boolean is |
2005 | function Has_Public_Visibility_Of_Subprogram return Boolean; | |
2006 | -- Determine whether type Typ has public visibility of subprogram | |
2007 | -- Subp_Id. | |
879ac954 | 2008 | |
82e5c243 AC |
2009 | ----------------------------------------- |
2010 | -- Has_Public_Visibility_Of_Subprogram -- | |
2011 | ----------------------------------------- | |
879ac954 | 2012 | |
82e5c243 AC |
2013 | function Has_Public_Visibility_Of_Subprogram return Boolean is |
2014 | Subp_Decl : constant Node_Id := Unit_Declaration_Node (Subp_Id); | |
879ac954 | 2015 | |
82e5c243 AC |
2016 | begin |
2017 | -- An Initialization procedure must be considered visible even | |
2018 | -- though it is internally generated. | |
879ac954 | 2019 | |
82e5c243 AC |
2020 | if Is_Init_Proc (Defining_Entity (Subp_Decl)) then |
2021 | return True; | |
879ac954 | 2022 | |
82e5c243 AC |
2023 | elsif Ekind (Scope (Typ)) /= E_Package then |
2024 | return False; | |
879ac954 | 2025 | |
82e5c243 AC |
2026 | -- Internally generated code is never publicly visible except |
2027 | -- for a subprogram that is the implementation of an expression | |
2028 | -- function. In that case the visibility is determined by the | |
2029 | -- last check. | |
879ac954 | 2030 | |
82e5c243 AC |
2031 | elsif not Comes_From_Source (Subp_Decl) |
2032 | and then | |
2033 | (Nkind (Original_Node (Subp_Decl)) /= N_Expression_Function | |
2034 | or else not | |
2035 | Comes_From_Source (Defining_Entity (Subp_Decl))) | |
2036 | then | |
2037 | return False; | |
879ac954 | 2038 | |
82e5c243 | 2039 | -- Determine whether the subprogram is declared in the visible |
bfda9ccd AC |
2040 | -- declarations of the package containing the type, or in the |
2041 | -- visible declaration of a child unit of that package. | |
879ac954 | 2042 | |
82e5c243 | 2043 | else |
bfda9ccd AC |
2044 | declare |
2045 | Decls : constant List_Id := | |
2046 | List_Containing (Subp_Decl); | |
2047 | Subp_Scope : constant Entity_Id := | |
2048 | Scope (Defining_Entity (Subp_Decl)); | |
2049 | Typ_Scope : constant Entity_Id := Scope (Typ); | |
2050 | ||
2051 | begin | |
2052 | return | |
2053 | Decls = Visible_Declarations | |
2054 | (Specification (Unit_Declaration_Node (Typ_Scope))) | |
2055 | ||
2056 | or else | |
2057 | (Ekind (Subp_Scope) = E_Package | |
2058 | and then Typ_Scope /= Subp_Scope | |
2059 | and then Is_Child_Unit (Subp_Scope) | |
2060 | and then | |
2061 | Is_Ancestor_Package (Typ_Scope, Subp_Scope) | |
2062 | and then | |
2063 | Decls = Visible_Declarations | |
2064 | (Specification | |
2065 | (Unit_Declaration_Node (Subp_Scope)))); | |
2066 | end; | |
82e5c243 AC |
2067 | end if; |
2068 | end Has_Public_Visibility_Of_Subprogram; | |
879ac954 | 2069 | |
82e5c243 | 2070 | -- Start of processing for Invariant_Checks_OK |
879ac954 | 2071 | |
82e5c243 AC |
2072 | begin |
2073 | return | |
2074 | Has_Invariants (Typ) | |
2075 | and then Present (Invariant_Procedure (Typ)) | |
2076 | and then not Has_Null_Body (Invariant_Procedure (Typ)) | |
2077 | and then Has_Public_Visibility_Of_Subprogram; | |
2078 | end Invariant_Checks_OK; | |
a6363ed3 | 2079 | |
82e5c243 | 2080 | -- Local variables |
879ac954 | 2081 | |
82e5c243 AC |
2082 | Loc : constant Source_Ptr := Sloc (Body_Decl); |
2083 | -- Source location of subprogram body contract | |
879ac954 | 2084 | |
82e5c243 AC |
2085 | Formal : Entity_Id; |
2086 | Typ : Entity_Id; | |
879ac954 | 2087 | |
82e5c243 | 2088 | -- Start of processing for Add_Invariant_And_Predicate_Checks |
879ac954 | 2089 | |
82e5c243 AC |
2090 | begin |
2091 | Result := Empty; | |
879ac954 | 2092 | |
82e5c243 | 2093 | -- Process the result of a function |
a6363ed3 | 2094 | |
82e5c243 AC |
2095 | if Ekind (Subp_Id) = E_Function then |
2096 | Typ := Etype (Subp_Id); | |
a6363ed3 | 2097 | |
82e5c243 AC |
2098 | -- Generate _Result which is used in procedure _Postconditions to |
2099 | -- verify the return value. | |
a6363ed3 | 2100 | |
82e5c243 AC |
2101 | Result := Make_Defining_Identifier (Loc, Name_uResult); |
2102 | Set_Etype (Result, Typ); | |
a6363ed3 | 2103 | |
82e5c243 AC |
2104 | -- Add an invariant check when the return type has invariants and |
2105 | -- the related function is visible to the outside. | |
a6363ed3 | 2106 | |
82e5c243 AC |
2107 | if Invariant_Checks_OK (Typ) then |
2108 | Append_Enabled_Item | |
2109 | (Item => | |
2110 | Make_Invariant_Call (New_Occurrence_Of (Result, Loc)), | |
2111 | List => Stmts); | |
2112 | end if; | |
a6363ed3 | 2113 | |
82e5c243 AC |
2114 | -- Add an invariant check when the return type is an access to a |
2115 | -- type with invariants. | |
a6363ed3 | 2116 | |
82e5c243 AC |
2117 | Add_Invariant_Access_Checks (Result); |
2118 | end if; | |
07820c51 | 2119 | |
82e5c243 AC |
2120 | -- Add invariant and predicates for all formals that qualify |
2121 | ||
2122 | Formal := First_Formal (Subp_Id); | |
2123 | while Present (Formal) loop | |
2124 | Typ := Etype (Formal); | |
2125 | ||
2126 | if Ekind (Formal) /= E_In_Parameter | |
2127 | or else Is_Access_Type (Typ) | |
2128 | then | |
2129 | if Invariant_Checks_OK (Typ) then | |
2130 | Append_Enabled_Item | |
2131 | (Item => | |
2132 | Make_Invariant_Call (New_Occurrence_Of (Formal, Loc)), | |
2133 | List => Stmts); | |
a6363ed3 | 2134 | end if; |
a6363ed3 | 2135 | |
82e5c243 | 2136 | Add_Invariant_Access_Checks (Formal); |
a6363ed3 | 2137 | |
82e5c243 AC |
2138 | -- Note: we used to add predicate checks for OUT and IN OUT |
2139 | -- formals here, but that was misguided, since such checks are | |
2140 | -- performed on the caller side, based on the predicate of the | |
2141 | -- actual, rather than the predicate of the formal. | |
879ac954 | 2142 | |
82e5c243 | 2143 | end if; |
879ac954 | 2144 | |
82e5c243 AC |
2145 | Next_Formal (Formal); |
2146 | end loop; | |
2147 | end Add_Invariant_And_Predicate_Checks; | |
879ac954 | 2148 | |
82e5c243 AC |
2149 | ------------------------- |
2150 | -- Append_Enabled_Item -- | |
2151 | ------------------------- | |
879ac954 | 2152 | |
82e5c243 AC |
2153 | procedure Append_Enabled_Item (Item : Node_Id; List : in out List_Id) is |
2154 | begin | |
2155 | -- Do not chain ignored or disabled pragmas | |
879ac954 | 2156 | |
82e5c243 AC |
2157 | if Nkind (Item) = N_Pragma |
2158 | and then (Is_Ignored (Item) or else Is_Disabled (Item)) | |
2159 | then | |
2160 | null; | |
879ac954 | 2161 | |
82e5c243 | 2162 | -- Otherwise, add the item |
879ac954 | 2163 | |
82e5c243 AC |
2164 | else |
2165 | if No (List) then | |
2166 | List := New_List; | |
2167 | end if; | |
879ac954 | 2168 | |
82e5c243 AC |
2169 | -- If the pragma is a conjunct in a composite postcondition, it |
2170 | -- has been processed in reverse order. In the postcondition body | |
2171 | -- it must appear before the others. | |
879ac954 | 2172 | |
82e5c243 AC |
2173 | if Nkind (Item) = N_Pragma |
2174 | and then From_Aspect_Specification (Item) | |
2175 | and then Split_PPC (Item) | |
2176 | then | |
2177 | Prepend (Item, List); | |
2178 | else | |
2179 | Append (Item, List); | |
2180 | end if; | |
2181 | end if; | |
2182 | end Append_Enabled_Item; | |
879ac954 | 2183 | |
82e5c243 AC |
2184 | ------------------------------------ |
2185 | -- Build_Postconditions_Procedure -- | |
2186 | ------------------------------------ | |
879ac954 | 2187 | |
82e5c243 AC |
2188 | procedure Build_Postconditions_Procedure |
2189 | (Subp_Id : Entity_Id; | |
2190 | Stmts : List_Id; | |
2191 | Result : Entity_Id) | |
2192 | is | |
2193 | procedure Insert_Before_First_Source_Declaration (Stmt : Node_Id); | |
2194 | -- Insert node Stmt before the first source declaration of the | |
2195 | -- related subprogram's body. If no such declaration exists, Stmt | |
2196 | -- becomes the last declaration. | |
2197 | ||
2198 | -------------------------------------------- | |
2199 | -- Insert_Before_First_Source_Declaration -- | |
2200 | -------------------------------------------- | |
2201 | ||
2202 | procedure Insert_Before_First_Source_Declaration (Stmt : Node_Id) is | |
2203 | Decls : constant List_Id := Declarations (Body_Decl); | |
2204 | Decl : Node_Id; | |
879ac954 AC |
2205 | |
2206 | begin | |
82e5c243 AC |
2207 | -- Inspect the declarations of the related subprogram body looking |
2208 | -- for the first source declaration. | |
879ac954 | 2209 | |
82e5c243 AC |
2210 | if Present (Decls) then |
2211 | Decl := First (Decls); | |
2212 | while Present (Decl) loop | |
2213 | if Comes_From_Source (Decl) then | |
2214 | Insert_Before (Decl, Stmt); | |
2215 | return; | |
2216 | end if; | |
879ac954 | 2217 | |
82e5c243 AC |
2218 | Next (Decl); |
2219 | end loop; | |
879ac954 | 2220 | |
82e5c243 AC |
2221 | -- If we get there, then the subprogram body lacks any source |
2222 | -- declarations. The body of _Postconditions now acts as the | |
2223 | -- last declaration. | |
879ac954 | 2224 | |
82e5c243 | 2225 | Append (Stmt, Decls); |
879ac954 | 2226 | |
82e5c243 AC |
2227 | -- Ensure that the body has a declaration list |
2228 | ||
2229 | else | |
2230 | Set_Declarations (Body_Decl, New_List (Stmt)); | |
879ac954 | 2231 | end if; |
82e5c243 | 2232 | end Insert_Before_First_Source_Declaration; |
879ac954 | 2233 | |
82e5c243 | 2234 | -- Local variables |
879ac954 | 2235 | |
82e5c243 AC |
2236 | Loc : constant Source_Ptr := Sloc (Body_Decl); |
2237 | Params : List_Id := No_List; | |
2238 | Proc_Bod : Node_Id; | |
2239 | Proc_Decl : Node_Id; | |
2240 | Proc_Id : Entity_Id; | |
2241 | Proc_Spec : Node_Id; | |
879ac954 | 2242 | |
82e5c243 | 2243 | -- Start of processing for Build_Postconditions_Procedure |
879ac954 | 2244 | |
82e5c243 AC |
2245 | begin |
2246 | -- Nothing to do if there are no actions to check on exit | |
879ac954 | 2247 | |
82e5c243 AC |
2248 | if No (Stmts) then |
2249 | return; | |
2250 | end if; | |
879ac954 | 2251 | |
82e5c243 AC |
2252 | Proc_Id := Make_Defining_Identifier (Loc, Name_uPostconditions); |
2253 | Set_Debug_Info_Needed (Proc_Id); | |
2254 | Set_Postconditions_Proc (Subp_Id, Proc_Id); | |
879ac954 | 2255 | |
82e5c243 AC |
2256 | -- Force the front-end inlining of _Postconditions when generating C |
2257 | -- code, since its body may have references to itypes defined in the | |
2258 | -- enclosing subprogram, which would cause problems for unnesting | |
2259 | -- routines in the absence of inlining. | |
879ac954 | 2260 | |
c63a2ad6 | 2261 | if Modify_Tree_For_C then |
82e5c243 AC |
2262 | Set_Has_Pragma_Inline (Proc_Id); |
2263 | Set_Has_Pragma_Inline_Always (Proc_Id); | |
2264 | Set_Is_Inlined (Proc_Id); | |
2265 | end if; | |
879ac954 | 2266 | |
82e5c243 AC |
2267 | -- The related subprogram is a function: create the specification of |
2268 | -- parameter _Result. | |
879ac954 | 2269 | |
82e5c243 AC |
2270 | if Present (Result) then |
2271 | Params := New_List ( | |
2272 | Make_Parameter_Specification (Loc, | |
2273 | Defining_Identifier => Result, | |
2274 | Parameter_Type => | |
2275 | New_Occurrence_Of (Etype (Result), Loc))); | |
2276 | end if; | |
879ac954 | 2277 | |
82e5c243 AC |
2278 | Proc_Spec := |
2279 | Make_Procedure_Specification (Loc, | |
2280 | Defining_Unit_Name => Proc_Id, | |
2281 | Parameter_Specifications => Params); | |
879ac954 | 2282 | |
82e5c243 | 2283 | Proc_Decl := Make_Subprogram_Declaration (Loc, Proc_Spec); |
879ac954 | 2284 | |
82e5c243 AC |
2285 | -- Insert _Postconditions before the first source declaration of the |
2286 | -- body. This ensures that the body will not cause any premature | |
2287 | -- freezing, as it may mention types: | |
879ac954 | 2288 | |
82e5c243 AC |
2289 | -- procedure Proc (Obj : Array_Typ) is |
2290 | -- procedure _postconditions is | |
2291 | -- begin | |
2292 | -- ... Obj ... | |
2293 | -- end _postconditions; | |
879ac954 | 2294 | |
82e5c243 AC |
2295 | -- subtype T is Array_Typ (Obj'First (1) .. Obj'Last (1)); |
2296 | -- begin | |
879ac954 | 2297 | |
82e5c243 AC |
2298 | -- In the example above, Obj is of type T but the incorrect placement |
2299 | -- of _Postconditions will cause a crash in gigi due to an out-of- | |
2300 | -- order reference. The body of _Postconditions must be placed after | |
2301 | -- the declaration of Temp to preserve correct visibility. | |
879ac954 | 2302 | |
82e5c243 AC |
2303 | Insert_Before_First_Source_Declaration (Proc_Decl); |
2304 | Analyze (Proc_Decl); | |
879ac954 | 2305 | |
82e5c243 AC |
2306 | -- Set an explicit End_Label to override the sloc of the implicit |
2307 | -- RETURN statement, and prevent it from inheriting the sloc of one | |
2308 | -- the postconditions: this would cause confusing debug info to be | |
2309 | -- produced, interfering with coverage-analysis tools. | |
2310 | ||
2311 | Proc_Bod := | |
2312 | Make_Subprogram_Body (Loc, | |
2313 | Specification => | |
2314 | Copy_Subprogram_Spec (Proc_Spec), | |
2315 | Declarations => Empty_List, | |
2316 | Handled_Statement_Sequence => | |
2317 | Make_Handled_Sequence_Of_Statements (Loc, | |
2318 | Statements => Stmts, | |
2319 | End_Label => Make_Identifier (Loc, Chars (Proc_Id)))); | |
2320 | ||
2321 | Insert_After_And_Analyze (Proc_Decl, Proc_Bod); | |
2322 | end Build_Postconditions_Procedure; | |
2323 | ||
2324 | ---------------------------- | |
2325 | -- Process_Contract_Cases -- | |
2326 | ---------------------------- | |
2327 | ||
2328 | procedure Process_Contract_Cases (Stmts : in out List_Id) is | |
2329 | procedure Process_Contract_Cases_For (Subp_Id : Entity_Id); | |
2330 | -- Process pragma Contract_Cases for subprogram Subp_Id | |
2331 | ||
2332 | -------------------------------- | |
2333 | -- Process_Contract_Cases_For -- | |
2334 | -------------------------------- | |
2335 | ||
2336 | procedure Process_Contract_Cases_For (Subp_Id : Entity_Id) is | |
2337 | Items : constant Node_Id := Contract (Subp_Id); | |
2338 | Prag : Node_Id; | |
2339 | ||
2340 | begin | |
2341 | if Present (Items) then | |
2342 | Prag := Contract_Test_Cases (Items); | |
2343 | while Present (Prag) loop | |
a8531f71 HK |
2344 | if Pragma_Name (Prag) = Name_Contract_Cases |
2345 | and then Is_Checked (Prag) | |
2346 | then | |
82e5c243 AC |
2347 | Expand_Pragma_Contract_Cases |
2348 | (CCs => Prag, | |
2349 | Subp_Id => Subp_Id, | |
2350 | Decls => Declarations (Body_Decl), | |
2351 | Stmts => Stmts); | |
2352 | end if; | |
879ac954 | 2353 | |
82e5c243 AC |
2354 | Prag := Next_Pragma (Prag); |
2355 | end loop; | |
2356 | end if; | |
2357 | end Process_Contract_Cases_For; | |
879ac954 | 2358 | |
dcd5fd67 PMR |
2359 | pragma Unmodified (Stmts); |
2360 | -- Stmts is passed as IN OUT to signal that the list can be updated, | |
2361 | -- even if the corresponding integer value representing the list does | |
2362 | -- not change. | |
2363 | ||
82e5c243 | 2364 | -- Start of processing for Process_Contract_Cases |
879ac954 | 2365 | |
82e5c243 AC |
2366 | begin |
2367 | Process_Contract_Cases_For (Body_Id); | |
879ac954 | 2368 | |
82e5c243 AC |
2369 | if Present (Spec_Id) then |
2370 | Process_Contract_Cases_For (Spec_Id); | |
2371 | end if; | |
2372 | end Process_Contract_Cases; | |
879ac954 | 2373 | |
82e5c243 AC |
2374 | ---------------------------- |
2375 | -- Process_Postconditions -- | |
2376 | ---------------------------- | |
879ac954 | 2377 | |
82e5c243 AC |
2378 | procedure Process_Postconditions (Stmts : in out List_Id) is |
2379 | procedure Process_Body_Postconditions (Post_Nam : Name_Id); | |
2380 | -- Collect all [refined] postconditions of a specific kind denoted | |
2381 | -- by Post_Nam that belong to the body, and generate pragma Check | |
2382 | -- equivalents in list Stmts. | |
879ac954 | 2383 | |
82e5c243 AC |
2384 | procedure Process_Spec_Postconditions; |
2385 | -- Collect all [inherited] postconditions of the spec, and generate | |
2386 | -- pragma Check equivalents in list Stmts. | |
2387 | ||
2388 | --------------------------------- | |
2389 | -- Process_Body_Postconditions -- | |
2390 | --------------------------------- | |
2391 | ||
2392 | procedure Process_Body_Postconditions (Post_Nam : Name_Id) is | |
2393 | Items : constant Node_Id := Contract (Body_Id); | |
2394 | Unit_Decl : constant Node_Id := Parent (Body_Decl); | |
879ac954 AC |
2395 | Decl : Node_Id; |
2396 | Prag : Node_Id; | |
879ac954 AC |
2397 | |
2398 | begin | |
2399 | -- Process the contract | |
2400 | ||
2401 | if Present (Items) then | |
2402 | Prag := Pre_Post_Conditions (Items); | |
2403 | while Present (Prag) loop | |
a8531f71 HK |
2404 | if Pragma_Name (Prag) = Post_Nam |
2405 | and then Is_Checked (Prag) | |
2406 | then | |
82e5c243 AC |
2407 | Append_Enabled_Item |
2408 | (Item => Build_Pragma_Check_Equivalent (Prag), | |
2409 | List => Stmts); | |
879ac954 AC |
2410 | end if; |
2411 | ||
2412 | Prag := Next_Pragma (Prag); | |
2413 | end loop; | |
2414 | end if; | |
2415 | ||
82e5c243 AC |
2416 | -- The subprogram body being processed is actually the proper body |
2417 | -- of a stub with a corresponding spec. The subprogram stub may | |
2418 | -- carry a postcondition pragma, in which case it must be taken | |
2419 | -- into account. The pragma appears after the stub. | |
879ac954 | 2420 | |
82e5c243 AC |
2421 | if Present (Spec_Id) and then Nkind (Unit_Decl) = N_Subunit then |
2422 | Decl := Next (Corresponding_Stub (Unit_Decl)); | |
879ac954 AC |
2423 | while Present (Decl) loop |
2424 | ||
2425 | -- Note that non-matching pragmas are skipped | |
2426 | ||
2427 | if Nkind (Decl) = N_Pragma then | |
a8531f71 HK |
2428 | if Pragma_Name (Decl) = Post_Nam |
2429 | and then Is_Checked (Decl) | |
2430 | then | |
82e5c243 AC |
2431 | Append_Enabled_Item |
2432 | (Item => Build_Pragma_Check_Equivalent (Decl), | |
2433 | List => Stmts); | |
879ac954 AC |
2434 | end if; |
2435 | ||
2436 | -- Skip internally generated code | |
2437 | ||
2438 | elsif not Comes_From_Source (Decl) then | |
2439 | null; | |
2440 | ||
82e5c243 AC |
2441 | -- Postcondition pragmas are usually grouped together. There |
2442 | -- is no need to inspect the whole declarative list. | |
879ac954 AC |
2443 | |
2444 | else | |
2445 | exit; | |
2446 | end if; | |
2447 | ||
2448 | Next (Decl); | |
2449 | end loop; | |
2450 | end if; | |
82e5c243 | 2451 | end Process_Body_Postconditions; |
879ac954 | 2452 | |
82e5c243 AC |
2453 | --------------------------------- |
2454 | -- Process_Spec_Postconditions -- | |
2455 | --------------------------------- | |
879ac954 | 2456 | |
82e5c243 AC |
2457 | procedure Process_Spec_Postconditions is |
2458 | Subps : constant Subprogram_List := | |
2459 | Inherited_Subprograms (Spec_Id); | |
a8531f71 | 2460 | Item : Node_Id; |
82e5c243 AC |
2461 | Items : Node_Id; |
2462 | Prag : Node_Id; | |
2463 | Subp_Id : Entity_Id; | |
879ac954 | 2464 | |
82e5c243 AC |
2465 | begin |
2466 | -- Process the contract | |
a6363ed3 | 2467 | |
82e5c243 | 2468 | Items := Contract (Spec_Id); |
a6363ed3 | 2469 | |
82e5c243 AC |
2470 | if Present (Items) then |
2471 | Prag := Pre_Post_Conditions (Items); | |
2472 | while Present (Prag) loop | |
a8531f71 HK |
2473 | if Pragma_Name (Prag) = Name_Postcondition |
2474 | and then Is_Checked (Prag) | |
2475 | then | |
82e5c243 AC |
2476 | Append_Enabled_Item |
2477 | (Item => Build_Pragma_Check_Equivalent (Prag), | |
2478 | List => Stmts); | |
2479 | end if; | |
a6363ed3 | 2480 | |
82e5c243 AC |
2481 | Prag := Next_Pragma (Prag); |
2482 | end loop; | |
2483 | end if; | |
a6363ed3 | 2484 | |
82e5c243 AC |
2485 | -- Process the contracts of all inherited subprograms, looking for |
2486 | -- class-wide postconditions. | |
07820c51 | 2487 | |
82e5c243 AC |
2488 | for Index in Subps'Range loop |
2489 | Subp_Id := Subps (Index); | |
2490 | Items := Contract (Subp_Id); | |
a6363ed3 | 2491 | |
82e5c243 AC |
2492 | if Present (Items) then |
2493 | Prag := Pre_Post_Conditions (Items); | |
2494 | while Present (Prag) loop | |
2495 | if Pragma_Name (Prag) = Name_Postcondition | |
2496 | and then Class_Present (Prag) | |
2497 | then | |
a8531f71 HK |
2498 | Item := |
2499 | Build_Pragma_Check_Equivalent | |
2500 | (Prag => Prag, | |
2501 | Subp_Id => Spec_Id, | |
2502 | Inher_Id => Subp_Id); | |
2503 | ||
2504 | -- The pragma Check equivalent of the class-wide | |
2505 | -- postcondition is still created even though the | |
2506 | -- pragma may be ignored because the equivalent | |
2507 | -- performs semantic checks. | |
2508 | ||
2509 | if Is_Checked (Prag) then | |
2510 | Append_Enabled_Item (Item, Stmts); | |
2511 | end if; | |
82e5c243 | 2512 | end if; |
a6363ed3 | 2513 | |
82e5c243 AC |
2514 | Prag := Next_Pragma (Prag); |
2515 | end loop; | |
a6363ed3 | 2516 | end if; |
879ac954 | 2517 | end loop; |
82e5c243 | 2518 | end Process_Spec_Postconditions; |
879ac954 | 2519 | |
dcd5fd67 PMR |
2520 | pragma Unmodified (Stmts); |
2521 | -- Stmts is passed as IN OUT to signal that the list can be updated, | |
2522 | -- even if the corresponding integer value representing the list does | |
2523 | -- not change. | |
2524 | ||
82e5c243 | 2525 | -- Start of processing for Process_Postconditions |
879ac954 | 2526 | |
82e5c243 AC |
2527 | begin |
2528 | -- The processing of postconditions is done in reverse order (body | |
2529 | -- first) to ensure the following arrangement: | |
879ac954 | 2530 | |
82e5c243 AC |
2531 | -- <refined postconditions from body> |
2532 | -- <postconditions from body> | |
2533 | -- <postconditions from spec> | |
2534 | -- <inherited postconditions> | |
2535 | ||
2536 | Process_Body_Postconditions (Name_Refined_Post); | |
2537 | Process_Body_Postconditions (Name_Postcondition); | |
879ac954 AC |
2538 | |
2539 | if Present (Spec_Id) then | |
82e5c243 | 2540 | Process_Spec_Postconditions; |
879ac954 | 2541 | end if; |
82e5c243 | 2542 | end Process_Postconditions; |
879ac954 | 2543 | |
82e5c243 AC |
2544 | --------------------------- |
2545 | -- Process_Preconditions -- | |
2546 | --------------------------- | |
879ac954 | 2547 | |
82e5c243 AC |
2548 | procedure Process_Preconditions is |
2549 | Class_Pre : Node_Id := Empty; | |
2550 | -- The sole [inherited] class-wide precondition pragma that applies | |
2551 | -- to the subprogram. | |
879ac954 | 2552 | |
82e5c243 AC |
2553 | Insert_Node : Node_Id := Empty; |
2554 | -- The insertion node after which all pragma Check equivalents are | |
2555 | -- inserted. | |
879ac954 | 2556 | |
82e5c243 AC |
2557 | function Is_Prologue_Renaming (Decl : Node_Id) return Boolean; |
2558 | -- Determine whether arbitrary declaration Decl denotes a renaming of | |
2559 | -- a discriminant or protection field _object. | |
879ac954 | 2560 | |
82e5c243 AC |
2561 | procedure Merge_Preconditions (From : Node_Id; Into : Node_Id); |
2562 | -- Merge two class-wide preconditions by "or else"-ing them. The | |
2563 | -- changes are accumulated in parameter Into. Update the error | |
2564 | -- message of Into. | |
879ac954 | 2565 | |
82e5c243 AC |
2566 | procedure Prepend_To_Decls (Item : Node_Id); |
2567 | -- Prepend a single item to the declarations of the subprogram body | |
879ac954 | 2568 | |
82e5c243 AC |
2569 | procedure Prepend_To_Decls_Or_Save (Prag : Node_Id); |
2570 | -- Save a class-wide precondition into Class_Pre, or prepend a normal | |
2571 | -- precondition to the declarations of the body and analyze it. | |
879ac954 | 2572 | |
82e5c243 AC |
2573 | procedure Process_Inherited_Preconditions; |
2574 | -- Collect all inherited class-wide preconditions and merge them into | |
2575 | -- one big precondition to be evaluated as pragma Check. | |
879ac954 | 2576 | |
82e5c243 AC |
2577 | procedure Process_Preconditions_For (Subp_Id : Entity_Id); |
2578 | -- Collect all preconditions of subprogram Subp_Id and prepend their | |
2579 | -- pragma Check equivalents to the declarations of the body. | |
879ac954 | 2580 | |
82e5c243 AC |
2581 | -------------------------- |
2582 | -- Is_Prologue_Renaming -- | |
2583 | -------------------------- | |
879ac954 | 2584 | |
82e5c243 AC |
2585 | function Is_Prologue_Renaming (Decl : Node_Id) return Boolean is |
2586 | Nam : Node_Id; | |
2587 | Obj : Entity_Id; | |
2588 | Pref : Node_Id; | |
2589 | Sel : Node_Id; | |
879ac954 | 2590 | |
82e5c243 AC |
2591 | begin |
2592 | if Nkind (Decl) = N_Object_Renaming_Declaration then | |
2593 | Obj := Defining_Entity (Decl); | |
2594 | Nam := Name (Decl); | |
879ac954 | 2595 | |
82e5c243 AC |
2596 | if Nkind (Nam) = N_Selected_Component then |
2597 | Pref := Prefix (Nam); | |
2598 | Sel := Selector_Name (Nam); | |
879ac954 | 2599 | |
82e5c243 AC |
2600 | -- A discriminant renaming appears as |
2601 | -- Discr : constant ... := Prefix.Discr; | |
879ac954 | 2602 | |
82e5c243 AC |
2603 | if Ekind (Obj) = E_Constant |
2604 | and then Is_Entity_Name (Sel) | |
2605 | and then Present (Entity (Sel)) | |
2606 | and then Ekind (Entity (Sel)) = E_Discriminant | |
2607 | then | |
2608 | return True; | |
879ac954 | 2609 | |
82e5c243 AC |
2610 | -- A protection field renaming appears as |
2611 | -- Prot : ... := _object._object; | |
879ac954 | 2612 | |
82e5c243 AC |
2613 | -- A renamed private component is just a component of |
2614 | -- _object, with an arbitrary name. | |
879ac954 | 2615 | |
82e5c243 AC |
2616 | elsif Ekind (Obj) = E_Variable |
2617 | and then Nkind (Pref) = N_Identifier | |
2618 | and then Chars (Pref) = Name_uObject | |
2619 | and then Nkind (Sel) = N_Identifier | |
2620 | then | |
2621 | return True; | |
2622 | end if; | |
2623 | end if; | |
2624 | end if; | |
879ac954 | 2625 | |
82e5c243 AC |
2626 | return False; |
2627 | end Is_Prologue_Renaming; | |
879ac954 | 2628 | |
82e5c243 AC |
2629 | ------------------------- |
2630 | -- Merge_Preconditions -- | |
2631 | ------------------------- | |
879ac954 | 2632 | |
82e5c243 AC |
2633 | procedure Merge_Preconditions (From : Node_Id; Into : Node_Id) is |
2634 | function Expression_Arg (Prag : Node_Id) return Node_Id; | |
2635 | -- Return the boolean expression argument of a precondition while | |
2636 | -- updating its parentheses count for the subsequent merge. | |
879ac954 | 2637 | |
82e5c243 AC |
2638 | function Message_Arg (Prag : Node_Id) return Node_Id; |
2639 | -- Return the message argument of a precondition | |
879ac954 | 2640 | |
82e5c243 AC |
2641 | -------------------- |
2642 | -- Expression_Arg -- | |
2643 | -------------------- | |
879ac954 | 2644 | |
82e5c243 AC |
2645 | function Expression_Arg (Prag : Node_Id) return Node_Id is |
2646 | Args : constant List_Id := Pragma_Argument_Associations (Prag); | |
2647 | Arg : constant Node_Id := Get_Pragma_Arg (Next (First (Args))); | |
879ac954 | 2648 | |
82e5c243 AC |
2649 | begin |
2650 | if Paren_Count (Arg) = 0 then | |
2651 | Set_Paren_Count (Arg, 1); | |
2652 | end if; | |
879ac954 | 2653 | |
82e5c243 AC |
2654 | return Arg; |
2655 | end Expression_Arg; | |
879ac954 | 2656 | |
82e5c243 AC |
2657 | ----------------- |
2658 | -- Message_Arg -- | |
2659 | ----------------- | |
879ac954 | 2660 | |
82e5c243 AC |
2661 | function Message_Arg (Prag : Node_Id) return Node_Id is |
2662 | Args : constant List_Id := Pragma_Argument_Associations (Prag); | |
2663 | begin | |
2664 | return Get_Pragma_Arg (Last (Args)); | |
2665 | end Message_Arg; | |
879ac954 | 2666 | |
82e5c243 | 2667 | -- Local variables |
879ac954 | 2668 | |
82e5c243 AC |
2669 | From_Expr : constant Node_Id := Expression_Arg (From); |
2670 | From_Msg : constant Node_Id := Message_Arg (From); | |
2671 | Into_Expr : constant Node_Id := Expression_Arg (Into); | |
2672 | Into_Msg : constant Node_Id := Message_Arg (Into); | |
2673 | Loc : constant Source_Ptr := Sloc (Into); | |
879ac954 | 2674 | |
82e5c243 | 2675 | -- Start of processing for Merge_Preconditions |
879ac954 | 2676 | |
82e5c243 AC |
2677 | begin |
2678 | -- Merge the two preconditions by "or else"-ing them | |
879ac954 | 2679 | |
82e5c243 AC |
2680 | Rewrite (Into_Expr, |
2681 | Make_Or_Else (Loc, | |
2682 | Right_Opnd => Relocate_Node (Into_Expr), | |
2683 | Left_Opnd => From_Expr)); | |
879ac954 | 2684 | |
82e5c243 AC |
2685 | -- Merge the two error messages to produce a single message of the |
2686 | -- form: | |
879ac954 | 2687 | |
82e5c243 AC |
2688 | -- failed precondition from ... |
2689 | -- also failed inherited precondition from ... | |
879ac954 | 2690 | |
82e5c243 AC |
2691 | if not Exception_Locations_Suppressed then |
2692 | Start_String (Strval (Into_Msg)); | |
2693 | Store_String_Char (ASCII.LF); | |
2694 | Store_String_Chars (" also "); | |
2695 | Store_String_Chars (Strval (From_Msg)); | |
879ac954 | 2696 | |
82e5c243 AC |
2697 | Set_Strval (Into_Msg, End_String); |
2698 | end if; | |
2699 | end Merge_Preconditions; | |
879ac954 | 2700 | |
82e5c243 AC |
2701 | ---------------------- |
2702 | -- Prepend_To_Decls -- | |
2703 | ---------------------- | |
879ac954 | 2704 | |
82e5c243 | 2705 | procedure Prepend_To_Decls (Item : Node_Id) is |
a8531f71 | 2706 | Decls : List_Id; |
879ac954 | 2707 | |
82e5c243 | 2708 | begin |
a8531f71 HK |
2709 | Decls := Declarations (Body_Decl); |
2710 | ||
82e5c243 | 2711 | -- Ensure that the body has a declarative list |
879ac954 | 2712 | |
82e5c243 AC |
2713 | if No (Decls) then |
2714 | Decls := New_List; | |
2715 | Set_Declarations (Body_Decl, Decls); | |
879ac954 AC |
2716 | end if; |
2717 | ||
82e5c243 AC |
2718 | Prepend_To (Decls, Item); |
2719 | end Prepend_To_Decls; | |
879ac954 | 2720 | |
82e5c243 AC |
2721 | ------------------------------ |
2722 | -- Prepend_To_Decls_Or_Save -- | |
2723 | ------------------------------ | |
879ac954 | 2724 | |
82e5c243 AC |
2725 | procedure Prepend_To_Decls_Or_Save (Prag : Node_Id) is |
2726 | Check_Prag : Node_Id; | |
879ac954 | 2727 | |
82e5c243 AC |
2728 | begin |
2729 | Check_Prag := Build_Pragma_Check_Equivalent (Prag); | |
879ac954 | 2730 | |
82e5c243 AC |
2731 | -- Save the sole class-wide precondition (if any) for the next |
2732 | -- step, where it will be merged with inherited preconditions. | |
879ac954 | 2733 | |
82e5c243 AC |
2734 | if Class_Present (Prag) then |
2735 | pragma Assert (No (Class_Pre)); | |
2736 | Class_Pre := Check_Prag; | |
879ac954 | 2737 | |
82e5c243 AC |
2738 | -- Accumulate the corresponding Check pragmas at the top of the |
2739 | -- declarations. Prepending the items ensures that they will be | |
2740 | -- evaluated in their original order. | |
879ac954 | 2741 | |
82e5c243 AC |
2742 | else |
2743 | if Present (Insert_Node) then | |
2744 | Insert_After (Insert_Node, Check_Prag); | |
2745 | else | |
2746 | Prepend_To_Decls (Check_Prag); | |
2747 | end if; | |
879ac954 | 2748 | |
82e5c243 | 2749 | Analyze (Check_Prag); |
879ac954 | 2750 | end if; |
82e5c243 | 2751 | end Prepend_To_Decls_Or_Save; |
879ac954 | 2752 | |
82e5c243 AC |
2753 | ------------------------------------- |
2754 | -- Process_Inherited_Preconditions -- | |
2755 | ------------------------------------- | |
879ac954 | 2756 | |
82e5c243 | 2757 | procedure Process_Inherited_Preconditions is |
a8531f71 HK |
2758 | Subps : constant Subprogram_List := |
2759 | Inherited_Subprograms (Spec_Id); | |
2760 | ||
2761 | Item : Node_Id; | |
2762 | Items : Node_Id; | |
2763 | Prag : Node_Id; | |
2764 | Subp_Id : Entity_Id; | |
879ac954 | 2765 | |
82e5c243 AC |
2766 | begin |
2767 | -- Process the contracts of all inherited subprograms, looking for | |
2768 | -- class-wide preconditions. | |
879ac954 | 2769 | |
82e5c243 AC |
2770 | for Index in Subps'Range loop |
2771 | Subp_Id := Subps (Index); | |
2772 | Items := Contract (Subp_Id); | |
879ac954 | 2773 | |
82e5c243 AC |
2774 | if Present (Items) then |
2775 | Prag := Pre_Post_Conditions (Items); | |
2776 | while Present (Prag) loop | |
2777 | if Pragma_Name (Prag) = Name_Precondition | |
2778 | and then Class_Present (Prag) | |
2779 | then | |
a8531f71 | 2780 | Item := |
82e5c243 AC |
2781 | Build_Pragma_Check_Equivalent |
2782 | (Prag => Prag, | |
2783 | Subp_Id => Spec_Id, | |
2784 | Inher_Id => Subp_Id); | |
879ac954 | 2785 | |
a8531f71 HK |
2786 | -- The pragma Check equivalent of the class-wide |
2787 | -- precondition is still created even though the | |
2788 | -- pragma may be ignored because the equivalent | |
2789 | -- performs semantic checks. | |
879ac954 | 2790 | |
a8531f71 HK |
2791 | if Is_Checked (Prag) then |
2792 | ||
2793 | -- The spec of an inherited subprogram already | |
2794 | -- yielded a class-wide precondition. Merge the | |
2795 | -- existing precondition with the current one | |
2796 | -- using "or else". | |
2797 | ||
2798 | if Present (Class_Pre) then | |
2799 | Merge_Preconditions (Item, Class_Pre); | |
2800 | else | |
2801 | Class_Pre := Item; | |
2802 | end if; | |
82e5c243 AC |
2803 | end if; |
2804 | end if; | |
879ac954 | 2805 | |
82e5c243 AC |
2806 | Prag := Next_Pragma (Prag); |
2807 | end loop; | |
2808 | end if; | |
2809 | end loop; | |
879ac954 | 2810 | |
82e5c243 | 2811 | -- Add the merged class-wide preconditions |
5f325af2 | 2812 | |
82e5c243 AC |
2813 | if Present (Class_Pre) then |
2814 | Prepend_To_Decls (Class_Pre); | |
2815 | Analyze (Class_Pre); | |
2816 | end if; | |
2817 | end Process_Inherited_Preconditions; | |
5f325af2 | 2818 | |
82e5c243 AC |
2819 | ------------------------------- |
2820 | -- Process_Preconditions_For -- | |
2821 | ------------------------------- | |
5f325af2 | 2822 | |
82e5c243 | 2823 | procedure Process_Preconditions_For (Subp_Id : Entity_Id) is |
a8531f71 HK |
2824 | Items : constant Node_Id := Contract (Subp_Id); |
2825 | ||
82e5c243 AC |
2826 | Decl : Node_Id; |
2827 | Prag : Node_Id; | |
2828 | Subp_Decl : Node_Id; | |
5f325af2 | 2829 | |
82e5c243 AC |
2830 | begin |
2831 | -- Process the contract | |
5f325af2 | 2832 | |
82e5c243 AC |
2833 | if Present (Items) then |
2834 | Prag := Pre_Post_Conditions (Items); | |
2835 | while Present (Prag) loop | |
a8531f71 HK |
2836 | if Pragma_Name (Prag) = Name_Precondition |
2837 | and then Is_Checked (Prag) | |
2838 | then | |
82e5c243 AC |
2839 | Prepend_To_Decls_Or_Save (Prag); |
2840 | end if; | |
5f325af2 | 2841 | |
82e5c243 AC |
2842 | Prag := Next_Pragma (Prag); |
2843 | end loop; | |
2844 | end if; | |
5f325af2 | 2845 | |
82e5c243 AC |
2846 | -- The subprogram declaration being processed is actually a body |
2847 | -- stub. The stub may carry a precondition pragma, in which case | |
2848 | -- it must be taken into account. The pragma appears after the | |
2849 | -- stub. | |
5f325af2 | 2850 | |
82e5c243 | 2851 | Subp_Decl := Unit_Declaration_Node (Subp_Id); |
5f325af2 | 2852 | |
82e5c243 | 2853 | if Nkind (Subp_Decl) = N_Subprogram_Body_Stub then |
5f325af2 | 2854 | |
82e5c243 | 2855 | -- Inspect the declarations following the body stub |
5f325af2 | 2856 | |
82e5c243 AC |
2857 | Decl := Next (Subp_Decl); |
2858 | while Present (Decl) loop | |
5f325af2 | 2859 | |
82e5c243 | 2860 | -- Note that non-matching pragmas are skipped |
5f325af2 | 2861 | |
82e5c243 | 2862 | if Nkind (Decl) = N_Pragma then |
a8531f71 HK |
2863 | if Pragma_Name (Decl) = Name_Precondition |
2864 | and then Is_Checked (Decl) | |
2865 | then | |
82e5c243 AC |
2866 | Prepend_To_Decls_Or_Save (Decl); |
2867 | end if; | |
5f325af2 | 2868 | |
82e5c243 | 2869 | -- Skip internally generated code |
5f325af2 | 2870 | |
82e5c243 AC |
2871 | elsif not Comes_From_Source (Decl) then |
2872 | null; | |
5f325af2 | 2873 | |
82e5c243 AC |
2874 | -- Preconditions are usually grouped together. There is no |
2875 | -- need to inspect the whole declarative list. | |
5f325af2 | 2876 | |
82e5c243 AC |
2877 | else |
2878 | exit; | |
2879 | end if; | |
5f325af2 | 2880 | |
82e5c243 AC |
2881 | Next (Decl); |
2882 | end loop; | |
2883 | end if; | |
2884 | end Process_Preconditions_For; | |
5f325af2 | 2885 | |
82e5c243 | 2886 | -- Local variables |
5f325af2 | 2887 | |
82e5c243 AC |
2888 | Decls : constant List_Id := Declarations (Body_Decl); |
2889 | Decl : Node_Id; | |
5f325af2 | 2890 | |
82e5c243 | 2891 | -- Start of processing for Process_Preconditions |
5f325af2 | 2892 | |
82e5c243 AC |
2893 | begin |
2894 | -- Find the proper insertion point for all pragma Check equivalents | |
5f325af2 | 2895 | |
82e5c243 AC |
2896 | if Present (Decls) then |
2897 | Decl := First (Decls); | |
2898 | while Present (Decl) loop | |
5f325af2 | 2899 | |
82e5c243 AC |
2900 | -- First source declaration terminates the search, because all |
2901 | -- preconditions must be evaluated prior to it, by definition. | |
5f325af2 | 2902 | |
82e5c243 AC |
2903 | if Comes_From_Source (Decl) then |
2904 | exit; | |
5f325af2 | 2905 | |
82e5c243 AC |
2906 | -- Certain internally generated object renamings such as those |
2907 | -- for discriminants and protection fields must be elaborated | |
2908 | -- before the preconditions are evaluated, as their expressions | |
2909 | -- may mention the discriminants. The renamings include those | |
2910 | -- for private components so we need to find the last such. | |
5f325af2 | 2911 | |
82e5c243 AC |
2912 | elsif Is_Prologue_Renaming (Decl) then |
2913 | while Present (Next (Decl)) | |
2914 | and then Is_Prologue_Renaming (Next (Decl)) | |
2915 | loop | |
2916 | Next (Decl); | |
2917 | end loop; | |
5f325af2 | 2918 | |
82e5c243 | 2919 | Insert_Node := Decl; |
5f325af2 | 2920 | |
82e5c243 AC |
2921 | -- Otherwise the declaration does not come from source. This |
2922 | -- also terminates the search, because internal code may raise | |
2923 | -- exceptions which should not preempt the preconditions. | |
5f325af2 | 2924 | |
82e5c243 AC |
2925 | else |
2926 | exit; | |
2927 | end if; | |
5f325af2 | 2928 | |
82e5c243 AC |
2929 | Next (Decl); |
2930 | end loop; | |
2931 | end if; | |
5f325af2 | 2932 | |
82e5c243 AC |
2933 | -- The processing of preconditions is done in reverse order (body |
2934 | -- first), because each pragma Check equivalent is inserted at the | |
2935 | -- top of the declarations. This ensures that the final order is | |
2936 | -- consistent with following diagram: | |
5f325af2 | 2937 | |
82e5c243 AC |
2938 | -- <inherited preconditions> |
2939 | -- <preconditions from spec> | |
2940 | -- <preconditions from body> | |
5f325af2 | 2941 | |
82e5c243 | 2942 | Process_Preconditions_For (Body_Id); |
5f325af2 | 2943 | |
82e5c243 AC |
2944 | if Present (Spec_Id) then |
2945 | Process_Preconditions_For (Spec_Id); | |
2946 | Process_Inherited_Preconditions; | |
2947 | end if; | |
2948 | end Process_Preconditions; | |
5f325af2 | 2949 | |
82e5c243 | 2950 | -- Local variables |
5f325af2 | 2951 | |
82e5c243 AC |
2952 | Restore_Scope : Boolean := False; |
2953 | Result : Entity_Id; | |
2954 | Stmts : List_Id := No_List; | |
2955 | Subp_Id : Entity_Id; | |
5f325af2 | 2956 | |
82e5c243 | 2957 | -- Start of processing for Expand_Subprogram_Contract |
5f325af2 | 2958 | |
82e5c243 AC |
2959 | begin |
2960 | -- Obtain the entity of the initial declaration | |
5f325af2 | 2961 | |
82e5c243 AC |
2962 | if Present (Spec_Id) then |
2963 | Subp_Id := Spec_Id; | |
2964 | else | |
2965 | Subp_Id := Body_Id; | |
2966 | end if; | |
5f325af2 | 2967 | |
82e5c243 | 2968 | -- Do not perform expansion activity when it is not needed |
5f325af2 | 2969 | |
82e5c243 AC |
2970 | if not Expander_Active then |
2971 | return; | |
5f325af2 | 2972 | |
82e5c243 | 2973 | -- ASIS requires an unaltered tree |
5f325af2 | 2974 | |
82e5c243 AC |
2975 | elsif ASIS_Mode then |
2976 | return; | |
5f325af2 | 2977 | |
82e5c243 | 2978 | -- GNATprove does not need the executable semantics of a contract |
5f325af2 | 2979 | |
82e5c243 AC |
2980 | elsif GNATprove_Mode then |
2981 | return; | |
5f325af2 | 2982 | |
82e5c243 AC |
2983 | -- The contract of a generic subprogram or one declared in a generic |
2984 | -- context is not expanded, as the corresponding instance will provide | |
2985 | -- the executable semantics of the contract. | |
5f325af2 | 2986 | |
82e5c243 AC |
2987 | elsif Is_Generic_Subprogram (Subp_Id) or else Inside_A_Generic then |
2988 | return; | |
5f325af2 | 2989 | |
82e5c243 AC |
2990 | -- All subprograms carry a contract, but for some it is not significant |
2991 | -- and should not be processed. This is a small optimization. | |
5f325af2 | 2992 | |
82e5c243 AC |
2993 | elsif not Has_Significant_Contract (Subp_Id) then |
2994 | return; | |
5f325af2 | 2995 | |
82e5c243 AC |
2996 | -- The contract of an ignored Ghost subprogram does not need expansion, |
2997 | -- because the subprogram and all calls to it will be removed. | |
5f325af2 | 2998 | |
82e5c243 AC |
2999 | elsif Is_Ignored_Ghost_Entity (Subp_Id) then |
3000 | return; | |
5f325af2 | 3001 | |
82e5c243 AC |
3002 | -- Do not re-expand the same contract. This scenario occurs when a |
3003 | -- construct is rewritten into something else during its analysis | |
3004 | -- (expression functions for instance). | |
5f325af2 | 3005 | |
a8531f71 | 3006 | elsif Has_Expanded_Contract (Subp_Id) then |
82e5c243 | 3007 | return; |
a8531f71 | 3008 | end if; |
5f325af2 | 3009 | |
a8531f71 | 3010 | -- Prevent multiple expansion attempts of the same contract |
5f325af2 | 3011 | |
a8531f71 | 3012 | Set_Has_Expanded_Contract (Subp_Id); |
5f325af2 | 3013 | |
82e5c243 AC |
3014 | -- Ensure that the formal parameters are visible when expanding all |
3015 | -- contract items. | |
5f325af2 | 3016 | |
82e5c243 AC |
3017 | if not In_Open_Scopes (Subp_Id) then |
3018 | Restore_Scope := True; | |
3019 | Push_Scope (Subp_Id); | |
5f325af2 | 3020 | |
82e5c243 AC |
3021 | if Is_Generic_Subprogram (Subp_Id) then |
3022 | Install_Generic_Formals (Subp_Id); | |
3023 | else | |
3024 | Install_Formals (Subp_Id); | |
3025 | end if; | |
3026 | end if; | |
5f325af2 | 3027 | |
82e5c243 AC |
3028 | -- The expansion of a subprogram contract involves the creation of Check |
3029 | -- pragmas to verify the contract assertions of the spec and body in a | |
3030 | -- particular order. The order is as follows: | |
5f325af2 | 3031 | |
82e5c243 AC |
3032 | -- function Example (...) return ... is |
3033 | -- procedure _Postconditions (...) is | |
3034 | -- begin | |
3035 | -- <refined postconditions from body> | |
3036 | -- <postconditions from body> | |
3037 | -- <postconditions from spec> | |
3038 | -- <inherited postconditions> | |
3039 | -- <contract case consequences> | |
3040 | -- <invariant check of function result> | |
3041 | -- <invariant and predicate checks of parameters> | |
3042 | -- end _Postconditions; | |
5f325af2 | 3043 | |
82e5c243 AC |
3044 | -- <inherited preconditions> |
3045 | -- <preconditions from spec> | |
3046 | -- <preconditions from body> | |
3047 | -- <contract case conditions> | |
5f325af2 | 3048 | |
82e5c243 AC |
3049 | -- <source declarations> |
3050 | -- begin | |
3051 | -- <source statements> | |
5f325af2 | 3052 | |
82e5c243 AC |
3053 | -- _Preconditions (Result); |
3054 | -- return Result; | |
3055 | -- end Example; | |
5f325af2 | 3056 | |
82e5c243 AC |
3057 | -- Routine _Postconditions holds all contract assertions that must be |
3058 | -- verified on exit from the related subprogram. | |
5f325af2 | 3059 | |
82e5c243 AC |
3060 | -- Step 1: Handle all preconditions. This action must come before the |
3061 | -- processing of pragma Contract_Cases because the pragma prepends items | |
3062 | -- to the body declarations. | |
5f325af2 | 3063 | |
82e5c243 AC |
3064 | Process_Preconditions; |
3065 | ||
3066 | -- Step 2: Handle all postconditions. This action must come before the | |
3067 | -- processing of pragma Contract_Cases because the pragma appends items | |
3068 | -- to list Stmts. | |
5f325af2 | 3069 | |
82e5c243 | 3070 | Process_Postconditions (Stmts); |
5f325af2 | 3071 | |
82e5c243 AC |
3072 | -- Step 3: Handle pragma Contract_Cases. This action must come before |
3073 | -- the processing of invariants and predicates because those append | |
3074 | -- items to list Stmts. | |
5f325af2 | 3075 | |
82e5c243 | 3076 | Process_Contract_Cases (Stmts); |
5f325af2 | 3077 | |
82e5c243 AC |
3078 | -- Step 4: Apply invariant and predicate checks on a function result and |
3079 | -- all formals. The resulting checks are accumulated in list Stmts. | |
5f325af2 | 3080 | |
82e5c243 | 3081 | Add_Invariant_And_Predicate_Checks (Subp_Id, Stmts, Result); |
5f325af2 | 3082 | |
82e5c243 | 3083 | -- Step 5: Construct procedure _Postconditions |
5f325af2 | 3084 | |
82e5c243 | 3085 | Build_Postconditions_Procedure (Subp_Id, Stmts, Result); |
5f325af2 | 3086 | |
82e5c243 AC |
3087 | if Restore_Scope then |
3088 | End_Scope; | |
3089 | end if; | |
3090 | end Expand_Subprogram_Contract; | |
5f325af2 | 3091 | |
65e5747e PMR |
3092 | ------------------------------- |
3093 | -- Freeze_Previous_Contracts -- | |
3094 | ------------------------------- | |
3095 | ||
3096 | procedure Freeze_Previous_Contracts (Body_Decl : Node_Id) is | |
3097 | function Causes_Contract_Freezing (N : Node_Id) return Boolean; | |
3098 | pragma Inline (Causes_Contract_Freezing); | |
3099 | -- Determine whether arbitrary node N causes contract freezing | |
3100 | ||
3101 | procedure Freeze_Contracts; | |
3102 | pragma Inline (Freeze_Contracts); | |
3103 | -- Freeze the contracts of all eligible constructs which precede body | |
3104 | -- Body_Decl. | |
3105 | ||
3106 | procedure Freeze_Enclosing_Package_Body; | |
3107 | pragma Inline (Freeze_Enclosing_Package_Body); | |
3108 | -- Freeze the contract of the nearest package body (if any) which | |
3109 | -- encloses body Body_Decl. | |
3110 | ||
3111 | ------------------------------ | |
3112 | -- Causes_Contract_Freezing -- | |
3113 | ------------------------------ | |
3114 | ||
3115 | function Causes_Contract_Freezing (N : Node_Id) return Boolean is | |
3116 | begin | |
3117 | return Nkind_In (N, N_Entry_Body, | |
3118 | N_Package_Body, | |
3119 | N_Protected_Body, | |
3120 | N_Subprogram_Body, | |
3121 | N_Subprogram_Body_Stub, | |
3122 | N_Task_Body); | |
3123 | end Causes_Contract_Freezing; | |
3124 | ||
3125 | ---------------------- | |
3126 | -- Freeze_Contracts -- | |
3127 | ---------------------- | |
3128 | ||
3129 | procedure Freeze_Contracts is | |
3130 | Body_Id : constant Entity_Id := Defining_Entity (Body_Decl); | |
3131 | Decl : Node_Id; | |
3132 | ||
3133 | begin | |
3134 | -- Nothing to do when the body which causes freezing does not appear | |
3135 | -- in a declarative list because there cannot possibly be constructs | |
3136 | -- with contracts. | |
3137 | ||
3138 | if not Is_List_Member (Body_Decl) then | |
3139 | return; | |
3140 | end if; | |
3141 | ||
3142 | -- Inspect the declarations preceding the body, and freeze individual | |
3143 | -- contracts of eligible constructs. | |
3144 | ||
3145 | Decl := Prev (Body_Decl); | |
3146 | while Present (Decl) loop | |
3147 | ||
3148 | -- Stop the traversal when a preceding construct that causes | |
3149 | -- freezing is encountered as there is no point in refreezing | |
3150 | -- the already frozen constructs. | |
3151 | ||
3152 | if Causes_Contract_Freezing (Decl) then | |
3153 | exit; | |
3154 | ||
3155 | -- Entry or subprogram declarations | |
3156 | ||
3157 | elsif Nkind_In (Decl, N_Abstract_Subprogram_Declaration, | |
3158 | N_Entry_Declaration, | |
3159 | N_Generic_Subprogram_Declaration, | |
3160 | N_Subprogram_Declaration) | |
3161 | then | |
3162 | Analyze_Entry_Or_Subprogram_Contract | |
3163 | (Subp_Id => Defining_Entity (Decl), | |
3164 | Freeze_Id => Body_Id); | |
3165 | ||
3166 | -- Objects | |
3167 | ||
3168 | elsif Nkind (Decl) = N_Object_Declaration then | |
3169 | Analyze_Object_Contract | |
3170 | (Obj_Id => Defining_Entity (Decl), | |
3171 | Freeze_Id => Body_Id); | |
3172 | ||
3173 | -- Protected units | |
3174 | ||
3175 | elsif Nkind_In (Decl, N_Protected_Type_Declaration, | |
3176 | N_Single_Protected_Declaration) | |
3177 | then | |
3178 | Analyze_Protected_Contract (Defining_Entity (Decl)); | |
3179 | ||
3180 | -- Subprogram body stubs | |
3181 | ||
3182 | elsif Nkind (Decl) = N_Subprogram_Body_Stub then | |
3183 | Analyze_Subprogram_Body_Stub_Contract (Defining_Entity (Decl)); | |
3184 | ||
3185 | -- Task units | |
3186 | ||
3187 | elsif Nkind_In (Decl, N_Single_Task_Declaration, | |
3188 | N_Task_Type_Declaration) | |
3189 | then | |
3190 | Analyze_Task_Contract (Defining_Entity (Decl)); | |
3191 | end if; | |
3192 | ||
3193 | Prev (Decl); | |
3194 | end loop; | |
3195 | end Freeze_Contracts; | |
3196 | ||
3197 | ----------------------------------- | |
3198 | -- Freeze_Enclosing_Package_Body -- | |
3199 | ----------------------------------- | |
3200 | ||
3201 | procedure Freeze_Enclosing_Package_Body is | |
3202 | Orig_Decl : constant Node_Id := Original_Node (Body_Decl); | |
3203 | Par : Node_Id; | |
3204 | ||
3205 | begin | |
3206 | -- Climb the parent chain looking for an enclosing package body. Do | |
3207 | -- not use the scope stack, because a body utilizes the entity of its | |
3208 | -- corresponding spec. | |
3209 | ||
3210 | Par := Parent (Body_Decl); | |
3211 | while Present (Par) loop | |
3212 | if Nkind (Par) = N_Package_Body then | |
3213 | Analyze_Package_Body_Contract | |
3214 | (Body_Id => Defining_Entity (Par), | |
3215 | Freeze_Id => Defining_Entity (Body_Decl)); | |
3216 | ||
3217 | exit; | |
3218 | ||
3219 | -- Do not look for an enclosing package body when the construct | |
3220 | -- which causes freezing is a body generated for an expression | |
3221 | -- function and it appears within a package spec. This ensures | |
3222 | -- that the traversal will not reach too far up the parent chain | |
3223 | -- and attempt to freeze a package body which must not be frozen. | |
3224 | ||
3225 | -- package body Enclosing_Body | |
3226 | -- with Refined_State => (State => Var) | |
3227 | -- is | |
3228 | -- package Nested is | |
3229 | -- type Some_Type is ...; | |
3230 | -- function Cause_Freezing return ...; | |
3231 | -- private | |
3232 | -- function Cause_Freezing is (...); | |
3233 | -- end Nested; | |
3234 | -- | |
3235 | -- Var : Nested.Some_Type; | |
3236 | ||
3237 | elsif Nkind (Par) = N_Package_Declaration | |
3238 | and then Nkind (Orig_Decl) = N_Expression_Function | |
3239 | then | |
3240 | exit; | |
3241 | ||
3242 | -- Prevent the search from going too far | |
3243 | ||
3244 | elsif Is_Body_Or_Package_Declaration (Par) then | |
3245 | exit; | |
3246 | end if; | |
3247 | ||
3248 | Par := Parent (Par); | |
3249 | end loop; | |
3250 | end Freeze_Enclosing_Package_Body; | |
3251 | ||
3252 | -- Local variables | |
3253 | ||
3254 | Body_Id : constant Entity_Id := Defining_Entity (Body_Decl); | |
3255 | ||
3256 | -- Start of processing for Freeze_Previous_Contracts | |
3257 | ||
3258 | begin | |
3259 | pragma Assert (Causes_Contract_Freezing (Body_Decl)); | |
3260 | ||
3261 | -- A body that is in the process of being inlined appears from source, | |
3262 | -- but carries name _parent. Such a body does not cause freezing of | |
3263 | -- contracts. | |
3264 | ||
3265 | if Chars (Body_Id) = Name_uParent then | |
3266 | return; | |
3267 | end if; | |
3268 | ||
3269 | Freeze_Enclosing_Package_Body; | |
3270 | Freeze_Contracts; | |
3271 | end Freeze_Previous_Contracts; | |
3272 | ||
82e5c243 AC |
3273 | --------------------------------- |
3274 | -- Inherit_Subprogram_Contract -- | |
3275 | --------------------------------- | |
5f325af2 | 3276 | |
82e5c243 AC |
3277 | procedure Inherit_Subprogram_Contract |
3278 | (Subp : Entity_Id; | |
3279 | From_Subp : Entity_Id) | |
3280 | is | |
3281 | procedure Inherit_Pragma (Prag_Id : Pragma_Id); | |
3282 | -- Propagate a pragma denoted by Prag_Id from From_Subp's contract to | |
3283 | -- Subp's contract. | |
5f325af2 | 3284 | |
82e5c243 AC |
3285 | -------------------- |
3286 | -- Inherit_Pragma -- | |
3287 | -------------------- | |
5f325af2 | 3288 | |
82e5c243 AC |
3289 | procedure Inherit_Pragma (Prag_Id : Pragma_Id) is |
3290 | Prag : constant Node_Id := Get_Pragma (From_Subp, Prag_Id); | |
3291 | New_Prag : Node_Id; | |
5f325af2 | 3292 | |
82e5c243 AC |
3293 | begin |
3294 | -- A pragma cannot be part of more than one First_Pragma/Next_Pragma | |
3295 | -- chains, therefore the node must be replicated. The new pragma is | |
3296 | -- flagged as inherited for distinction purposes. | |
5f325af2 | 3297 | |
82e5c243 AC |
3298 | if Present (Prag) then |
3299 | New_Prag := New_Copy_Tree (Prag); | |
3300 | Set_Is_Inherited_Pragma (New_Prag); | |
5f325af2 | 3301 | |
82e5c243 | 3302 | Add_Contract_Item (New_Prag, Subp); |
5f325af2 | 3303 | end if; |
82e5c243 | 3304 | end Inherit_Pragma; |
5f325af2 | 3305 | |
82e5c243 | 3306 | -- Start of processing for Inherit_Subprogram_Contract |
5f325af2 | 3307 | |
82e5c243 AC |
3308 | begin |
3309 | -- Inheritance is carried out only when both entities are subprograms | |
3310 | -- with contracts. | |
5f325af2 | 3311 | |
82e5c243 AC |
3312 | if Is_Subprogram_Or_Generic_Subprogram (Subp) |
3313 | and then Is_Subprogram_Or_Generic_Subprogram (From_Subp) | |
3314 | and then Present (Contract (From_Subp)) | |
3315 | then | |
3316 | Inherit_Pragma (Pragma_Extensions_Visible); | |
3317 | end if; | |
3318 | end Inherit_Subprogram_Contract; | |
5f325af2 | 3319 | |
82e5c243 AC |
3320 | ------------------------------------- |
3321 | -- Instantiate_Subprogram_Contract -- | |
3322 | ------------------------------------- | |
5f325af2 | 3323 | |
82e5c243 AC |
3324 | procedure Instantiate_Subprogram_Contract (Templ : Node_Id; L : List_Id) is |
3325 | procedure Instantiate_Pragmas (First_Prag : Node_Id); | |
3326 | -- Instantiate all contract-related source pragmas found in the list, | |
3327 | -- starting with pragma First_Prag. Each instantiated pragma is added | |
3328 | -- to list L. | |
5f325af2 | 3329 | |
82e5c243 AC |
3330 | ------------------------- |
3331 | -- Instantiate_Pragmas -- | |
3332 | ------------------------- | |
5f325af2 | 3333 | |
82e5c243 AC |
3334 | procedure Instantiate_Pragmas (First_Prag : Node_Id) is |
3335 | Inst_Prag : Node_Id; | |
3336 | Prag : Node_Id; | |
5f325af2 | 3337 | |
82e5c243 AC |
3338 | begin |
3339 | Prag := First_Prag; | |
3340 | while Present (Prag) loop | |
3341 | if Is_Generic_Contract_Pragma (Prag) then | |
3342 | Inst_Prag := | |
3343 | Copy_Generic_Node (Prag, Empty, Instantiating => True); | |
5f325af2 | 3344 | |
82e5c243 AC |
3345 | Set_Analyzed (Inst_Prag, False); |
3346 | Append_To (L, Inst_Prag); | |
3347 | end if; | |
5f325af2 | 3348 | |
82e5c243 AC |
3349 | Prag := Next_Pragma (Prag); |
3350 | end loop; | |
3351 | end Instantiate_Pragmas; | |
5f325af2 | 3352 | |
82e5c243 | 3353 | -- Local variables |
5f325af2 | 3354 | |
82e5c243 | 3355 | Items : constant Node_Id := Contract (Defining_Entity (Templ)); |
5f325af2 | 3356 | |
82e5c243 | 3357 | -- Start of processing for Instantiate_Subprogram_Contract |
5f325af2 | 3358 | |
82e5c243 AC |
3359 | begin |
3360 | if Present (Items) then | |
3361 | Instantiate_Pragmas (Pre_Post_Conditions (Items)); | |
3362 | Instantiate_Pragmas (Contract_Test_Cases (Items)); | |
3363 | Instantiate_Pragmas (Classifications (Items)); | |
3364 | end if; | |
3365 | end Instantiate_Subprogram_Contract; | |
5f325af2 | 3366 | |
82e5c243 AC |
3367 | ---------------------------------------- |
3368 | -- Save_Global_References_In_Contract -- | |
3369 | ---------------------------------------- | |
5f325af2 | 3370 | |
82e5c243 AC |
3371 | procedure Save_Global_References_In_Contract |
3372 | (Templ : Node_Id; | |
3373 | Gen_Id : Entity_Id) | |
3374 | is | |
3375 | procedure Save_Global_References_In_List (First_Prag : Node_Id); | |
3376 | -- Save all global references in contract-related source pragmas found | |
3377 | -- in the list, starting with pragma First_Prag. | |
5f325af2 | 3378 | |
82e5c243 AC |
3379 | ------------------------------------ |
3380 | -- Save_Global_References_In_List -- | |
3381 | ------------------------------------ | |
5f325af2 | 3382 | |
82e5c243 AC |
3383 | procedure Save_Global_References_In_List (First_Prag : Node_Id) is |
3384 | Prag : Node_Id; | |
5f325af2 | 3385 | |
5f325af2 | 3386 | begin |
82e5c243 AC |
3387 | Prag := First_Prag; |
3388 | while Present (Prag) loop | |
3389 | if Is_Generic_Contract_Pragma (Prag) then | |
3390 | Save_Global_References (Prag); | |
3391 | end if; | |
3392 | ||
3393 | Prag := Next_Pragma (Prag); | |
3394 | end loop; | |
3395 | end Save_Global_References_In_List; | |
5f325af2 AC |
3396 | |
3397 | -- Local variables | |
3398 | ||
82e5c243 | 3399 | Items : constant Node_Id := Contract (Defining_Entity (Templ)); |
5f325af2 | 3400 | |
82e5c243 | 3401 | -- Start of processing for Save_Global_References_In_Contract |
5f325af2 AC |
3402 | |
3403 | begin | |
82e5c243 AC |
3404 | -- The entity of the analyzed generic copy must be on the scope stack |
3405 | -- to ensure proper detection of global references. | |
3406 | ||
3407 | Push_Scope (Gen_Id); | |
3408 | ||
3409 | if Permits_Aspect_Specifications (Templ) | |
3410 | and then Has_Aspects (Templ) | |
3411 | then | |
3412 | Save_Global_References_In_Aspects (Templ); | |
3413 | end if; | |
3414 | ||
3415 | if Present (Items) then | |
3416 | Save_Global_References_In_List (Pre_Post_Conditions (Items)); | |
3417 | Save_Global_References_In_List (Contract_Test_Cases (Items)); | |
3418 | Save_Global_References_In_List (Classifications (Items)); | |
3419 | end if; | |
3420 | ||
3421 | Pop_Scope; | |
3422 | end Save_Global_References_In_Contract; | |
5f325af2 | 3423 | |
879ac954 | 3424 | end Contracts; |