[gcc r12-6249] [Ada] Expand controlling functions wrappers in GNATprove mode

[Pierre-Marie de Rodat]

https://gcc.gnu.org/g:3531f20f6cff7e43dcde44b200467872a925188f

commit r12-6249-g3531f20f6cff7e43dcde44b200467872a925188f
Author: Piotr Trojanek <trojanek@adacore.com>
Date:   Wed Nov 24 23:21:07 2021 +0100

    [Ada] Expand controlling functions wrappers in GNATprove mode
    
    gcc/ada/
    
            * exp_ch3.ads (Make_Controlling_Function_Wrappers): Move
            declaration from body to spec, so it can be called by
            SPARK-specific expansion.
            * exp_ch3.adb (Make_Controlling_Function_Wrappers): Likewise.
            * exp_spark.adb (SPARK_Freeze_Type): Enable expansion of
            wrappers for function with controlling result types.

Diff:
---
 gcc/ada/exp_ch3.adb   | 11 -----------
 gcc/ada/exp_ch3.ads   | 11 +++++++++++
 gcc/ada/exp_spark.adb | 32 ++++++++++++++++++++++++++++++++
 3 files changed, 43 insertions(+), 11 deletions(-)

diff --git a/gcc/ada/exp_ch3.adb b/gcc/ada/exp_ch3.adb
index 13ae58dc22b..20a1da831cf 100644
--- a/gcc/ada/exp_ch3.adb
+++ b/gcc/ada/exp_ch3.adb
@@ -294,17 +294,6 @@ package body Exp_Ch3 is
    --  inherited. If the result is false, the init_proc and the discriminant
    --  checking functions of the parent can be reused by a derived type.
 
-   procedure Make_Controlling_Function_Wrappers
-     (Tag_Typ   : Entity_Id;
-      Decl_List : out List_Id;
-      Body_List : out List_Id);
-   --  Ada 2005 (AI-391): Makes specs and bodies for the wrapper functions
-   --  associated with inherited functions with controlling results which
-   --  are not overridden. The body of each wrapper function consists solely
-   --  of a return statement whose expression is an extension aggregate
-   --  invoking the inherited subprogram's parent subprogram and extended
-   --  with a null association list.
-
    function Make_Null_Procedure_Specs (Tag_Typ : Entity_Id) return List_Id;
    --  Ada 2005 (AI-251): Makes specs for null procedures associated with any
    --  null procedures inherited from an interface type that have not been
diff --git a/gcc/ada/exp_ch3.ads b/gcc/ada/exp_ch3.ads
index c7648e6f419..db78ee9bef8 100644
--- a/gcc/ada/exp_ch3.ads
+++ b/gcc/ada/exp_ch3.ads
@@ -158,6 +158,17 @@ package Exp_Ch3 is
    --  initialized; if Variable_Comps is True then tags components located at
    --  variable positions of Target are initialized.
 
+   procedure Make_Controlling_Function_Wrappers
+     (Tag_Typ   : Entity_Id;
+      Decl_List : out List_Id;
+      Body_List : out List_Id);
+   --  Ada 2005 (AI-391): Makes specs and bodies for the wrapper functions
+   --  associated with inherited functions with controlling results which
+   --  are not overridden. The body of each wrapper function consists solely
+   --  of a return statement whose expression is an extension aggregate
+   --  invoking the inherited subprogram's parent subprogram and extended
+   --  with a null association list.
+
    procedure Make_Predefined_Primitive_Eq_Spec
      (Tag_Typ     : Entity_Id;
       Predef_List : List_Id;
diff --git a/gcc/ada/exp_spark.adb b/gcc/ada/exp_spark.adb
index 84927f8509c..62b85ccf21a 100644
--- a/gcc/ada/exp_spark.adb
+++ b/gcc/ada/exp_spark.adb
@@ -903,6 +903,9 @@ package body Exp_SPARK is
       Eq_Spec     : Node_Id := Empty;
       Predef_List : List_Id;
 
+      Wrapper_Decl_List : List_Id;
+      Wrapper_Body_List : List_Id := No_List;
+
       Saved_GM  : constant Ghost_Mode_Type := Ghost_Mode;
       Saved_IGR : constant Node_Id         := Ignored_Ghost_Region;
       --  Save the Ghost-related attributes to restore on exit
@@ -961,6 +964,35 @@ package body Exp_SPARK is
          end if;
       end if;
 
+      if Ekind (Typ) = E_Record_Type
+        and then Is_Tagged_Type (Typ)
+        and then not Is_CPP_Class (Typ)
+      then
+         --  Ada 2005 (AI-391): For a nonabstract null extension, create
+         --  wrapper functions for each nonoverridden inherited function
+         --  with a controlling result of the type. The wrapper for such
+         --  a function returns an extension aggregate that invokes the
+         --  parent function.
+
+         if Ada_Version >= Ada_2005
+           and then not Is_Abstract_Type (Typ)
+           and then Is_Null_Extension (Typ)
+         then
+            Exp_Ch3.Make_Controlling_Function_Wrappers
+              (Typ, Wrapper_Decl_List, Wrapper_Body_List);
+            Insert_List_Before_And_Analyze (N, Wrapper_Decl_List);
+         end if;
+
+         --  Ada 2005 (AI-391): If any wrappers were created for nonoverridden
+         --  inherited functions, then add their bodies to the AST, so they
+         --  will be processed like ordinary subprogram bodies (even though the
+         --  compiler adds them into the freezing action).
+
+         if not Is_Interface (Typ) then
+            Insert_List_Before_And_Analyze (N, Wrapper_Body_List);
+         end if;
+      end if;
+
       Restore_Ghost_Region (Saved_GM, Saved_IGR);
    end SPARK_Freeze_Type;