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