|
111
|
1 ------------------------------------------------------------------------------
|
|
|
2 -- --
|
|
|
3 -- GNAT COMPILER COMPONENTS --
|
|
|
4 -- --
|
|
|
5 -- C O N T R A C T S --
|
|
|
6 -- --
|
|
|
7 -- B o d y --
|
|
|
8 -- --
|
|
145
|
9 -- Copyright (C) 2015-2019, Free Software Foundation, Inc. --
|
|
111
|
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;
|
|
131
|
34 with Freeze; use Freeze;
|
|
|
35 with Lib; use Lib;
|
|
111
|
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;
|
|
|
45 with Sem_Ch13; use Sem_Ch13;
|
|
|
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;
|
|
131
|
51 with Stand; use Stand;
|
|
111
|
52 with Stringt; use Stringt;
|
|
|
53 with Tbuild; use Tbuild;
|
|
|
54
|
|
|
55 package body Contracts is
|
|
|
56
|
|
131
|
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
|
|
111
|
63
|
|
|
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
|
|
|
118 -- A contract must contain only pragmas
|
|
|
119
|
|
|
120 pragma Assert (Nkind (Prag) = N_Pragma);
|
|
|
121 Prag_Nam : constant Name_Id := Pragma_Name (Prag);
|
|
|
122
|
|
|
123 -- Start of processing for Add_Contract_Item
|
|
|
124
|
|
|
125 begin
|
|
|
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
|
|
|
133 -- Constants, the applicable pragmas are:
|
|
|
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
|
|
|
146 -- Entry bodies, the applicable pragmas are:
|
|
|
147 -- Refined_Depends
|
|
|
148 -- Refined_Global
|
|
|
149 -- Refined_Post
|
|
|
150
|
|
|
151 elsif Is_Entry_Body (Id) then
|
|
|
152 if Nam_In (Prag_Nam, Name_Refined_Depends, Name_Refined_Global) then
|
|
|
153 Add_Classification;
|
|
|
154
|
|
|
155 elsif Prag_Nam = Name_Refined_Post then
|
|
|
156 Add_Pre_Post_Condition;
|
|
|
157
|
|
|
158 -- The pragma is not a proper contract item
|
|
|
159
|
|
|
160 else
|
|
|
161 raise Program_Error;
|
|
|
162 end if;
|
|
|
163
|
|
|
164 -- Entry or subprogram declarations, the applicable pragmas are:
|
|
|
165 -- Attach_Handler
|
|
|
166 -- Contract_Cases
|
|
|
167 -- Depends
|
|
|
168 -- Extensions_Visible
|
|
|
169 -- Global
|
|
|
170 -- Interrupt_Handler
|
|
|
171 -- Postcondition
|
|
|
172 -- Precondition
|
|
|
173 -- Test_Case
|
|
|
174 -- Volatile_Function
|
|
|
175
|
|
|
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)
|
|
|
181 then
|
|
|
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;
|
|
|
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
|
|
|
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
|
|
|
204 -- The pragma is not a proper contract item
|
|
|
205
|
|
|
206 else
|
|
|
207 raise Program_Error;
|
|
|
208 end if;
|
|
|
209
|
|
|
210 -- Packages or instantiations, the applicable pragmas are:
|
|
|
211 -- Abstract_States
|
|
|
212 -- Initial_Condition
|
|
|
213 -- Initializes
|
|
|
214 -- Part_Of (instantiation only)
|
|
|
215
|
|
|
216 elsif Ekind_In (Id, E_Generic_Package, E_Package) then
|
|
|
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
|
|
|
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
|
|
|
260 -- Subprogram bodies, the applicable pragmas are:
|
|
|
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
|
|
|
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
|
|
|
300 -- Part_Of
|
|
|
301
|
|
|
302 elsif Ekind (Id) = E_Task_Type then
|
|
|
303 if Nam_In (Prag_Nam, Name_Depends, Name_Global, Name_Part_Of) then
|
|
|
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:
|
|
|
313 -- Async_Readers
|
|
|
314 -- Async_Writers
|
|
|
315 -- Constant_After_Elaboration
|
|
|
316 -- Depends
|
|
|
317 -- Effective_Reads
|
|
|
318 -- Effective_Writes
|
|
|
319 -- Global
|
|
145
|
320 -- No_Caching
|
|
111
|
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,
|
|
|
327 Name_Depends,
|
|
|
328 Name_Effective_Reads,
|
|
|
329 Name_Effective_Writes,
|
|
|
330 Name_Global,
|
|
145
|
331 Name_No_Caching,
|
|
111
|
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
|
|
|
344 -----------------------
|
|
|
345 -- Analyze_Contracts --
|
|
|
346 -----------------------
|
|
|
347
|
|
|
348 procedure Analyze_Contracts (L : List_Id) is
|
|
131
|
349 Decl : Node_Id;
|
|
|
350
|
|
111
|
351 begin
|
|
|
352 Decl := First (L);
|
|
|
353 while Present (Decl) loop
|
|
|
354
|
|
|
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
|
|
|
362 declare
|
|
|
363 Subp_Id : constant Entity_Id := Defining_Entity (Decl);
|
|
|
364
|
|
|
365 begin
|
|
131
|
366 Analyze_Entry_Or_Subprogram_Contract (Subp_Id);
|
|
111
|
367
|
|
|
368 -- If analysis of a class-wide pre/postcondition indicates
|
|
|
369 -- that a class-wide clone is needed, analyze its declaration
|
|
|
370 -- now. Its body is created when the body of the original
|
|
|
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;
|
|
|
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
|
|
131
|
388 Analyze_Object_Contract (Defining_Entity (Decl));
|
|
|
389
|
|
|
390 -- Package instantiation
|
|
|
391
|
|
|
392 elsif Nkind (Decl) = N_Package_Instantiation then
|
|
|
393 Analyze_Package_Instantiation_Contract (Defining_Entity (Decl));
|
|
111
|
394
|
|
|
395 -- Protected units
|
|
|
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));
|
|
|
413
|
|
131
|
414 -- For type declarations, we need to do the preanalysis of Iterable
|
|
|
415 -- aspect specifications.
|
|
|
416
|
|
111
|
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);
|
|
131
|
425
|
|
111
|
426 begin
|
|
|
427 if Present (It) then
|
|
|
428 Validate_Iterable_Aspect (E, It);
|
|
|
429 end if;
|
|
|
430 end;
|
|
|
431 end if;
|
|
|
432
|
|
|
433 Next (Decl);
|
|
|
434 end loop;
|
|
|
435 end Analyze_Contracts;
|
|
|
436
|
|
|
437 -----------------------------------------------
|
|
|
438 -- Analyze_Entry_Or_Subprogram_Body_Contract --
|
|
|
439 -----------------------------------------------
|
|
|
440
|
|
|
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
|
|
|
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);
|
|
|
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
|
|
|
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
|
|
|
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
|
|
|
477 Set_SPARK_Mode (Body_Id);
|
|
|
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
|
|
|
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.
|
|
|
491
|
|
|
492 if SPARK_Mode = On
|
|
|
493 and then Ekind_In (Body_Id, E_Function, E_Generic_Function)
|
|
|
494 and then Comes_From_Source (Spec_Id)
|
|
|
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
|
|
|
503 Restore_SPARK_Mode (Saved_SM, Saved_SMP);
|
|
|
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
|
|
|
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
|
|
|
531 procedure Analyze_Entry_Or_Subprogram_Contract
|
|
|
532 (Subp_Id : Entity_Id;
|
|
|
533 Freeze_Id : Entity_Id := Empty)
|
|
|
534 is
|
|
|
535 Items : constant Node_Id := Contract (Subp_Id);
|
|
|
536 Subp_Decl : constant Node_Id := Unit_Declaration_Node (Subp_Id);
|
|
|
537
|
|
|
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
|
|
|
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;
|
|
|
549 Prag : Node_Id;
|
|
|
550 Prag_Nam : Name_Id;
|
|
|
551
|
|
|
552 begin
|
|
|
553 -- Do not analyze a contract multiple times
|
|
|
554
|
|
|
555 if Present (Items) then
|
|
|
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
|
|
|
568 Set_SPARK_Mode (Subp_Id);
|
|
|
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
|
|
|
578 -- Do not analyze the pre/postconditions of an entry declaration
|
|
|
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).
|
|
|
582
|
|
|
583 if Skip_Assert_Exprs then
|
|
|
584 null;
|
|
|
585
|
|
131
|
586 -- Otherwise analyze the pre/postconditions.
|
|
|
587 -- If these come from an aspect specification, their expressions
|
|
|
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.
|
|
111
|
592
|
|
|
593 else
|
|
131
|
594 declare
|
|
|
595 Bod : Node_Id;
|
|
|
596 Freeze_Types : Boolean := False;
|
|
|
597
|
|
|
598 begin
|
|
|
599 if Present (Freeze_Id) then
|
|
|
600 Bod := Unit_Declaration_Node (Freeze_Id);
|
|
|
601
|
|
|
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
|
|
|
614 if Freeze_Types
|
|
|
615 and then Present (Corresponding_Aspect (Prag))
|
|
|
616 then
|
|
|
617 Freeze_Expr_Types
|
|
|
618 (Def_Id => Subp_Id,
|
|
|
619 Typ => Standard_Boolean,
|
|
|
620 Expr => Expression (Corresponding_Aspect (Prag)),
|
|
|
621 N => Bod);
|
|
|
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;
|
|
111
|
628 end if;
|
|
|
629
|
|
|
630 -- Analyze contract-cases and test-cases
|
|
|
631
|
|
|
632 Prag := Contract_Test_Cases (Items);
|
|
|
633 while Present (Prag) loop
|
|
|
634 Prag_Nam := Pragma_Name (Prag);
|
|
|
635
|
|
|
636 if Prag_Nam = Name_Contract_Cases then
|
|
|
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
|
|
|
649 Analyze_Contract_Cases_In_Decl_Part (Prag, Freeze_Id);
|
|
|
650 end if;
|
|
|
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
|
|
|
663 Prag_Nam := Pragma_Name (Prag);
|
|
|
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)
|
|
|
703 and then Comes_From_Source (Subp_Id)
|
|
|
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
|
|
|
712 Restore_SPARK_Mode (Saved_SM, Saved_SMP);
|
|
|
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
|
|
|
724 -----------------------------
|
|
|
725 -- Analyze_Object_Contract --
|
|
|
726 -----------------------------
|
|
|
727
|
|
|
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
|
|
|
732 procedure Analyze_Object_Contract
|
|
|
733 (Obj_Id : Entity_Id;
|
|
|
734 Freeze_Id : Entity_Id := Empty)
|
|
|
735 is
|
|
|
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;
|
|
145
|
746 NC_Val : Boolean := False;
|
|
111
|
747 Items : Node_Id;
|
|
|
748 Prag : Node_Id;
|
|
|
749 Ref_Elmt : Elmt_Id;
|
|
|
750 Seen : Boolean := False;
|
|
|
751
|
|
|
752 begin
|
|
|
753 -- The loop parameter in an element iterator over a formal container
|
|
|
754 -- is declared with an object declaration, but no contracts apply.
|
|
|
755
|
|
|
756 if Ekind (Obj_Id) = E_Loop_Parameter then
|
|
|
757 return;
|
|
|
758 end if;
|
|
|
759
|
|
|
760 -- Do not analyze a contract multiple times
|
|
|
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
|
|
|
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
|
|
|
781 Set_SPARK_Mode (Obj_Id);
|
|
|
782 end if;
|
|
|
783
|
|
|
784 -- Constant-related checks
|
|
|
785
|
|
|
786 if Ekind (Obj_Id) = E_Constant then
|
|
|
787
|
|
|
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
|
|
|
799 -- A constant cannot be effectively volatile (SPARK RM 7.1.3(4)).
|
|
|
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
|
|
|
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
|
|
|
813 -- Variable-related checks
|
|
|
814
|
|
|
815 else pragma Assert (Ekind (Obj_Id) = E_Variable);
|
|
|
816
|
|
|
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
|
|
145
|
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
|
|
111
|
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
|
|
|
890 Analyze_Part_Of_In_Decl_Part (Prag, Freeze_Id);
|
|
|
891
|
|
|
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
|
|
|
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
|
|
|
916 -- The following checks are relevant only when SPARK_Mode is on, as
|
|
|
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
|
|
131
|
928 ("volatile variable & must be declared at library level "
|
|
|
929 & "(SPARK RM 7.1.3(3))", Obj_Id);
|
|
111
|
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);
|
|
|
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;
|
|
|
956 end if;
|
|
|
957
|
|
|
958 -- Common checks
|
|
|
959
|
|
|
960 if Comes_From_Source (Obj_Id) and then Is_Ghost_Entity (Obj_Id) then
|
|
|
961
|
|
|
962 -- A Ghost object cannot be of a type that yields a synchronized
|
|
|
963 -- object (SPARK RM 6.9(19)).
|
|
|
964
|
|
|
965 if Yields_Synchronized_Object (Obj_Typ) then
|
|
|
966 Error_Msg_N ("ghost object & cannot be synchronized", Obj_Id);
|
|
|
967
|
|
|
968 -- A Ghost object cannot be effectively volatile (SPARK RM 6.9(7) and
|
|
|
969 -- SPARK RM 6.9(19)).
|
|
|
970
|
|
|
971 elsif Is_Effectively_Volatile (Obj_Id) then
|
|
|
972 Error_Msg_N ("ghost object & cannot be volatile", Obj_Id);
|
|
|
973
|
|
|
974 -- A Ghost object cannot be imported or exported (SPARK RM 6.9(7)).
|
|
|
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.
|
|
|
977
|
|
|
978 elsif Is_Exported (Obj_Id) then
|
|
|
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;
|
|
|
985
|
|
|
986 -- Restore the SPARK_Mode of the enclosing context after all delayed
|
|
|
987 -- pragmas have been analyzed.
|
|
|
988
|
|
|
989 Restore_SPARK_Mode (Saved_SM, Saved_SMP);
|
|
|
990 end Analyze_Object_Contract;
|
|
|
991
|
|
|
992 -----------------------------------
|
|
|
993 -- Analyze_Package_Body_Contract --
|
|
|
994 -----------------------------------
|
|
|
995
|
|
|
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
|
|
|
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);
|
|
|
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
|
|
|
1012 Ref_State : Node_Id;
|
|
|
1013
|
|
|
1014 begin
|
|
|
1015 -- Do not analyze a contract multiple times
|
|
|
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
|
|
|
1030 Set_SPARK_Mode (Body_Id);
|
|
|
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);
|
|
|
1039 end if;
|
|
|
1040
|
|
|
1041 -- Restore the SPARK_Mode of the enclosing context after all delayed
|
|
|
1042 -- pragmas have been analyzed.
|
|
|
1043
|
|
|
1044 Restore_SPARK_Mode (Saved_SM, Saved_SMP);
|
|
|
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
|
|
|
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
|
|
|
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);
|
|
|
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
|
|
|
1072 Init : Node_Id := Empty;
|
|
|
1073 Init_Cond : Node_Id := Empty;
|
|
|
1074 Prag : Node_Id;
|
|
|
1075 Prag_Nam : Name_Id;
|
|
|
1076
|
|
|
1077 begin
|
|
|
1078 -- Do not analyze a contract multiple times
|
|
|
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
|
|
|
1093 Set_SPARK_Mode (Pack_Id);
|
|
|
1094
|
|
|
1095 if Present (Items) then
|
|
|
1096
|
|
|
1097 -- Locate and store pragmas Initial_Condition and Initializes, since
|
|
|
1098 -- their order of analysis matters.
|
|
|
1099
|
|
|
1100 Prag := Classifications (Items);
|
|
|
1101 while Present (Prag) loop
|
|
|
1102 Prag_Nam := Pragma_Name (Prag);
|
|
|
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
|
|
|
1114 -- Analyze the initialization-related pragmas. Initializes must come
|
|
|
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
|
|
|
1126 -- Restore the SPARK_Mode of the enclosing context after all delayed
|
|
|
1127 -- pragmas have been analyzed.
|
|
|
1128
|
|
|
1129 Restore_SPARK_Mode (Saved_SM, Saved_SMP);
|
|
|
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;
|
|
|
1140
|
|
131
|
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;
|
|
111
|
1159
|
|
|
1160 begin
|
|
131
|
1161 -- Nothing to do when the package instantiation is erroneous or left
|
|
|
1162 -- partially decorated.
|
|
|
1163
|
|
|
1164 if No (Inst_Spec) then
|
|
111
|
1165 return;
|
|
|
1166 end if;
|
|
|
1167
|
|
131
|
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);
|
|
111
|
1189 end if;
|
|
131
|
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;
|
|
111
|
1196
|
|
|
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);
|
|
|
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;
|
|
|
1214 end Analyze_Protected_Contract;
|
|
|
1215
|
|
|
1216 -------------------------------------------
|
|
|
1217 -- Analyze_Subprogram_Body_Stub_Contract --
|
|
|
1218 -------------------------------------------
|
|
|
1219
|
|
|
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);
|
|
|
1223
|
|
|
1224 begin
|
|
|
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.
|
|
|
1228
|
|
|
1229 -- The stub is a completion, the applicable pragmas are:
|
|
|
1230 -- Refined_Depends
|
|
|
1231 -- Refined_Global
|
|
|
1232
|
|
|
1233 if Present (Spec_Id) then
|
|
|
1234 Analyze_Entry_Or_Subprogram_Body_Contract (Stub_Id);
|
|
|
1235
|
|
|
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
|
|
|
1243
|
|
|
1244 else
|
|
|
1245 Analyze_Entry_Or_Subprogram_Contract (Stub_Id);
|
|
|
1246 end if;
|
|
|
1247 end Analyze_Subprogram_Body_Stub_Contract;
|
|
|
1248
|
|
|
1249 ---------------------------
|
|
|
1250 -- Analyze_Task_Contract --
|
|
|
1251 ---------------------------
|
|
|
1252
|
|
|
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
|
|
|
1257 procedure Analyze_Task_Contract (Task_Id : Entity_Id) is
|
|
|
1258 Items : constant Node_Id := Contract (Task_Id);
|
|
|
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;
|
|
|
1265
|
|
|
1266 begin
|
|
|
1267 -- Do not analyze a contract multiple times
|
|
|
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
|
|
|
1280 -- related task unit.
|
|
|
1281
|
|
|
1282 Set_SPARK_Mode (Task_Id);
|
|
|
1283
|
|
|
1284 -- Analyze Global first, as Depends may mention items classified in the
|
|
|
1285 -- global categorization.
|
|
|
1286
|
|
|
1287 Prag := Get_Pragma (Task_Id, Pragma_Global);
|
|
|
1288
|
|
|
1289 if Present (Prag) then
|
|
|
1290 Analyze_Global_In_Decl_Part (Prag);
|
|
|
1291 end if;
|
|
|
1292
|
|
|
1293 -- Depends must be analyzed after Global in order to see the modes of
|
|
|
1294 -- all global items.
|
|
|
1295
|
|
|
1296 Prag := Get_Pragma (Task_Id, Pragma_Depends);
|
|
|
1297
|
|
|
1298 if Present (Prag) then
|
|
|
1299 Analyze_Depends_In_Decl_Part (Prag);
|
|
|
1300 end if;
|
|
|
1301
|
|
|
1302 -- Restore the SPARK_Mode of the enclosing context after all delayed
|
|
|
1303 -- pragmas have been analyzed.
|
|
|
1304
|
|
|
1305 Restore_SPARK_Mode (Saved_SM, Saved_SMP);
|
|
|
1306 end Analyze_Task_Contract;
|
|
|
1307
|
|
|
1308 -----------------------------
|
|
|
1309 -- Create_Generic_Contract --
|
|
|
1310 -----------------------------
|
|
|
1311
|
|
|
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);
|
|
|
1315
|
|
|
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.
|
|
|
1319
|
|
|
1320 ---------------------------------
|
|
|
1321 -- Add_Generic_Contract_Pragma --
|
|
|
1322 ---------------------------------
|
|
|
1323
|
|
|
1324 procedure Add_Generic_Contract_Pragma (Prag : Node_Id) is
|
|
|
1325 Prag_Templ : Node_Id;
|
|
|
1326
|
|
|
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).
|
|
|
1331
|
|
|
1332 Set_Is_Generic_Contract_Pragma (Prag);
|
|
|
1333
|
|
|
1334 -- Pragmas that apply to a generic subprogram declaration are not
|
|
|
1335 -- part of the semantic structure of the generic template:
|
|
|
1336
|
|
|
1337 -- generic
|
|
|
1338 -- procedure Example (Formal : Integer);
|
|
|
1339 -- pragma Precondition (Formal > 0);
|
|
|
1340
|
|
|
1341 -- Create a generic template for such pragmas and link the template
|
|
|
1342 -- of the pragma with the generic template.
|
|
|
1343
|
|
|
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);
|
|
|
1348
|
|
|
1349 Set_Is_Generic_Contract_Pragma (Prag_Templ);
|
|
|
1350 Add_Contract_Item (Prag_Templ, Templ_Id);
|
|
|
1351
|
|
|
1352 -- Otherwise link the pragma with the generic template
|
|
|
1353
|
|
|
1354 else
|
|
|
1355 Add_Contract_Item (Prag, Templ_Id);
|
|
|
1356 end if;
|
|
|
1357 end Add_Generic_Contract_Pragma;
|
|
|
1358
|
|
|
1359 -- Local variables
|
|
|
1360
|
|
|
1361 Context : constant Node_Id := Parent (Unit);
|
|
|
1362 Decl : Node_Id := Empty;
|
|
|
1363
|
|
|
1364 -- Start of processing for Create_Generic_Contract
|
|
|
1365
|
|
|
1366 begin
|
|
|
1367 -- A generic package declaration carries contract-related source pragmas
|
|
|
1368 -- in its visible declarations.
|
|
|
1369
|
|
|
1370 if Nkind (Templ) = N_Generic_Package_Declaration then
|
|
|
1371 Set_Ekind (Templ_Id, E_Generic_Package);
|
|
|
1372
|
|
|
1373 if Present (Visible_Declarations (Specification (Templ))) then
|
|
|
1374 Decl := First (Visible_Declarations (Specification (Templ)));
|
|
|
1375 end if;
|
|
|
1376
|
|
|
1377 -- A generic package body carries contract-related source pragmas in its
|
|
|
1378 -- declarations.
|
|
|
1379
|
|
|
1380 elsif Nkind (Templ) = N_Package_Body then
|
|
|
1381 Set_Ekind (Templ_Id, E_Package_Body);
|
|
|
1382
|
|
|
1383 if Present (Declarations (Templ)) then
|
|
|
1384 Decl := First (Declarations (Templ));
|
|
|
1385 end if;
|
|
|
1386
|
|
|
1387 -- Generic subprogram declaration
|
|
|
1388
|
|
|
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;
|
|
|
1395
|
|
|
1396 -- When the generic subprogram acts as a compilation unit, inspect
|
|
|
1397 -- the Pragmas_After list for contract-related source pragmas.
|
|
|
1398
|
|
|
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;
|
|
|
1405
|
|
|
1406 -- Otherwise inspect the successive declarations for contract-related
|
|
|
1407 -- source pragmas.
|
|
|
1408
|
|
|
1409 else
|
|
|
1410 Decl := Next (Unit);
|
|
|
1411 end if;
|
|
|
1412
|
|
|
1413 -- A generic subprogram body carries contract-related source pragmas in
|
|
|
1414 -- its declarations.
|
|
|
1415
|
|
|
1416 elsif Nkind (Templ) = N_Subprogram_Body then
|
|
|
1417 Set_Ekind (Templ_Id, E_Subprogram_Body);
|
|
|
1418
|
|
|
1419 if Present (Declarations (Templ)) then
|
|
|
1420 Decl := First (Declarations (Templ));
|
|
|
1421 end if;
|
|
|
1422 end if;
|
|
|
1423
|
|
|
1424 -- Inspect the relevant declarations looking for contract-related source
|
|
|
1425 -- pragmas and add them to the contract of the generic unit.
|
|
|
1426
|
|
|
1427 while Present (Decl) loop
|
|
|
1428 if Comes_From_Source (Decl) then
|
|
|
1429 if Nkind (Decl) = N_Pragma then
|
|
|
1430
|
|
|
1431 -- The source pragma is a contract annotation
|
|
|
1432
|
|
|
1433 if Is_Contract_Annotation (Decl) then
|
|
|
1434 Add_Generic_Contract_Pragma (Decl);
|
|
|
1435 end if;
|
|
|
1436
|
|
|
1437 -- The region where a contract-related source pragma may appear
|
|
|
1438 -- ends with the first source non-pragma declaration or statement.
|
|
|
1439
|
|
|
1440 else
|
|
|
1441 exit;
|
|
|
1442 end if;
|
|
|
1443 end if;
|
|
|
1444
|
|
|
1445 Next (Decl);
|
|
|
1446 end loop;
|
|
|
1447 end Create_Generic_Contract;
|
|
|
1448
|
|
|
1449 --------------------------------
|
|
|
1450 -- Expand_Subprogram_Contract --
|
|
|
1451 --------------------------------
|
|
|
1452
|
|
|
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);
|
|
|
1456
|
|
|
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.
|
|
|
1466
|
|
|
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.
|
|
|
1471
|
|
|
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.
|
|
|
1480
|
|
|
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.
|
|
|
1484
|
|
|
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.
|
|
|
1488
|
|
|
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.
|
|
|
1492
|
|
|
1493 ----------------------------------------
|
|
|
1494 -- Add_Invariant_And_Predicate_Checks --
|
|
|
1495 ----------------------------------------
|
|
|
1496
|
|
|
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.
|
|
|
1512
|
|
|
1513 ---------------------------------
|
|
|
1514 -- Add_Invariant_Access_Checks --
|
|
|
1515 ---------------------------------
|
|
|
1516
|
|
|
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;
|
|
|
1521
|
|
|
1522 begin
|
|
|
1523 Typ := Etype (Id);
|
|
|
1524
|
|
|
1525 if Is_Access_Type (Typ) and then not Is_Access_Constant (Typ) then
|
|
|
1526 Typ := Designated_Type (Typ);
|
|
|
1527
|
|
|
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;
|
|
|
1550 end if;
|
|
|
1551 end Add_Invariant_Access_Checks;
|
|
|
1552
|
|
|
1553 -------------------------
|
|
|
1554 -- Invariant_Checks_OK --
|
|
|
1555 -------------------------
|
|
|
1556
|
|
|
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.
|
|
|
1561
|
|
|
1562 -----------------------------------------
|
|
|
1563 -- Has_Public_Visibility_Of_Subprogram --
|
|
|
1564 -----------------------------------------
|
|
|
1565
|
|
|
1566 function Has_Public_Visibility_Of_Subprogram return Boolean is
|
|
|
1567 Subp_Decl : constant Node_Id := Unit_Declaration_Node (Subp_Id);
|
|
|
1568
|
|
|
1569 begin
|
|
|
1570 -- An Initialization procedure must be considered visible even
|
|
|
1571 -- though it is internally generated.
|
|
|
1572
|
|
|
1573 if Is_Init_Proc (Defining_Entity (Subp_Decl)) then
|
|
|
1574 return True;
|
|
|
1575
|
|
|
1576 elsif Ekind (Scope (Typ)) /= E_Package then
|
|
|
1577 return False;
|
|
|
1578
|
|
|
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.
|
|
|
1583
|
|
|
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;
|
|
|
1591
|
|
|
1592 -- Determine whether the subprogram is declared in the visible
|
|
|
1593 -- declarations of the package containing the type, or in the
|
|
|
1594 -- visible declaration of a child unit of that package.
|
|
|
1595
|
|
|
1596 else
|
|
|
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;
|
|
|
1620 end if;
|
|
|
1621 end Has_Public_Visibility_Of_Subprogram;
|
|
|
1622
|
|
|
1623 -- Start of processing for Invariant_Checks_OK
|
|
|
1624
|
|
|
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;
|
|
|
1632
|
|
|
1633 -- Local variables
|
|
|
1634
|
|
|
1635 Loc : constant Source_Ptr := Sloc (Body_Decl);
|
|
|
1636 -- Source location of subprogram body contract
|
|
|
1637
|
|
|
1638 Formal : Entity_Id;
|
|
|
1639 Typ : Entity_Id;
|
|
|
1640
|
|
|
1641 -- Start of processing for Add_Invariant_And_Predicate_Checks
|
|
|
1642
|
|
|
1643 begin
|
|
|
1644 Result := Empty;
|
|
|
1645
|
|
|
1646 -- Process the result of a function
|
|
|
1647
|
|
|
1648 if Ekind (Subp_Id) = E_Function then
|
|
|
1649 Typ := Etype (Subp_Id);
|
|
|
1650
|
|
|
1651 -- Generate _Result which is used in procedure _Postconditions to
|
|
|
1652 -- verify the return value.
|
|
|
1653
|
|
|
1654 Result := Make_Defining_Identifier (Loc, Name_uResult);
|
|
|
1655 Set_Etype (Result, Typ);
|
|
|
1656
|
|
|
1657 -- Add an invariant check when the return type has invariants and
|
|
|
1658 -- the related function is visible to the outside.
|
|
|
1659
|
|
|
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;
|
|
|
1666
|
|
|
1667 -- Add an invariant check when the return type is an access to a
|
|
|
1668 -- type with invariants.
|
|
|
1669
|
|
|
1670 Add_Invariant_Access_Checks (Result);
|
|
|
1671 end if;
|
|
|
1672
|
|
|
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);
|
|
|
1687 end if;
|
|
|
1688
|
|
|
1689 Add_Invariant_Access_Checks (Formal);
|
|
|
1690
|
|
|
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.
|
|
|
1695
|
|
|
1696 end if;
|
|
|
1697
|
|
|
1698 Next_Formal (Formal);
|
|
|
1699 end loop;
|
|
|
1700 end Add_Invariant_And_Predicate_Checks;
|
|
|
1701
|
|
|
1702 -------------------------
|
|
|
1703 -- Append_Enabled_Item --
|
|
|
1704 -------------------------
|
|
|
1705
|
|
|
1706 procedure Append_Enabled_Item (Item : Node_Id; List : in out List_Id) is
|
|
|
1707 begin
|
|
|
1708 -- Do not chain ignored or disabled pragmas
|
|
|
1709
|
|
|
1710 if Nkind (Item) = N_Pragma
|
|
|
1711 and then (Is_Ignored (Item) or else Is_Disabled (Item))
|
|
|
1712 then
|
|
|
1713 null;
|
|
|
1714
|
|
|
1715 -- Otherwise, add the item
|
|
|
1716
|
|
|
1717 else
|
|
|
1718 if No (List) then
|
|
|
1719 List := New_List;
|
|
|
1720 end if;
|
|
|
1721
|
|
|
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.
|
|
|
1725
|
|
|
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;
|
|
|
1736
|
|
|
1737 ------------------------------------
|
|
|
1738 -- Build_Postconditions_Procedure --
|
|
|
1739 ------------------------------------
|
|
|
1740
|
|
|
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;
|
|
|
1758
|
|
|
1759 begin
|
|
|
1760 -- Inspect the declarations of the related subprogram body looking
|
|
|
1761 -- for the first source declaration.
|
|
|
1762
|
|
|
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;
|
|
|
1770
|
|
|
1771 Next (Decl);
|
|
|
1772 end loop;
|
|
|
1773
|
|
|
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.
|
|
|
1777
|
|
|
1778 Append (Stmt, Decls);
|
|
|
1779
|
|
|
1780 -- Ensure that the body has a declaration list
|
|
|
1781
|
|
|
1782 else
|
|
|
1783 Set_Declarations (Body_Decl, New_List (Stmt));
|
|
|
1784 end if;
|
|
|
1785 end Insert_Before_First_Source_Declaration;
|
|
|
1786
|
|
|
1787 -- Local variables
|
|
|
1788
|
|
|
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;
|
|
|
1795
|
|
|
1796 -- Start of processing for Build_Postconditions_Procedure
|
|
|
1797
|
|
|
1798 begin
|
|
|
1799 -- Nothing to do if there are no actions to check on exit
|
|
|
1800
|
|
|
1801 if No (Stmts) then
|
|
|
1802 return;
|
|
|
1803 end if;
|
|
|
1804
|
|
|
1805 Proc_Id := Make_Defining_Identifier (Loc, Name_uPostconditions);
|
|
|
1806 Set_Debug_Info_Needed (Proc_Id);
|
|
|
1807 Set_Postconditions_Proc (Subp_Id, Proc_Id);
|
|
|
1808
|
|
|
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.
|
|
|
1813
|
|
|
1814 if Modify_Tree_For_C then
|
|
|
1815 Set_Has_Pragma_Inline (Proc_Id);
|
|
|
1816 Set_Has_Pragma_Inline_Always (Proc_Id);
|
|
|
1817 Set_Is_Inlined (Proc_Id);
|
|
|
1818 end if;
|
|
|
1819
|
|
|
1820 -- The related subprogram is a function: create the specification of
|
|
|
1821 -- parameter _Result.
|
|
|
1822
|
|
|
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;
|
|
|
1830
|
|
|
1831 Proc_Spec :=
|
|
|
1832 Make_Procedure_Specification (Loc,
|
|
|
1833 Defining_Unit_Name => Proc_Id,
|
|
|
1834 Parameter_Specifications => Params);
|
|
|
1835
|
|
|
1836 Proc_Decl := Make_Subprogram_Declaration (Loc, Proc_Spec);
|
|
|
1837
|
|
|
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:
|
|
|
1841
|
|
|
1842 -- procedure Proc (Obj : Array_Typ) is
|
|
|
1843 -- procedure _postconditions is
|
|
|
1844 -- begin
|
|
|
1845 -- ... Obj ...
|
|
|
1846 -- end _postconditions;
|
|
|
1847
|
|
|
1848 -- subtype T is Array_Typ (Obj'First (1) .. Obj'Last (1));
|
|
|
1849 -- begin
|
|
|
1850
|
|
|
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.
|
|
|
1855
|
|
|
1856 Insert_Before_First_Source_Declaration (Proc_Decl);
|
|
|
1857 Analyze (Proc_Decl);
|
|
|
1858
|
|
|
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
|
|
131
|
1897 if Pragma_Name (Prag) = Name_Contract_Cases
|
|
|
1898 and then Is_Checked (Prag)
|
|
|
1899 then
|
|
111
|
1900 Expand_Pragma_Contract_Cases
|
|
|
1901 (CCs => Prag,
|
|
|
1902 Subp_Id => Subp_Id,
|
|
|
1903 Decls => Declarations (Body_Decl),
|
|
|
1904 Stmts => Stmts);
|
|
|
1905 end if;
|
|
|
1906
|
|
|
1907 Prag := Next_Pragma (Prag);
|
|
|
1908 end loop;
|
|
|
1909 end if;
|
|
|
1910 end Process_Contract_Cases_For;
|
|
|
1911
|
|
131
|
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
|
|
111
|
1917 -- Start of processing for Process_Contract_Cases
|
|
|
1918
|
|
|
1919 begin
|
|
|
1920 Process_Contract_Cases_For (Body_Id);
|
|
|
1921
|
|
|
1922 if Present (Spec_Id) then
|
|
|
1923 Process_Contract_Cases_For (Spec_Id);
|
|
|
1924 end if;
|
|
|
1925 end Process_Contract_Cases;
|
|
|
1926
|
|
|
1927 ----------------------------
|
|
|
1928 -- Process_Postconditions --
|
|
|
1929 ----------------------------
|
|
|
1930
|
|
|
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.
|
|
|
1936
|
|
|
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);
|
|
|
1948 Decl : Node_Id;
|
|
|
1949 Prag : Node_Id;
|
|
|
1950
|
|
|
1951 begin
|
|
|
1952 -- Process the contract
|
|
|
1953
|
|
|
1954 if Present (Items) then
|
|
|
1955 Prag := Pre_Post_Conditions (Items);
|
|
|
1956 while Present (Prag) loop
|
|
131
|
1957 if Pragma_Name (Prag) = Post_Nam
|
|
|
1958 and then Is_Checked (Prag)
|
|
|
1959 then
|
|
111
|
1960 Append_Enabled_Item
|
|
|
1961 (Item => Build_Pragma_Check_Equivalent (Prag),
|
|
|
1962 List => Stmts);
|
|
|
1963 end if;
|
|
|
1964
|
|
|
1965 Prag := Next_Pragma (Prag);
|
|
|
1966 end loop;
|
|
|
1967 end if;
|
|
|
1968
|
|
|
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.
|
|
|
1973
|
|
|
1974 if Present (Spec_Id) and then Nkind (Unit_Decl) = N_Subunit then
|
|
|
1975 Decl := Next (Corresponding_Stub (Unit_Decl));
|
|
|
1976 while Present (Decl) loop
|
|
|
1977
|
|
|
1978 -- Note that non-matching pragmas are skipped
|
|
|
1979
|
|
|
1980 if Nkind (Decl) = N_Pragma then
|
|
131
|
1981 if Pragma_Name (Decl) = Post_Nam
|
|
|
1982 and then Is_Checked (Decl)
|
|
|
1983 then
|
|
111
|
1984 Append_Enabled_Item
|
|
|
1985 (Item => Build_Pragma_Check_Equivalent (Decl),
|
|
|
1986 List => Stmts);
|
|
|
1987 end if;
|
|
|
1988
|
|
|
1989 -- Skip internally generated code
|
|
|
1990
|
|
|
1991 elsif not Comes_From_Source (Decl) then
|
|
|
1992 null;
|
|
|
1993
|
|
|
1994 -- Postcondition pragmas are usually grouped together. There
|
|
|
1995 -- is no need to inspect the whole declarative list.
|
|
|
1996
|
|
|
1997 else
|
|
|
1998 exit;
|
|
|
1999 end if;
|
|
|
2000
|
|
|
2001 Next (Decl);
|
|
|
2002 end loop;
|
|
|
2003 end if;
|
|
|
2004 end Process_Body_Postconditions;
|
|
|
2005
|
|
|
2006 ---------------------------------
|
|
|
2007 -- Process_Spec_Postconditions --
|
|
|
2008 ---------------------------------
|
|
|
2009
|
|
|
2010 procedure Process_Spec_Postconditions is
|
|
|
2011 Subps : constant Subprogram_List :=
|
|
|
2012 Inherited_Subprograms (Spec_Id);
|
|
131
|
2013 Item : Node_Id;
|
|
111
|
2014 Items : Node_Id;
|
|
|
2015 Prag : Node_Id;
|
|
|
2016 Subp_Id : Entity_Id;
|
|
|
2017
|
|
|
2018 begin
|
|
|
2019 -- Process the contract
|
|
|
2020
|
|
|
2021 Items := Contract (Spec_Id);
|
|
|
2022
|
|
|
2023 if Present (Items) then
|
|
|
2024 Prag := Pre_Post_Conditions (Items);
|
|
|
2025 while Present (Prag) loop
|
|
131
|
2026 if Pragma_Name (Prag) = Name_Postcondition
|
|
|
2027 and then Is_Checked (Prag)
|
|
|
2028 then
|
|
111
|
2029 Append_Enabled_Item
|
|
|
2030 (Item => Build_Pragma_Check_Equivalent (Prag),
|
|
|
2031 List => Stmts);
|
|
|
2032 end if;
|
|
|
2033
|
|
|
2034 Prag := Next_Pragma (Prag);
|
|
|
2035 end loop;
|
|
|
2036 end if;
|
|
|
2037
|
|
|
2038 -- Process the contracts of all inherited subprograms, looking for
|
|
|
2039 -- class-wide postconditions.
|
|
|
2040
|
|
|
2041 for Index in Subps'Range loop
|
|
|
2042 Subp_Id := Subps (Index);
|
|
|
2043 Items := Contract (Subp_Id);
|
|
|
2044
|
|
|
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
|
|
131
|
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;
|
|
111
|
2065 end if;
|
|
|
2066
|
|
|
2067 Prag := Next_Pragma (Prag);
|
|
|
2068 end loop;
|
|
|
2069 end if;
|
|
|
2070 end loop;
|
|
|
2071 end Process_Spec_Postconditions;
|
|
|
2072
|
|
131
|
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
|
|
111
|
2078 -- Start of processing for Process_Postconditions
|
|
|
2079
|
|
|
2080 begin
|
|
|
2081 -- The processing of postconditions is done in reverse order (body
|
|
|
2082 -- first) to ensure the following arrangement:
|
|
|
2083
|
|
|
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);
|
|
|
2091
|
|
|
2092 if Present (Spec_Id) then
|
|
|
2093 Process_Spec_Postconditions;
|
|
|
2094 end if;
|
|
|
2095 end Process_Postconditions;
|
|
|
2096
|
|
|
2097 ---------------------------
|
|
|
2098 -- Process_Preconditions --
|
|
|
2099 ---------------------------
|
|
|
2100
|
|
|
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.
|
|
|
2105
|
|
|
2106 Insert_Node : Node_Id := Empty;
|
|
|
2107 -- The insertion node after which all pragma Check equivalents are
|
|
|
2108 -- inserted.
|
|
|
2109
|
|
|
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.
|
|
|
2113
|
|
|
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.
|
|
|
2118
|
|
|
2119 procedure Prepend_To_Decls (Item : Node_Id);
|
|
|
2120 -- Prepend a single item to the declarations of the subprogram body
|
|
|
2121
|
|
|
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.
|
|
|
2125
|
|
|
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.
|
|
|
2129
|
|
|
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.
|
|
|
2133
|
|
|
2134 --------------------------
|
|
|
2135 -- Is_Prologue_Renaming --
|
|
|
2136 --------------------------
|
|
|
2137
|
|
|
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;
|
|
|
2143
|
|
|
2144 begin
|
|
|
2145 if Nkind (Decl) = N_Object_Renaming_Declaration then
|
|
|
2146 Obj := Defining_Entity (Decl);
|
|
|
2147 Nam := Name (Decl);
|
|
|
2148
|
|
|
2149 if Nkind (Nam) = N_Selected_Component then
|
|
|
2150 Pref := Prefix (Nam);
|
|
|
2151 Sel := Selector_Name (Nam);
|
|
|
2152
|
|
|
2153 -- A discriminant renaming appears as
|
|
|
2154 -- Discr : constant ... := Prefix.Discr;
|
|
|
2155
|
|
|
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;
|
|
|
2162
|
|
|
2163 -- A protection field renaming appears as
|
|
|
2164 -- Prot : ... := _object._object;
|
|
|
2165
|
|
|
2166 -- A renamed private component is just a component of
|
|
|
2167 -- _object, with an arbitrary name.
|
|
|
2168
|
|
|
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;
|
|
|
2178
|
|
|
2179 return False;
|
|
|
2180 end Is_Prologue_Renaming;
|
|
|
2181
|
|
|
2182 -------------------------
|
|
|
2183 -- Merge_Preconditions --
|
|
|
2184 -------------------------
|
|
|
2185
|
|
|
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.
|
|
|
2190
|
|
|
2191 function Message_Arg (Prag : Node_Id) return Node_Id;
|
|
|
2192 -- Return the message argument of a precondition
|
|
|
2193
|
|
|
2194 --------------------
|
|
|
2195 -- Expression_Arg --
|
|
|
2196 --------------------
|
|
|
2197
|
|
|
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)));
|
|
|
2201
|
|
|
2202 begin
|
|
|
2203 if Paren_Count (Arg) = 0 then
|
|
|
2204 Set_Paren_Count (Arg, 1);
|
|
|
2205 end if;
|
|
|
2206
|
|
|
2207 return Arg;
|
|
|
2208 end Expression_Arg;
|
|
|
2209
|
|
|
2210 -----------------
|
|
|
2211 -- Message_Arg --
|
|
|
2212 -----------------
|
|
|
2213
|
|
|
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;
|
|
|
2219
|
|
|
2220 -- Local variables
|
|
|
2221
|
|
|
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);
|
|
|
2227
|
|
|
2228 -- Start of processing for Merge_Preconditions
|
|
|
2229
|
|
|
2230 begin
|
|
|
2231 -- Merge the two preconditions by "or else"-ing them
|
|
|
2232
|
|
|
2233 Rewrite (Into_Expr,
|
|
|
2234 Make_Or_Else (Loc,
|
|
|
2235 Right_Opnd => Relocate_Node (Into_Expr),
|
|
|
2236 Left_Opnd => From_Expr));
|
|
|
2237
|
|
|
2238 -- Merge the two error messages to produce a single message of the
|
|
|
2239 -- form:
|
|
|
2240
|
|
|
2241 -- failed precondition from ...
|
|
|
2242 -- also failed inherited precondition from ...
|
|
|
2243
|
|
|
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));
|
|
|
2249
|
|
|
2250 Set_Strval (Into_Msg, End_String);
|
|
|
2251 end if;
|
|
|
2252 end Merge_Preconditions;
|
|
|
2253
|
|
|
2254 ----------------------
|
|
|
2255 -- Prepend_To_Decls --
|
|
|
2256 ----------------------
|
|
|
2257
|
|
|
2258 procedure Prepend_To_Decls (Item : Node_Id) is
|
|
131
|
2259 Decls : List_Id;
|
|
111
|
2260
|
|
|
2261 begin
|
|
131
|
2262 Decls := Declarations (Body_Decl);
|
|
|
2263
|
|
111
|
2264 -- Ensure that the body has a declarative list
|
|
|
2265
|
|
|
2266 if No (Decls) then
|
|
|
2267 Decls := New_List;
|
|
|
2268 Set_Declarations (Body_Decl, Decls);
|
|
|
2269 end if;
|
|
|
2270
|
|
|
2271 Prepend_To (Decls, Item);
|
|
|
2272 end Prepend_To_Decls;
|
|
|
2273
|
|
|
2274 ------------------------------
|
|
|
2275 -- Prepend_To_Decls_Or_Save --
|
|
|
2276 ------------------------------
|
|
|
2277
|
|
|
2278 procedure Prepend_To_Decls_Or_Save (Prag : Node_Id) is
|
|
|
2279 Check_Prag : Node_Id;
|
|
|
2280
|
|
|
2281 begin
|
|
|
2282 Check_Prag := Build_Pragma_Check_Equivalent (Prag);
|
|
|
2283
|
|
|
2284 -- Save the sole class-wide precondition (if any) for the next
|
|
|
2285 -- step, where it will be merged with inherited preconditions.
|
|
|
2286
|
|
|
2287 if Class_Present (Prag) then
|
|
|
2288 pragma Assert (No (Class_Pre));
|
|
|
2289 Class_Pre := Check_Prag;
|
|
|
2290
|
|
|
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.
|
|
|
2294
|
|
|
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;
|
|
|
2301
|
|
|
2302 Analyze (Check_Prag);
|
|
|
2303 end if;
|
|
|
2304 end Prepend_To_Decls_Or_Save;
|
|
|
2305
|
|
|
2306 -------------------------------------
|
|
|
2307 -- Process_Inherited_Preconditions --
|
|
|
2308 -------------------------------------
|
|
|
2309
|
|
|
2310 procedure Process_Inherited_Preconditions is
|
|
131
|
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;
|
|
111
|
2318
|
|
|
2319 begin
|
|
|
2320 -- Process the contracts of all inherited subprograms, looking for
|
|
|
2321 -- class-wide preconditions.
|
|
|
2322
|
|
|
2323 for Index in Subps'Range loop
|
|
|
2324 Subp_Id := Subps (Index);
|
|
|
2325 Items := Contract (Subp_Id);
|
|
|
2326
|
|
|
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
|
|
131
|
2333 Item :=
|
|
111
|
2334 Build_Pragma_Check_Equivalent
|
|
|
2335 (Prag => Prag,
|
|
|
2336 Subp_Id => Spec_Id,
|
|
|
2337 Inher_Id => Subp_Id);
|
|
|
2338
|
|
131
|
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.
|
|
|
2343
|
|
|
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;
|
|
111
|
2356 end if;
|
|
|
2357 end if;
|
|
|
2358
|
|
|
2359 Prag := Next_Pragma (Prag);
|
|
|
2360 end loop;
|
|
|
2361 end if;
|
|
|
2362 end loop;
|
|
|
2363
|
|
|
2364 -- Add the merged class-wide preconditions
|
|
|
2365
|
|
|
2366 if Present (Class_Pre) then
|
|
|
2367 Prepend_To_Decls (Class_Pre);
|
|
|
2368 Analyze (Class_Pre);
|
|
|
2369 end if;
|
|
|
2370 end Process_Inherited_Preconditions;
|
|
|
2371
|
|
|
2372 -------------------------------
|
|
|
2373 -- Process_Preconditions_For --
|
|
|
2374 -------------------------------
|
|
|
2375
|
|
|
2376 procedure Process_Preconditions_For (Subp_Id : Entity_Id) is
|
|
|
2377 Items : constant Node_Id := Contract (Subp_Id);
|
|
131
|
2378 Subp_Decl : constant Node_Id := Unit_Declaration_Node (Subp_Id);
|
|
111
|
2379 Decl : Node_Id;
|
|
131
|
2380 Freeze_T : Boolean;
|
|
111
|
2381 Prag : Node_Id;
|
|
|
2382
|
|
|
2383 begin
|
|
131
|
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
|
|
|
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;
|
|
111
|
2397
|
|
|
2398 if Present (Items) then
|
|
|
2399 Prag := Pre_Post_Conditions (Items);
|
|
|
2400 while Present (Prag) loop
|
|
131
|
2401 if Pragma_Name (Prag) = Name_Precondition
|
|
|
2402 and then Is_Checked (Prag)
|
|
|
2403 then
|
|
|
2404 if Freeze_T
|
|
|
2405 and then Present (Corresponding_Aspect (Prag))
|
|
|
2406 then
|
|
|
2407 Freeze_Expr_Types
|
|
|
2408 (Def_Id => Subp_Id,
|
|
|
2409 Typ => Standard_Boolean,
|
|
|
2410 Expr => Expression (Corresponding_Aspect (Prag)),
|
|
|
2411 N => Body_Decl);
|
|
|
2412 end if;
|
|
|
2413
|
|
111
|
2414 Prepend_To_Decls_Or_Save (Prag);
|
|
|
2415 end if;
|
|
|
2416
|
|
|
2417 Prag := Next_Pragma (Prag);
|
|
|
2418 end loop;
|
|
|
2419 end if;
|
|
|
2420
|
|
|
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.
|
|
|
2425
|
|
|
2426 if Nkind (Subp_Decl) = N_Subprogram_Body_Stub then
|
|
|
2427
|
|
|
2428 -- Inspect the declarations following the body stub
|
|
|
2429
|
|
|
2430 Decl := Next (Subp_Decl);
|
|
|
2431 while Present (Decl) loop
|
|
|
2432
|
|
|
2433 -- Note that non-matching pragmas are skipped
|
|
|
2434
|
|
|
2435 if Nkind (Decl) = N_Pragma then
|
|
131
|
2436 if Pragma_Name (Decl) = Name_Precondition
|
|
|
2437 and then Is_Checked (Decl)
|
|
|
2438 then
|
|
111
|
2439 Prepend_To_Decls_Or_Save (Decl);
|
|
|
2440 end if;
|
|
|
2441
|
|
|
2442 -- Skip internally generated code
|
|
|
2443
|
|
|
2444 elsif not Comes_From_Source (Decl) then
|
|
|
2445 null;
|
|
|
2446
|
|
|
2447 -- Preconditions are usually grouped together. There is no
|
|
|
2448 -- need to inspect the whole declarative list.
|
|
|
2449
|
|
|
2450 else
|
|
|
2451 exit;
|
|
|
2452 end if;
|
|
|
2453
|
|
|
2454 Next (Decl);
|
|
|
2455 end loop;
|
|
|
2456 end if;
|
|
|
2457 end Process_Preconditions_For;
|
|
|
2458
|
|
|
2459 -- Local variables
|
|
|
2460
|
|
|
2461 Decls : constant List_Id := Declarations (Body_Decl);
|
|
|
2462 Decl : Node_Id;
|
|
|
2463
|
|
|
2464 -- Start of processing for Process_Preconditions
|
|
|
2465
|
|
|
2466 begin
|
|
|
2467 -- Find the proper insertion point for all pragma Check equivalents
|
|
|
2468
|
|
|
2469 if Present (Decls) then
|
|
|
2470 Decl := First (Decls);
|
|
|
2471 while Present (Decl) loop
|
|
|
2472
|
|
|
2473 -- First source declaration terminates the search, because all
|
|
|
2474 -- preconditions must be evaluated prior to it, by definition.
|
|
|
2475
|
|
|
2476 if Comes_From_Source (Decl) then
|
|
|
2477 exit;
|
|
|
2478
|
|
|
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.
|
|
|
2484
|
|
|
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;
|
|
|
2491
|
|
|
2492 Insert_Node := Decl;
|
|
|
2493
|
|
|
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.
|
|
|
2497
|
|
|
2498 else
|
|
|
2499 exit;
|
|
|
2500 end if;
|
|
|
2501
|
|
|
2502 Next (Decl);
|
|
|
2503 end loop;
|
|
|
2504 end if;
|
|
|
2505
|
|
|
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:
|
|
|
2510
|
|
|
2511 -- <inherited preconditions>
|
|
|
2512 -- <preconditions from spec>
|
|
|
2513 -- <preconditions from body>
|
|
|
2514
|
|
|
2515 Process_Preconditions_For (Body_Id);
|
|
|
2516
|
|
|
2517 if Present (Spec_Id) then
|
|
|
2518 Process_Preconditions_For (Spec_Id);
|
|
|
2519 Process_Inherited_Preconditions;
|
|
|
2520 end if;
|
|
|
2521 end Process_Preconditions;
|
|
|
2522
|
|
|
2523 -- Local variables
|
|
|
2524
|
|
|
2525 Restore_Scope : Boolean := False;
|
|
|
2526 Result : Entity_Id;
|
|
|
2527 Stmts : List_Id := No_List;
|
|
|
2528 Subp_Id : Entity_Id;
|
|
|
2529
|
|
|
2530 -- Start of processing for Expand_Subprogram_Contract
|
|
|
2531
|
|
|
2532 begin
|
|
|
2533 -- Obtain the entity of the initial declaration
|
|
|
2534
|
|
|
2535 if Present (Spec_Id) then
|
|
|
2536 Subp_Id := Spec_Id;
|
|
|
2537 else
|
|
|
2538 Subp_Id := Body_Id;
|
|
|
2539 end if;
|
|
|
2540
|
|
|
2541 -- Do not perform expansion activity when it is not needed
|
|
|
2542
|
|
|
2543 if not Expander_Active then
|
|
|
2544 return;
|
|
|
2545
|
|
|
2546 -- ASIS requires an unaltered tree
|
|
|
2547
|
|
|
2548 elsif ASIS_Mode then
|
|
|
2549 return;
|
|
|
2550
|
|
|
2551 -- GNATprove does not need the executable semantics of a contract
|
|
|
2552
|
|
|
2553 elsif GNATprove_Mode then
|
|
|
2554 return;
|
|
|
2555
|
|
|
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.
|
|
|
2559
|
|
|
2560 elsif Is_Generic_Subprogram (Subp_Id) or else Inside_A_Generic then
|
|
|
2561 return;
|
|
|
2562
|
|
|
2563 -- All subprograms carry a contract, but for some it is not significant
|
|
|
2564 -- and should not be processed. This is a small optimization.
|
|
|
2565
|
|
|
2566 elsif not Has_Significant_Contract (Subp_Id) then
|
|
|
2567 return;
|
|
|
2568
|
|
|
2569 -- The contract of an ignored Ghost subprogram does not need expansion,
|
|
|
2570 -- because the subprogram and all calls to it will be removed.
|
|
|
2571
|
|
|
2572 elsif Is_Ignored_Ghost_Entity (Subp_Id) then
|
|
|
2573 return;
|
|
|
2574
|
|
|
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).
|
|
|
2578
|
|
131
|
2579 elsif Has_Expanded_Contract (Subp_Id) then
|
|
111
|
2580 return;
|
|
|
2581 end if;
|
|
|
2582
|
|
131
|
2583 -- Prevent multiple expansion attempts of the same contract
|
|
|
2584
|
|
|
2585 Set_Has_Expanded_Contract (Subp_Id);
|
|
|
2586
|
|
111
|
2587 -- Ensure that the formal parameters are visible when expanding all
|
|
|
2588 -- contract items.
|
|
|
2589
|
|
|
2590 if not In_Open_Scopes (Subp_Id) then
|
|
|
2591 Restore_Scope := True;
|
|
|
2592 Push_Scope (Subp_Id);
|
|
|
2593
|
|
|
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;
|
|
|
2600
|
|
|
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:
|
|
|
2604
|
|
|
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;
|
|
|
2616
|
|
|
2617 -- <inherited preconditions>
|
|
|
2618 -- <preconditions from spec>
|
|
|
2619 -- <preconditions from body>
|
|
|
2620 -- <contract case conditions>
|
|
|
2621
|
|
|
2622 -- <source declarations>
|
|
|
2623 -- begin
|
|
|
2624 -- <source statements>
|
|
|
2625
|
|
|
2626 -- _Preconditions (Result);
|
|
|
2627 -- return Result;
|
|
|
2628 -- end Example;
|
|
|
2629
|
|
|
2630 -- Routine _Postconditions holds all contract assertions that must be
|
|
|
2631 -- verified on exit from the related subprogram.
|
|
|
2632
|
|
|
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.
|
|
|
2636
|
|
|
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.
|
|
|
2642
|
|
|
2643 Process_Postconditions (Stmts);
|
|
|
2644
|
|
|
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.
|
|
|
2648
|
|
|
2649 Process_Contract_Cases (Stmts);
|
|
|
2650
|
|
|
2651 -- Step 4: Apply invariant and predicate checks on a function result and
|
|
|
2652 -- all formals. The resulting checks are accumulated in list Stmts.
|
|
|
2653
|
|
|
2654 Add_Invariant_And_Predicate_Checks (Subp_Id, Stmts, Result);
|
|
|
2655
|
|
|
2656 -- Step 5: Construct procedure _Postconditions
|
|
|
2657
|
|
|
2658 Build_Postconditions_Procedure (Subp_Id, Stmts, Result);
|
|
|
2659
|
|
|
2660 if Restore_Scope then
|
|
|
2661 End_Scope;
|
|
|
2662 end if;
|
|
|
2663 end Expand_Subprogram_Contract;
|
|
|
2664
|
|
131
|
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
|
|
111
|
2846 ---------------------------------
|
|
|
2847 -- Inherit_Subprogram_Contract --
|
|
|
2848 ---------------------------------
|
|
|
2849
|
|
|
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.
|
|
|
2857
|
|
|
2858 --------------------
|
|
|
2859 -- Inherit_Pragma --
|
|
|
2860 --------------------
|
|
|
2861
|
|
|
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;
|
|
|
2865
|
|
|
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.
|
|
|
2870
|
|
|
2871 if Present (Prag) then
|
|
|
2872 New_Prag := New_Copy_Tree (Prag);
|
|
|
2873 Set_Is_Inherited_Pragma (New_Prag);
|
|
|
2874
|
|
|
2875 Add_Contract_Item (New_Prag, Subp);
|
|
|
2876 end if;
|
|
|
2877 end Inherit_Pragma;
|
|
|
2878
|
|
|
2879 -- Start of processing for Inherit_Subprogram_Contract
|
|
|
2880
|
|
|
2881 begin
|
|
|
2882 -- Inheritance is carried out only when both entities are subprograms
|
|
|
2883 -- with contracts.
|
|
|
2884
|
|
|
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;
|
|
|
2892
|
|
|
2893 -------------------------------------
|
|
|
2894 -- Instantiate_Subprogram_Contract --
|
|
|
2895 -------------------------------------
|
|
|
2896
|
|
|
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.
|
|
|
2902
|
|
|
2903 -------------------------
|
|
|
2904 -- Instantiate_Pragmas --
|
|
|
2905 -------------------------
|
|
|
2906
|
|
|
2907 procedure Instantiate_Pragmas (First_Prag : Node_Id) is
|
|
|
2908 Inst_Prag : Node_Id;
|
|
|
2909 Prag : Node_Id;
|
|
|
2910
|
|
|
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);
|
|
|
2917
|
|
|
2918 Set_Analyzed (Inst_Prag, False);
|
|
|
2919 Append_To (L, Inst_Prag);
|
|
|
2920 end if;
|
|
|
2921
|
|
|
2922 Prag := Next_Pragma (Prag);
|
|
|
2923 end loop;
|
|
|
2924 end Instantiate_Pragmas;
|
|
|
2925
|
|
|
2926 -- Local variables
|
|
|
2927
|
|
|
2928 Items : constant Node_Id := Contract (Defining_Entity (Templ));
|
|
|
2929
|
|
|
2930 -- Start of processing for Instantiate_Subprogram_Contract
|
|
|
2931
|
|
|
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;
|
|
|
2939
|
|
|
2940 ----------------------------------------
|
|
|
2941 -- Save_Global_References_In_Contract --
|
|
|
2942 ----------------------------------------
|
|
|
2943
|
|
|
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.
|
|
|
2951
|
|
|
2952 ------------------------------------
|
|
|
2953 -- Save_Global_References_In_List --
|
|
|
2954 ------------------------------------
|
|
|
2955
|
|
|
2956 procedure Save_Global_References_In_List (First_Prag : Node_Id) is
|
|
|
2957 Prag : Node_Id;
|
|
|
2958
|
|
|
2959 begin
|
|
|
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;
|
|
|
2969
|
|
|
2970 -- Local variables
|
|
|
2971
|
|
|
2972 Items : constant Node_Id := Contract (Defining_Entity (Templ));
|
|
|
2973
|
|
|
2974 -- Start of processing for Save_Global_References_In_Contract
|
|
|
2975
|
|
|
2976 begin
|
|
|
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;
|
|
|
2996
|
|
|
2997 end Contracts;
|
