diff mbox series

[Ada] Expand controlling function wrapper into expression function

Message ID 20220105113354.GA2716256@adacore.com
State New
Headers show
Series [Ada] Expand controlling function wrapper into expression function | expand

Commit Message

Pierre-Marie de Rodat Jan. 5, 2022, 11:33 a.m. UTC 
GNATprove prefers various internally generated functions to be
expression functions, because then it will use the expression itself as
an implicit postcondition. The same applies to wrappers for dispatching
functions with controlling results.

Tested on x86_64-pc-linux-gnu, committed on trunk

gcc/ada/

	* exp_ch3.adb (Make_Controlling_Function_Wrappers): For
	GNATprove build the wrapper as an expression function.
diff mbox series

Patch

diff --git a/gcc/ada/exp_ch3.adb b/gcc/ada/exp_ch3.adb
--- a/gcc/ada/exp_ch3.adb
+++ b/gcc/ada/exp_ch3.adb
@@ -9607,11 +9607,11 @@  package body Exp_Ch3 is
       Actual_List : List_Id;
       Formal      : Entity_Id;
       Par_Formal  : Entity_Id;
+      Ext_Aggr    : Node_Id;
       Formal_Node : Node_Id;
       Func_Body   : Node_Id;
       Func_Decl   : Node_Id;
       Func_Id     : Entity_Id;
-      Return_Stmt : Node_Id;
 
    --  Start of processing for Make_Controlling_Function_Wrappers
 
@@ -9731,25 +9731,38 @@  package body Exp_Ch3 is
                Actual_List := No_List;
             end if;
 
-            Return_Stmt :=
-              Make_Simple_Return_Statement (Loc,
-                Expression =>
-                  Make_Extension_Aggregate (Loc,
-                    Ancestor_Part       =>
-                      Make_Function_Call (Loc,
-                        Name                   =>
-                          New_Occurrence_Of (Alias (Subp), Loc),
-                        Parameter_Associations => Actual_List),
-                    Null_Record_Present => True));
-
-            Func_Body :=
-              Make_Subprogram_Body (Loc,
-                Specification              =>
-                  Make_Wrapper_Specification (Subp),
-                Declarations               => Empty_List,
-                Handled_Statement_Sequence =>
-                  Make_Handled_Sequence_Of_Statements (Loc,
-                    Statements => New_List (Return_Stmt)));
+            Ext_Aggr :=
+              Make_Extension_Aggregate (Loc,
+                Ancestor_Part       =>
+                  Make_Function_Call (Loc,
+                    Name                   =>
+                      New_Occurrence_Of (Alias (Subp), Loc),
+                    Parameter_Associations => Actual_List),
+                Null_Record_Present => True);
+
+            --  GNATprove will use expression of an expression function as an
+            --  implicit postcondition. GNAT will not benefit from expression
+            --  function (and would struggle if we add an expression function
+            --  to freezing actions).
+
+            if GNATprove_Mode then
+               Func_Body :=
+                 Make_Expression_Function (Loc,
+                   Specification =>
+                     Make_Wrapper_Specification (Subp),
+                   Expression => Ext_Aggr);
+            else
+               Func_Body :=
+                 Make_Subprogram_Body (Loc,
+                   Specification              =>
+                     Make_Wrapper_Specification (Subp),
+                   Declarations               => Empty_List,
+                   Handled_Statement_Sequence =>
+                     Make_Handled_Sequence_Of_Statements (Loc,
+                       Statements => New_List (
+                         Make_Simple_Return_Statement (Loc,
+                           Expression => Ext_Aggr))));
+            end if;
 
             Append_To (Body_List, Func_Body);