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.

5 files changed, 54 insertions, 18 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;
 
    ---------------------------------------
diff --git a/gcc/ada/contracts.ads b/gcc/ada/contracts.ads
index 0625b9f..d52e1aa 100644
--- a/gcc/ada/contracts.ads
+++ b/gcc/ada/contracts.ads
@@ -139,6 +139,8 @@ package Contracts is
    --    Async_Writers
    --    Effective_Reads
    --    Effective_Writes
+   --    Postcondition
+   --    Precondition
    --
    --  In the case of a protected or task type, there will also be
    --  a call to Analyze_Protected_Contract or Analyze_Task_Contract.
diff --git a/gcc/ada/sem_attr.adb b/gcc/ada/sem_attr.adb
index 8257d4b..f5ee275 100644
--- a/gcc/ada/sem_attr.adb
+++ b/gcc/ada/sem_attr.adb
@@ -1513,6 +1513,7 @@ package body Sem_Attr is
          elsif Nkind (Subp_Decl) not in N_Abstract_Subprogram_Declaration
                                       | N_Entry_Declaration
                                       | N_Expression_Function
+                                      | N_Full_Type_Declaration
                                       | N_Generic_Subprogram_Declaration
                                       | N_Subprogram_Body
                                       | N_Subprogram_Body_Stub
@@ -6009,6 +6010,18 @@ package body Sem_Attr is
                        ("incorrect prefix for attribute %, expected %", P);
                   end if;
 
+               --  If the prefix is an access-to-subprogram type, then it must
+               --  be the same as the annotated type.
+
+               elsif Is_Access_Subprogram_Type (Pref_Id) then
+                  if Pref_Id = Spec_Id then
+                     Set_Etype (N, Etype (Designated_Type (Spec_Id)));
+                  else
+                     Error_Msg_Name_2 := Chars (Spec_Id);
+                     Error_Attr
+                       ("incorrect prefix for attribute %, expected %", P);
+                  end if;
+
                --  Otherwise the prefix denotes some other form of subprogram
                --  entity.
 
diff --git a/gcc/ada/sem_ch3.adb b/gcc/ada/sem_ch3.adb
index 634b1cb..f360be8 100644
--- a/gcc/ada/sem_ch3.adb
+++ b/gcc/ada/sem_ch3.adb
@@ -6848,25 +6848,16 @@ package body Sem_Ch3 is
       declare
          Asp  : Node_Id;
          A_Id : Aspect_Id;
-         Cond : Node_Id;
-         Expr : Node_Id;
 
       begin
          Asp := First (Aspect_Specifications (Decl));
          while Present (Asp) loop
             A_Id := Get_Aspect_Id (Chars (Identifier (Asp)));
             if A_Id = Aspect_Pre or else A_Id = Aspect_Post then
-               Cond := Asp;
-               Expr := Expression (Cond);
-               Replace_Type_Name (Expr);
-               Next (Asp);
-
-               Remove (Cond);
-               Append (Cond, Contracts);
-
-            else
-               Next (Asp);
+               Append (New_Copy_Tree (Asp), Contracts);
+               Replace_Type_Name (Expression (Last (Contracts)));
             end if;
+            Next (Asp);
          end loop;
       end;
 
diff --git a/gcc/ada/sem_prag.adb b/gcc/ada/sem_prag.adb
index 5363d2b..88dacf5 100644
--- a/gcc/ada/sem_prag.adb
+++ b/gcc/ada/sem_prag.adb
@@ -5235,9 +5235,19 @@ package body Sem_Prag is
          then
             null;
 
-         --  An access-to-subprogram type can have pre/postconditions, but
-         --  these are transferred to the generated subprogram wrapper and
-         --  analyzed there.
+         --  An access-to-subprogram type can have pre/postconditions, which
+         --  are both analyzed when attached to the type and copied to the
+         --  generated subprogram wrapper and analyzed there.
+
+         elsif Nkind (Subp_Decl) = N_Full_Type_Declaration
+           and then Nkind (Type_Definition (Subp_Decl)) in
+                      N_Access_To_Subprogram_Definition
+         then
+            if Ada_Version < Ada_2022 then
+               Error_Msg_Ada_2022_Feature
+                 ("pre/postcondition access-to-subprogram", Loc);
+               raise Pragma_Exit;
+            end if;
 
          --  Otherwise the placement of the pragma is illegal
 
@@ -26635,11 +26645,15 @@ package body Sem_Prag is
 
       if not In_Open_Scopes (Spec_Id) then
          Restore_Scope := True;
-         Push_Scope (Spec_Id);
 
          if Is_Generic_Subprogram (Spec_Id) then
+            Push_Scope (Spec_Id);
             Install_Generic_Formals (Spec_Id);
+         elsif Is_Access_Subprogram_Type (Spec_Id) then
+            Push_Scope (Designated_Type (Spec_Id));
+            Install_Formals (Designated_Type (Spec_Id));
          else
+            Push_Scope (Spec_Id);
             Install_Formals (Spec_Id);
          end if;
       end if;