[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.

3 files changed, 43 insertions, 11 deletions

diff --git a/gcc/ada/exp_ch3.adb b/gcc/ada/exp_ch3.adb
index 13ae58d..20a1da8 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 c7648e6..db78ee9 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 84927f8..62b85cc 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;