From mboxrd@z Thu Jan 1 00:00:00 1970 Return-Path: Received: by sourceware.org (Postfix, from userid 1914) id C334B3858434; Wed, 5 Jan 2022 11:35:34 +0000 (GMT) DKIM-Filter: OpenDKIM Filter v2.11.0 sourceware.org C334B3858434 MIME-Version: 1.0 Content-Transfer-Encoding: 7bit Content-Type: text/plain; charset="utf-8" From: Pierre-Marie de Rodat To: gcc-cvs@gcc.gnu.org Subject: [gcc r12-6250] [Ada] Expand controlling function wrapper into expression function X-Act-Checkin: gcc X-Git-Author: Piotr Trojanek X-Git-Refname: refs/heads/master X-Git-Oldrev: 3531f20f6cff7e43dcde44b200467872a925188f X-Git-Newrev: 2af751b3b8db297e1cc78e3968ca1f714b75c4ea Message-Id: <20220105113534.C334B3858434@sourceware.org> Date: Wed, 5 Jan 2022 11:35:34 +0000 (GMT) X-BeenThere: gcc-cvs@gcc.gnu.org X-Mailman-Version: 2.1.29 Precedence: list List-Id: Gcc-cvs mailing list List-Unsubscribe: , List-Archive: List-Help: List-Subscribe: , X-List-Received-Date: Wed, 05 Jan 2022 11:35:34 -0000 https://gcc.gnu.org/g:2af751b3b8db297e1cc78e3968ca1f714b75c4ea commit r12-6250-g2af751b3b8db297e1cc78e3968ca1f714b75c4ea Author: Piotr Trojanek Date: Wed Dec 1 17:51:13 2021 +0100 [Ada] Expand controlling function wrapper into expression function gcc/ada/ * exp_ch3.adb (Make_Controlling_Function_Wrappers): For GNATprove build the wrapper as an expression function. Diff: --- gcc/ada/exp_ch3.adb | 53 +++++++++++++++++++++++++++++++++-------------------- 1 file changed, 33 insertions(+), 20 deletions(-) diff --git a/gcc/ada/exp_ch3.adb b/gcc/ada/exp_ch3.adb index 20a1da831cf..eb386e4250a 100644 --- 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);