aboutsummaryrefslogtreecommitdiff
path: root/gcc/ada/contracts.adb
diff options
context:
space:
mode:
authorPiotr Trojanek <trojanek@adacore.com>2023-03-29 10:03:29 +0200
committerMarc Poulhiès <poulhies@adacore.com>2023-05-29 10:23:17 +0200
commit1b19e6abc715c60506efff6bd5c705e727e0e373 (patch)
treed862021a896569da76c9d6595d5fcbd016e771e9 /gcc/ada/contracts.adb
parente9fd9efc8d64f944cb480322ee5ed2d0a46db87d (diff)
downloadgcc-1b19e6abc715c60506efff6bd5c705e727e0e373.zip
gcc-1b19e6abc715c60506efff6bd5c705e727e0e373.tar.gz
gcc-1b19e6abc715c60506efff6bd5c705e727e0e373.tar.bz2
ada: Analyze pre/post on access-to-subprogram without a wrapper
Aspects Pre/Post attached to an access-to-subprogram type were relocated to a spec of a wrapper subprogram and analyzed there; the body of the wrapper was only created with expansion enabled. However, there were several problems with this approach. When switch -gnat2022 was missing, we didn't relocate the Pre/Post aspects to wrapper and complained that their placement is incorrect (because we wrongly assumed that relocation is unconditional). Now we gently inform, that these aspects are Ada 2022 features that require -gnat20222 switch. When switch -gnata was missing, we entirely bypassed analysis of the Pre/Post aspects on access-to-subprogram. This was unlike for Pre/Post aspects on subprograms, which are checked for legality regardless of the -gnata switch. Finally, in the GNATprove backend we were picking the Pre/Post contract on an access-to-subprogram type from the wrapper, which was awkward as otherwise we had to ignore the wrapper specs and special-case for their missing bodies. In general, it is cleaner for GNATprove to extract the aspect expressions from where they originally appear and not from various expansion artifacts like access-to-subprogram wrappers (but the same applies to predication functions, type invariant procedures and default initialization procedures). Now we analyze the Pre/Post aspects on the types where they are originally attached, regardless of the -gnata switch. Once we adapt GNATprove to pick the aspect expression from there, we will stop creating the wrapper spec when expansion is disabled. gcc/ada/ * contracts.adb (Add_Pre_Post_Condition): Adapt to handle pre/post of an access-to-subprogram type. (Analyze_Type_Contract): Analyze pre/post of an access-to-subprogram. * contracts.ads (Analyze_Type_Contract): Adapt comment. * sem_ch3.adb (Build_Access_Subprogram_Wrapper): Copy pre/post aspects to wrapper spec and keep it on the type. * sem_prag.adb (Analyze_Pre_Post_Condition): Expect pre/post aspects on access-to-subprogram and complain if they appear without -gnat2022 switch. (Analyze_Pre_Post_Condition_In_Decl_Part): Adapt to handle pre/post on an access-to-subprogram type entity. * sem_attr.adb (Analyze_Attribute_Old_Result): Likewise. (Result): Likewise.
Diffstat (limited to 'gcc/ada/contracts.adb')
-rw-r--r--gcc/ada/contracts.adb20
1 files changed, 18 insertions, 2 deletions
diff --git a/gcc/ada/contracts.adb b/gcc/ada/contracts.adb
index d3ceaa9..012ea33 100644
--- a/gcc/ada/contracts.adb
+++ b/gcc/ada/contracts.adb
@@ -311,10 +311,13 @@ package body Contracts is
-- The four volatility refinement pragmas are ok for all types.
-- Part_Of is ok for task types and protected types.
-- Depends and Global are ok for task types.
+ --
+ -- Precondition and Postcondition are added separately; they are allowed
+ -- for access-to-subprogram types.
elsif Is_Type (Id) then
declare
- Is_OK : constant Boolean :=
+ Is_OK_Classification : constant Boolean :=
Prag_Nam in Name_Async_Readers
| Name_Async_Writers
| Name_Effective_Reads
@@ -326,9 +329,16 @@ package body Contracts is
| Name_Global)
or else (Ekind (Id) = E_Protected_Type
and Prag_Nam = Name_Part_Of);
+
begin
- if Is_OK then
+ if Is_OK_Classification then
Add_Classification;
+
+ elsif Ekind (Id) in Access_Subprogram_Kind
+ and then Prag_Nam in Name_Precondition
+ | Name_Postcondition
+ then
+ Add_Pre_Post_Condition;
else
-- The pragma is not a proper contract item
@@ -1580,6 +1590,12 @@ package body Contracts is
begin
Check_Type_Or_Object_External_Properties
(Type_Or_Obj_Id => Type_Id);
+
+ -- Analyze Pre/Post on access-to-subprogram type
+
+ if Is_Access_Subprogram_Type (Type_Id) then
+ Analyze_Entry_Or_Subprogram_Contract (Type_Id);
+ end if;
end Analyze_Type_Contract;
---------------------------------------