From 7f5e1dee7c70db3fd4e4dab5f205a30b8373a8de Mon Sep 17 00:00:00 2001 From: Javier Miranda Date: Wed, 20 Apr 2016 09:15:47 +0000 Subject: [PATCH] contracts.adb (Build_Postconditions_Procedure): Code cleanup. 2016-04-20 Javier Miranda * contracts.adb (Build_Postconditions_Procedure): Code cleanup. * ghost.adb (Os_OK_Ghost_Context.Is_OK_Declaration): Handle the declaration of the internally built _postcondition procedure. From-SVN: r235245 --- gcc/ada/ChangeLog | 6 ++++ gcc/ada/contracts.adb | 67 ++++++++++++++++++++----------------------- gcc/ada/ghost.adb | 25 +++++++++++----- 3 files changed, 55 insertions(+), 43 deletions(-) diff --git a/gcc/ada/ChangeLog b/gcc/ada/ChangeLog index fe429f1283e..db327f32d25 100644 --- a/gcc/ada/ChangeLog +++ b/gcc/ada/ChangeLog @@ -1,3 +1,9 @@ +2016-04-20 Javier Miranda + + * contracts.adb (Build_Postconditions_Procedure): Code cleanup. + * ghost.adb (Os_OK_Ghost_Context.Is_OK_Declaration): Handle the + declaration of the internally built _postcondition procedure. + 2016-04-20 Arnaud Charlet * snames.ads-tmpl (Internal_Attribute_Id, Attribute_Class_Array): Fix diff --git a/gcc/ada/contracts.adb b/gcc/ada/contracts.adb index a5f8bc3e5a3..af6264cd106 100644 --- a/gcc/ada/contracts.adb +++ b/gcc/ada/contracts.adb @@ -1749,8 +1749,7 @@ package body Contracts is end if; Proc_Id := Make_Defining_Identifier (Loc, Name_uPostconditions); - Set_Debug_Info_Needed (Proc_Id); - Set_Postconditions_Proc (Subp_Id, Proc_Id); + Set_Debug_Info_Needed (Proc_Id); -- The related subprogram is a function: create the specification of -- parameter _Result. @@ -1786,51 +1785,47 @@ package body Contracts is -- the postconditions: this would cause confusing debug info to be -- produced, interfering with coverage-analysis tools. - Proc_Bod := - Make_Subprogram_Body (Loc, - Specification => + declare + Proc_Decl : Node_Id; + Proc_Decl_Id : Entity_Id; + Proc_Spec : Node_Id; + begin + Proc_Spec := Make_Procedure_Specification (Loc, Defining_Unit_Name => Proc_Id, - Parameter_Specifications => Params), + Parameter_Specifications => Params); - Declarations => Empty_List, - Handled_Statement_Sequence => - Make_Handled_Sequence_Of_Statements (Loc, - Statements => Stmts, - End_Label => Make_Identifier (Loc, Chars (Proc_Id)))); + Proc_Decl := Make_Subprogram_Declaration (Loc, Proc_Spec); + Proc_Decl_Id := Defining_Entity (Specification (Proc_Decl)); + Set_Postconditions_Proc (Subp_Id, Proc_Decl_Id); - Insert_Before_First_Source_Declaration (Proc_Bod); + -- Force the front end inlining of _PostConditions when generating + -- C code since its body may have references to itypes defined in + -- the enclosing subprogram, thus causing problems to unnesting + -- routines. - -- Force the front-end inlining of _PostConditions when generating - -- C code, since its body may have references to itypes defined in - -- the enclosing subprogram, thus causing problems for the unnested - -- routines. For this purpose its declaration with proper decoration - -- for inlining is needed. - - if Generate_C_Code then - declare - Proc_Decl : Node_Id; - Proc_Decl_Id : Entity_Id; - - begin - Proc_Decl := - Make_Subprogram_Declaration (Loc, - Specification => - Copy_Subprogram_Spec (Specification (Proc_Bod))); - Insert_Before (Proc_Bod, Proc_Decl); - - Proc_Decl_Id := Defining_Entity (Specification (Proc_Decl)); + if Generate_C_Code then Set_Has_Pragma_Inline (Proc_Decl_Id); Set_Has_Pragma_Inline_Always (Proc_Decl_Id); Set_Is_Inlined (Proc_Decl_Id); + end if; - Set_Postconditions_Proc (Subp_Id, Proc_Decl_Id); + Insert_Before_First_Source_Declaration (Proc_Decl); + Analyze (Proc_Decl); - Analyze (Proc_Decl); - end; - end if; + Proc_Bod := + Make_Subprogram_Body (Loc, + Specification => + Copy_Subprogram_Spec (Proc_Spec), + Declarations => Empty_List, + Handled_Statement_Sequence => + Make_Handled_Sequence_Of_Statements (Loc, + Statements => Stmts, + End_Label => Make_Identifier (Loc, Chars (Proc_Id)))); - Analyze (Proc_Bod); + Insert_Before_First_Source_Declaration (Proc_Bod); + Analyze (Proc_Bod); + end; end Build_Postconditions_Procedure; ---------------------------- diff --git a/gcc/ada/ghost.adb b/gcc/ada/ghost.adb index 9d01b6dce14..69865b531c9 100644 --- a/gcc/ada/ghost.adb +++ b/gcc/ada/ghost.adb @@ -254,15 +254,26 @@ package body Ghost is then Subp_Id := Corresponding_Spec (Decl); - -- The original context is an expression function that has - -- been split into a spec and a body. The context is OK as - -- long as the initial declaration is Ghost. - if Present (Subp_Id) then - Subp_Decl := Original_Node (Unit_Declaration_Node (Subp_Id)); - if Nkind (Subp_Decl) = N_Expression_Function then - return Is_Subject_To_Ghost (Subp_Decl); + -- The context is the internally built _postconditions + -- subprogram, which it is OK because the real check was + -- done before expansion activities. + + if Chars (Subp_Id) = Name_uPostconditions then + return True; + + else + Subp_Decl := + Original_Node (Unit_Declaration_Node (Subp_Id)); + + -- The original context is an expression function that + -- has been split into a spec and a body. The context is + -- OK as long as the initial declaration is Ghost. + + if Nkind (Subp_Decl) = N_Expression_Function then + return Is_Subject_To_Ghost (Subp_Decl); + end if; end if; -- Otherwise this is either an internal body or an internal