From 039538bc35b844d57ca526bf1a274c93d251b6f5 Mon Sep 17 00:00:00 2001 From: Arnaud Charlet Date: Thu, 30 Oct 2014 12:34:41 +0100 Subject: [PATCH] [multiple changes] 2014-10-30 Yannick Moy * inline.adb (Has_Single_Return_In_GNATprove_Mode): Return False when return statement is inside one or more blocks. 2014-10-30 Hristian Kirtchev * exp_ch7.adb (Is_Subprogram_Call): Account for the case where an object declaration initialized by a function call that returns an unconstrained result may be rewritted as a renaming of the secondary stack result. 2014-10-30 Hristian Kirtchev * aspects.adb: Add an entry for aspect Extensions_Visible in table Canonical_Aspect. * aspects.ads: Add entry for aspect Extensions_Visible in tables Aspect_Argument, Aspect_Delay, Aspect_Id, Aspect_Names, Implementation_Defined_Aspect. * einfo.adb (Get_Pragma): Include pragma Extensions_Visible in the list of contract pragmas. * par-prag.adb Pragma Extensions_Visible does not require special processing from the parser. * sem_ch3.adb (Analyze_Object_Declaration): Prevent an implicit class-wide conversion of a formal parameter of a specific tagged type whose related subprogram is subject to pragma Extensions_Visible with value "False". (Check_Abstract_Overriding): Add various overriding checks related to pragma Extensions_Visible. (Derive_Subprogram): A subprogram subject to pragma Extensions_Visible with value False requires overriding if the subprogram has at least one controlling OUT parameter. (Is_EVF_Procedure): New routine. * sem_ch4.adb (Analyze_Type_Conversion): A formal parameter of a specific tagged type whose related subprogram is subject to pragma Extensions_Visible with value "False" cannot appear in a class-wide conversion. * sem_ch6.adb (Analyze_Subprogram_Contract): Remove the assertion to account for pragma Extensions_Visible. (Check_Overriding_Indicator): An overriding subprogram inherits the contact of the overridden subprogram. (New_Overloaded_Entity): An overriding subprogram inherits the contact of the overridden subprogram. * sem_ch13.adb (Analyze_Aspect_Specifications): Add processing for aspect Extensions_Visible. (Check_Aspect_At_Freeze_Point): Aspect Extensions_Visible does not require special processing at the freeze point. * sem_prag.adb Add an entry for pragma Extensions_Visible in table Sig_Flags. (Analyze_Pragma): Ensure that various SPARK pragmas lack identifiers in their arguments. Add processing for pragma Extensions_Visible. (Chain_CTC): Code reformatting. * sem_res.adb (Resolve_Actuals): A formal parameter of a specific tagged type whose related subprogram is subject to pragma Extensions_Visible with value "False" cannot act as an actual in a subprogram with value "True". * sem_util.adb (Add_Classification): New routine. (Add_Contract_Item): Account for pragma Extensions_Visible. Code reformatting. (Add_Contract_Test_Case): New routine. (Add_Pre_Post_Condition): New routine. (Extensions_Visible_Status): New routine. (Inherit_Subprogram_Contract): New routine. (Is_EVF_Expression): New routine. (Is_Specific_Tagged_Type): New routine. * sem_util.ads Add type Extensions_Visible_Mode and document all values. (Add_Contract_Item): Add pragma Extensions_Visible to the comment on usage. (Inherit_Subprogram_Contract): New routine. (Is_EVF_Expression): New routine. (Is_Specific_Tagged_Type): New routine. * sinfo.adb (Is_Inherited): New routine. (Set_Is_Inherited): New routine. * sinfo.ads Add flag Is_Inherited along with its usage in nodes. (Is_Inherited): New routine along with pragma Inline. (Set_Is_Inherited): New routine along with pragma Inline. * snames.ads-tmpl: Add predefined name "Extensions_Visible" and a new Pragma_Id for the pragma. From-SVN: r216919 --- gcc/ada/ChangeLog | 132 ++++++++++++++++ gcc/ada/aspects.adb | 1 + gcc/ada/aspects.ads | 9 +- gcc/ada/einfo.adb | 35 ++--- gcc/ada/exp_ch7.adb | 11 +- gcc/ada/inline.adb | 19 +-- gcc/ada/par-prag.adb | 1 + gcc/ada/sem_ch13.adb | 16 ++ gcc/ada/sem_ch3.adb | 93 ++++++++++- gcc/ada/sem_ch4.adb | 38 +++-- gcc/ada/sem_ch6.adb | 28 +++- gcc/ada/sem_prag.adb | 195 ++++++++++++++++++++---- gcc/ada/sem_res.adb | 20 ++- gcc/ada/sem_util.adb | 330 +++++++++++++++++++++++++++++++++++----- gcc/ada/sem_util.ads | 42 +++++ gcc/ada/sinfo.adb | 16 ++ gcc/ada/sinfo.ads | 17 ++- gcc/ada/snames.ads-tmpl | 2 + 18 files changed, 869 insertions(+), 136 deletions(-) diff --git a/gcc/ada/ChangeLog b/gcc/ada/ChangeLog index 8c6bf7a5857..65e0b602754 100644 --- a/gcc/ada/ChangeLog +++ b/gcc/ada/ChangeLog @@ -1,3 +1,135 @@ +2014-10-30 Yannick Moy + + * inline.adb (Has_Single_Return_In_GNATprove_Mode): + Return False when return statement is inside one or more blocks. + +2014-10-30 Hristian Kirtchev + + * exp_ch7.adb (Is_Subprogram_Call): Account for the case where an + object declaration initialized by a function call that returns + an unconstrained result may be rewritted as a renaming of the + secondary stack result. + +2014-10-30 Hristian Kirtchev + + * aspects.adb: Add an entry for aspect Extensions_Visible in + table Canonical_Aspect. + * aspects.ads: Add entry for aspect Extensions_Visible in + tables Aspect_Argument, Aspect_Delay, Aspect_Id, Aspect_Names, + Implementation_Defined_Aspect. + * einfo.adb (Get_Pragma): Include pragma Extensions_Visible in + the list of contract pragmas. + * par-prag.adb Pragma Extensions_Visible does not require special + processing from the parser. + * sem_ch3.adb (Analyze_Object_Declaration): Prevent an + implicit class-wide conversion of a formal parameter + of a specific tagged type whose related subprogram is + subject to pragma Extensions_Visible with value "False". + (Check_Abstract_Overriding): Add various overriding checks + related to pragma Extensions_Visible. + (Derive_Subprogram): + A subprogram subject to pragma Extensions_Visible with value + False requires overriding if the subprogram has at least one + controlling OUT parameter. + (Is_EVF_Procedure): New routine. + * sem_ch4.adb (Analyze_Type_Conversion): A formal parameter of + a specific tagged type whose related subprogram is subject to + pragma Extensions_Visible with value "False" cannot appear in + a class-wide conversion. + * sem_ch6.adb (Analyze_Subprogram_Contract): Remove + the assertion to account for pragma Extensions_Visible. + (Check_Overriding_Indicator): An overriding subprogram + inherits the contact of the overridden subprogram. + (New_Overloaded_Entity): An overriding subprogram inherits the + contact of the overridden subprogram. + * sem_ch13.adb (Analyze_Aspect_Specifications): Add processing + for aspect Extensions_Visible. + (Check_Aspect_At_Freeze_Point): Aspect Extensions_Visible does not + require special processing at the freeze point. + * sem_prag.adb Add an entry for pragma Extensions_Visible in + table Sig_Flags. + (Analyze_Pragma): Ensure that various SPARK + pragmas lack identifiers in their arguments. Add processing for + pragma Extensions_Visible. + (Chain_CTC): Code reformatting. + * sem_res.adb (Resolve_Actuals): A formal parameter of a + specific tagged type whose related subprogram is subject to + pragma Extensions_Visible with value "False" cannot act as an + actual in a subprogram with value "True". + * sem_util.adb (Add_Classification): New routine. + (Add_Contract_Item): Account for pragma Extensions_Visible. Code + reformatting. + (Add_Contract_Test_Case): New routine. + (Add_Pre_Post_Condition): New routine. + (Extensions_Visible_Status): New routine. + (Inherit_Subprogram_Contract): New routine. + (Is_EVF_Expression): New routine. + (Is_Specific_Tagged_Type): New routine. + * sem_util.ads Add type Extensions_Visible_Mode and document all values. + (Add_Contract_Item): Add pragma Extensions_Visible to the + comment on usage. + (Inherit_Subprogram_Contract): New routine. + (Is_EVF_Expression): New routine. + (Is_Specific_Tagged_Type): New routine. + * sinfo.adb (Is_Inherited): New routine. + (Set_Is_Inherited): New routine. + * sinfo.ads Add flag Is_Inherited along with its usage in + nodes. + (Is_Inherited): New routine along with pragma Inline. + (Set_Is_Inherited): New routine along with pragma Inline. + * snames.ads-tmpl: Add predefined name "Extensions_Visible" + and a new Pragma_Id for the pragma. + +2014-10-30 Vincent Celier + + * prj-proc.adb (Process_Case_Construction): Do not look for + the ultimate extending project for a case variable. + +2014-10-30 Pierre-Marie Derodat + + * exp_dbug.adb, opt.ads (GNAT_Encodings): Import from C. Define + enumerators. + (gnat_encodings): Define a dummy variable for the AAMP back-end. + (Get_Encoded_Name): When -fgnat-encodings=all|gdb, encode names + for all discrete types whose bounds do not match size and do so + only for biased types when -fgnat-encodings=minimal. + * gcc-interface/decl.c (gnat_to_gnu_entity): Do not create ___XA + parallel types when array bounds are constant while the lower bound is + not 1. Also stop generating them because the bound type is + larger than sizetype. + * gcc-interface/misc.c (gnat_encodings): New. + +2014-10-30 Thomas Quinot + + * opt.adb (Set_Opt_Config_Switches): For an internal unit, + always reset Default_SSO to ' '. + +2014-10-30 Thomas Quinot + + * freeze.adb (Freeze_Record_Type): Set SSO from default before + checking SSO consistency. + +2014-10-30 Javier Miranda + + * inline.adb (Check_Package_Body_For_Inlining): + Cleanup this subprogram to implement exactly the behavior + documented in the spec. + +2014-10-30 Hristian Kirtchev + + * a-comutr.adb, a-cimutr.adb (Insert_Child): Add new variable First. + Update the position after all insertions have taken place. + +2014-10-30 Ed Schonberg + + * sem_prag.adb (Analyze_Pragma, case License): Do not perform + analysis of pragma arguments when in CodePeer mode, pragma has + different format on other compilers. + +2014-10-30 Thomas Quinot + + * s-os_lib.adb: Minor reformatting. + 2014-10-29 Richard Sandiford * gcc-interface/decl.c, gcc-interface/gigi.h, gcc-interface/misc.c, diff --git a/gcc/ada/aspects.adb b/gcc/ada/aspects.adb index ecac9ff2941..ee8e8b831c8 100644 --- a/gcc/ada/aspects.adb +++ b/gcc/ada/aspects.adb @@ -522,6 +522,7 @@ package body Aspects is Aspect_Effective_Writes => Aspect_Effective_Writes, Aspect_Elaborate_Body => Aspect_Elaborate_Body, Aspect_Export => Aspect_Export, + Aspect_Extensions_Visible => Aspect_Extensions_Visible, Aspect_External_Name => Aspect_External_Name, Aspect_External_Tag => Aspect_External_Tag, Aspect_Favor_Top_Level => Aspect_Favor_Top_Level, diff --git a/gcc/ada/aspects.ads b/gcc/ada/aspects.ads index 173c66db173..50bada041f0 100644 --- a/gcc/ada/aspects.ads +++ b/gcc/ada/aspects.ads @@ -94,6 +94,7 @@ package Aspects is Aspect_Dimension_System, -- GNAT Aspect_Dispatching_Domain, Aspect_Dynamic_Predicate, + Aspect_Extensions_Visible, -- GNAT Aspect_External_Name, Aspect_External_Tag, Aspect_Global, -- GNAT @@ -230,6 +231,7 @@ package Aspects is Aspect_Dimension_System => True, Aspect_Effective_Reads => True, Aspect_Effective_Writes => True, + Aspect_Extensions_Visible => True, Aspect_Favor_Top_Level => True, Aspect_Global => True, Aspect_Inline_Always => True, @@ -318,6 +320,7 @@ package Aspects is Aspect_Dimension_System => Expression, Aspect_Dispatching_Domain => Expression, Aspect_Dynamic_Predicate => Expression, + Aspect_Extensions_Visible => Optional_Expression, Aspect_External_Name => Expression, Aspect_External_Tag => Expression, Aspect_Global => Expression, @@ -408,9 +411,10 @@ package Aspects is Aspect_Effective_Reads => Name_Effective_Reads, Aspect_Effective_Writes => Name_Effective_Writes, Aspect_Elaborate_Body => Name_Elaborate_Body, + Aspect_Export => Name_Export, + Aspect_Extensions_Visible => Name_Extensions_Visible, Aspect_External_Name => Name_External_Name, Aspect_External_Tag => Name_External_Tag, - Aspect_Export => Name_Export, Aspect_Favor_Top_Level => Name_Favor_Top_Level, Aspect_Global => Name_Global, Aspect_Implicit_Dereference => Name_Implicit_Dereference, @@ -618,9 +622,9 @@ package Aspects is Aspect_Dispatching_Domain => Always_Delay, Aspect_Dynamic_Predicate => Always_Delay, Aspect_Elaborate_Body => Always_Delay, + Aspect_Export => Always_Delay, Aspect_External_Name => Always_Delay, Aspect_External_Tag => Always_Delay, - Aspect_Export => Always_Delay, Aspect_Favor_Top_Level => Always_Delay, Aspect_Implicit_Dereference => Always_Delay, Aspect_Import => Always_Delay, @@ -689,6 +693,7 @@ package Aspects is Aspect_Dimension_System => Never_Delay, Aspect_Effective_Reads => Never_Delay, Aspect_Effective_Writes => Never_Delay, + Aspect_Extensions_Visible => Never_Delay, Aspect_Global => Never_Delay, Aspect_Initial_Condition => Never_Delay, Aspect_Initializes => Never_Delay, diff --git a/gcc/ada/einfo.adb b/gcc/ada/einfo.adb index 18cac0f9b4b..aaa6ea5f060 100644 --- a/gcc/ada/einfo.adb +++ b/gcc/ada/einfo.adb @@ -6684,31 +6684,32 @@ package body Einfo is function Get_Pragma (E : Entity_Id; Id : Pragma_Id) return Node_Id is Is_CDG : constant Boolean := - Id = Pragma_Abstract_State or else - Id = Pragma_Async_Readers or else - Id = Pragma_Async_Writers or else - Id = Pragma_Depends or else - Id = Pragma_Effective_Reads or else - Id = Pragma_Effective_Writes or else - Id = Pragma_Global or else - Id = Pragma_Initial_Condition or else - Id = Pragma_Initializes or else - Id = Pragma_Part_Of or else - Id = Pragma_Refined_Depends or else - Id = Pragma_Refined_Global or else + Id = Pragma_Abstract_State or else + Id = Pragma_Async_Readers or else + Id = Pragma_Async_Writers or else + Id = Pragma_Depends or else + Id = Pragma_Effective_Reads or else + Id = Pragma_Effective_Writes or else + Id = Pragma_Extensions_Visible or else + Id = Pragma_Global or else + Id = Pragma_Initial_Condition or else + Id = Pragma_Initializes or else + Id = Pragma_Part_Of or else + Id = Pragma_Refined_Depends or else + Id = Pragma_Refined_Global or else Id = Pragma_Refined_State; Is_CTC : constant Boolean := - Id = Pragma_Contract_Cases or else + Id = Pragma_Contract_Cases or else Id = Pragma_Test_Case; Is_PPC : constant Boolean := - Id = Pragma_Precondition or else - Id = Pragma_Postcondition or else + Id = Pragma_Precondition or else + Id = Pragma_Postcondition or else Id = Pragma_Refined_Post; In_Contract : constant Boolean := Is_CDG or Is_CTC or Is_PPC; - Item : Node_Id; - Items : Node_Id; + Item : Node_Id; + Items : Node_Id; begin -- Handle pragmas that appear in N_Contract nodes. Those have to be diff --git a/gcc/ada/exp_ch7.adb b/gcc/ada/exp_ch7.adb index b98aed6bbab..8d5dd36aee8 100644 --- a/gcc/ada/exp_ch7.adb +++ b/gcc/ada/exp_ch7.adb @@ -4532,11 +4532,14 @@ package body Exp_Ch7 is function Is_Subprogram_Call (N : Node_Id) return Traverse_Result is begin -- Complex constructs are factored out by the expander and their - -- occurrences are replaced with references to temporaries. Due to - -- this expansion activity, inspect the original tree to detect - -- subprogram calls. + -- occurrences are replaced with references to temporaries or + -- object renamings. Due to this expansion activity, inspect the + -- original tree to detect subprogram calls. - if Nkind (N) = N_Identifier and then Original_Node (N) /= N then + if Nkind_In (N, N_Identifier, + N_Object_Renaming_Declaration) + and then Original_Node (N) /= N + then Detect_Subprogram_Call (Original_Node (N)); -- The original construct contains a subprogram call, there is diff --git a/gcc/ada/inline.adb b/gcc/ada/inline.adb index efb4e6cd0f3..8e2df38468f 100644 --- a/gcc/ada/inline.adb +++ b/gcc/ada/inline.adb @@ -933,7 +933,10 @@ package body Inline is function Has_Single_Return_In_GNATprove_Mode return Boolean; -- This function is called only in GNATprove mode, and it returns -- True if the subprogram has no return statement or a single return - -- statement as last statement. + -- statement as last statement. It returns False for subprogram with + -- a single return as last statement inside one or more blocks, as + -- inlining would generate gotos in that case as well (although the + -- goto is useless in that case). function Uses_Secondary_Stack (Bod : Node_Id) return Boolean; -- If the body of the subprogram includes a call that returns an @@ -1003,15 +1006,10 @@ package body Inline is -- Start of processing for Has_Single_Return_In_GNATprove_Mode begin - -- Retrieve last statement inside possible block statements + -- Retrieve the last statement Last_Statement := Last (Statements (Handled_Statement_Sequence (N))); - while Nkind (Last_Statement) = N_Block_Statement loop - Last_Statement := - Last (Statements (Handled_Statement_Sequence (Last_Statement))); - end loop; - -- Check that the last statement is the only possible return -- statement in the subprogram. @@ -2049,16 +2047,15 @@ package body Inline is OK : Boolean; begin - if Is_Compilation_Unit (P) + if Front_End_Inlining + and then Is_Compilation_Unit (P) and then not Is_Generic_Instance (P) then Bname := Get_Body_Name (Get_Unit_Name (Unit (N))); E := First_Entity (P); while Present (E) loop - if Has_Pragma_Inline_Always (E) - or else (Front_End_Inlining and then Has_Pragma_Inline (E)) - then + if Has_Pragma_Inline (E) then if not Is_Loaded (Bname) then Load_Needed_Body (N, OK); diff --git a/gcc/ada/par-prag.adb b/gcc/ada/par-prag.adb index 44f936e96e7..7bf57290ca5 100644 --- a/gcc/ada/par-prag.adb +++ b/gcc/ada/par-prag.adb @@ -1220,6 +1220,7 @@ begin Pragma_Export_Value | Pragma_Export_Valued_Procedure | Pragma_Extend_System | + Pragma_Extensions_Visible | Pragma_External | Pragma_External_Name_Casing | Pragma_Favor_Top_Level | diff --git a/gcc/ada/sem_ch13.adb b/gcc/ada/sem_ch13.adb index 15e232be336..2546533432c 100644 --- a/gcc/ada/sem_ch13.adb +++ b/gcc/ada/sem_ch13.adb @@ -2256,6 +2256,21 @@ package body Sem_Ch13 is Insert_Pragma (Aitem); goto Continue; + -- Aspect Extensions_Visible is never delayed because it is + -- equivalent to a source pragma which appears after the + -- related subprogram. + + when Aspect_Extensions_Visible => + Make_Aitem_Pragma + (Pragma_Argument_Associations => New_List ( + Make_Pragma_Argument_Association (Loc, + Expression => Relocate_Node (Expr))), + Pragma_Name => Name_Extensions_Visible); + + Decorate (Aspect, Aitem); + Insert_Pragma (Aitem); + goto Continue; + -- Global -- Aspect Global is never delayed because it is equivalent to @@ -8817,6 +8832,7 @@ package body Sem_Ch13 is Aspect_Default_Initial_Condition | Aspect_Dimension | Aspect_Dimension_System | + Aspect_Extensions_Visible | Aspect_Implicit_Dereference | Aspect_Initial_Condition | Aspect_Initializes | diff --git a/gcc/ada/sem_ch3.adb b/gcc/ada/sem_ch3.adb index 5993bdb634d..78b4697b6b3 100644 --- a/gcc/ada/sem_ch3.adb +++ b/gcc/ada/sem_ch3.adb @@ -590,6 +590,12 @@ package body Sem_Ch3 is -- Propagate static and dynamic predicate flags from a parent to the -- subtype in a subtype declaration with and without constraints. + function Is_EVF_Procedure (Subp : Entity_Id) return Boolean; + -- Subsidiary to Check_Abstract_Overriding and Derive_Subprogram. + -- Determine whether subprogram Subp is a procedure subject to pragma + -- Extensions_Visible with value False and has at least one controlling + -- parameter of mode OUT. + function Is_Valid_Constraint_Kind (T_Kind : Type_Kind; Constraint_Kind : Node_Kind) return Boolean; @@ -3638,8 +3644,8 @@ package body Sem_Ch3 is and then Is_Access_Constant (Etype (E)) then Error_Msg_N - ("access to variable cannot be initialized " - & "with an access-to-constant expression", E); + ("access to variable cannot be initialized with an " + & "access-to-constant expression", E); end if; if not Assignment_OK (N) then @@ -3694,6 +3700,17 @@ package body Sem_Ch3 is Check_SPARK_05_Restriction ("initialization expression is not appropriate", E); end if; + + -- A formal parameter of a specific tagged type whose related + -- subprogram is subject to pragma Extensions_Visible with value + -- "False" cannot be implicitly converted to a class-wide type by + -- means of an initialization expression. + + if Is_Class_Wide_Type (T) and then Is_EVF_Expression (E) then + Error_Msg_N + ("formal parameter with Extensions_Visible False cannot be " + & "implicitly converted to class-wide type", E); + end if; end if; -- If the No_Streams restriction is set, check that the type of the @@ -9790,6 +9807,15 @@ package body Sem_Ch3 is then null; + -- A null extension is not obliged to override an inherited + -- procedure subject to pragma Extensions_Visible with value + -- False and at least one controlling OUT parameter. + + elsif Is_Null_Extension (T) + and then Is_EVF_Procedure (Subp) + then + null; + else Error_Msg_NE ("type must be declared abstract or & overridden", @@ -9833,6 +9859,16 @@ package body Sem_Ch3 is ("\& subprogram# is not visible", T, Subp); + -- Clarify the case where a non-null extension must + -- override inherited procedure subject to pragma + -- Extensions_Visible with value False and at least + -- one controlling OUT param. + + elsif Is_EVF_Procedure (E) then + Error_Msg_NE + ("\& # is subject to Extensions_Visible False", + T, Subp); + else Error_Msg_NE ("\& has been inherited from subprogram #", @@ -9902,6 +9938,20 @@ package body Sem_Ch3 is Error_Msg_Node_2 := Subp; Error_Msg_N ("nonabstract type& has abstract subprogram&!", T); end if; + + -- A subprogram subject to pragma Extensions_Visible with value + -- "True" cannot override a subprogram subject to the same pragma + -- with value "False". + + elsif Extensions_Visible_Status (Subp) = Extensions_Visible_True + and then Present (Overridden_Operation (Subp)) + and then Extensions_Visible_Status (Overridden_Operation (Subp)) = + Extensions_Visible_False + then + Error_Msg_Sloc := Sloc (Overridden_Operation (Subp)); + Error_Msg_N + ("subprogram & with Extensions_Visible True cannot override " + & "subprogram # with Extensions_Visible False", Subp); end if; -- Ada 2012 (AI05-0030): Perform checks related to pragma Implemented @@ -14254,8 +14304,7 @@ package body Sem_Ch3 is -- Start of processing for Derive_Subprogram begin - New_Subp := - New_Entity (Nkind (Parent_Subp), Sloc (Derived_Type)); + New_Subp := New_Entity (Nkind (Parent_Subp), Sloc (Derived_Type)); Set_Ekind (New_Subp, Ekind (Parent_Subp)); Set_Contract (New_Subp, Make_Contract (Sloc (New_Subp))); @@ -14490,6 +14539,10 @@ package body Sem_Ch3 is -- Ada 2005 (AI-228): Calculate the "require overriding" and "abstract" -- properties of the subprogram, as defined in RM-3.9.3(4/2-6/2). + -- A subprogram subject to pragma Extensions_Visible with value False + -- requires overriding if the subprogram has at least one controlling + -- OUT parameter. + elsif Ada_Version >= Ada_2005 and then (Is_Abstract_Subprogram (Alias (New_Subp)) or else (Is_Tagged_Type (Derived_Type) @@ -14500,7 +14553,8 @@ package body Sem_Ch3 is E_Anonymous_Access_Type and then Designated_Type (Etype (New_Subp)) = Derived_Type - and then not Is_Null_Extension (Derived_Type))) + and then not Is_Null_Extension (Derived_Type)) + or else Is_EVF_Procedure (Alias (New_Subp))) and then No (Actual_Subp) then if not Is_Tagged_Type (Derived_Type) @@ -17339,6 +17393,35 @@ package body Sem_Ch3 is (Subt, Has_Dynamic_Predicate_Aspect (Par)); end Inherit_Predicate_Flags; + ---------------------- + -- Is_EVF_Procedure -- + ---------------------- + + function Is_EVF_Procedure (Subp : Entity_Id) return Boolean is + Formal : Entity_Id; + + begin + -- Examine the formals of an Extensions_Visible False procedure looking + -- for a controlling OUT parameter. + + if Ekind (Subp) = E_Procedure + and then Extensions_Visible_Status (Subp) = Extensions_Visible_False + then + Formal := First_Formal (Subp); + while Present (Formal) loop + if Ekind (Formal) = E_Out_Parameter + and then Is_Controlling_Formal (Formal) + then + return True; + end if; + + Next_Formal (Formal); + end loop; + end if; + + return False; + end Is_EVF_Procedure; + ----------------------- -- Is_Null_Extension -- ----------------------- diff --git a/gcc/ada/sem_ch4.adb b/gcc/ada/sem_ch4.adb index 3f9fc98e78f..8b2a8050e2f 100644 --- a/gcc/ada/sem_ch4.adb +++ b/gcc/ada/sem_ch4.adb @@ -4944,14 +4944,13 @@ package body Sem_Ch4 is procedure Analyze_Type_Conversion (N : Node_Id) is Expr : constant Node_Id := Expression (N); - T : Entity_Id; + Typ : Entity_Id; begin - -- If Conversion_OK is set, then the Etype is already set, and the - -- only processing required is to analyze the expression. This is - -- used to construct certain "illegal" conversions which are not - -- allowed by Ada semantics, but can be handled OK by Gigi, see - -- Sinfo for further details. + -- If Conversion_OK is set, then the Etype is already set, and the only + -- processing required is to analyze the expression. This is used to + -- construct certain "illegal" conversions which are not allowed by Ada + -- semantics, but can be handled by Gigi, see Sinfo for further details. if Conversion_OK (N) then Analyze (Expr); @@ -4962,9 +4961,9 @@ package body Sem_Ch4 is -- checks to make sure the argument of the conversion is appropriate. Find_Type (Subtype_Mark (N)); - T := Entity (Subtype_Mark (N)); - Set_Etype (N, T); - Check_Fully_Declared (T, N); + Typ := Entity (Subtype_Mark (N)); + Set_Etype (N, Typ); + Check_Fully_Declared (Typ, N); Analyze_Expression (Expr); Validate_Remote_Type_Type_Conversion (N); @@ -5002,7 +5001,7 @@ package body Sem_Ch4 is elsif Nkind (Expr) = N_Character_Literal then if Ada_Version = Ada_83 then - Resolve (Expr, T); + Resolve (Expr, Typ); else Error_Msg_N ("argument of conversion cannot be character literal", N); @@ -5010,14 +5009,23 @@ package body Sem_Ch4 is end if; elsif Nkind (Expr) = N_Attribute_Reference - and then - Nam_In (Attribute_Name (Expr), Name_Access, - Name_Unchecked_Access, - Name_Unrestricted_Access) + and then Nam_In (Attribute_Name (Expr), Name_Access, + Name_Unchecked_Access, + Name_Unrestricted_Access) then Error_Msg_N ("argument of conversion cannot be access", N); Error_Msg_N ("\use qualified expression instead", N); end if; + + -- A formal parameter of a specific tagged type whose related subprogram + -- is subject to pragma Extensions_Visible with value "False" cannot + -- appear in a class-wide conversion. + + if Is_Class_Wide_Type (Typ) and then Is_EVF_Expression (Expr) then + Error_Msg_N + ("formal parameter with Extensions_Visible False cannot be " + & "converted to class-wide type", Expr); + end if; end Analyze_Type_Conversion; ---------------------- @@ -7603,7 +7611,7 @@ package body Sem_Ch4 is if not Is_Aliased_View (Obj) then Error_Msg_NE ("object in prefixed call to & must be aliased " - & " (RM-2005 4.3.1 (13))", Prefix (First_Actual), Subprog); + & "(RM-2005 4.3.1 (13))", Prefix (First_Actual), Subprog); end if; Analyze (First_Actual); diff --git a/gcc/ada/sem_ch6.adb b/gcc/ada/sem_ch6.adb index 2466e87cbba..6f28cbf4efa 100644 --- a/gcc/ada/sem_ch6.adb +++ b/gcc/ada/sem_ch6.adb @@ -4074,8 +4074,12 @@ package body Sem_Ch6 is if Nam = Name_Depends then Depends := Prag; - else pragma Assert (Nam = Name_Global); + + elsif Nam = Name_Global then Global := Prag; + + -- Note that pragma Extensions_Visible has already been analyzed + end if; Prag := Next_Pragma (Prag); @@ -5696,10 +5700,12 @@ package body Sem_Ch6 is and then Present (Alias (Overridden_Subp)) and then Comes_From_Source (Alias (Overridden_Subp)) then - Set_Overridden_Operation (Subp, Alias (Overridden_Subp)); + Set_Overridden_Operation (Subp, Alias (Overridden_Subp)); + Inherit_Subprogram_Contract (Subp, Alias (Overridden_Subp)); else - Set_Overridden_Operation (Subp, Overridden_Subp); + Set_Overridden_Operation (Subp, Overridden_Subp); + Inherit_Subprogram_Contract (Subp, Overridden_Subp); end if; end if; end if; @@ -9457,9 +9463,12 @@ package body Sem_Ch6 is -- E overrides the operation from which S is inherited. if Present (Alias (S)) then - Set_Overridden_Operation (E, Alias (S)); + Set_Overridden_Operation (E, Alias (S)); + Inherit_Subprogram_Contract (E, Alias (S)); + else - Set_Overridden_Operation (E, S); + Set_Overridden_Operation (E, S); + Inherit_Subprogram_Contract (E, S); end if; if Comes_From_Source (E) then @@ -9625,7 +9634,8 @@ package body Sem_Ch6 is and then Present (Alias (E)) and then Comes_From_Source (Alias (E)) then - Set_Overridden_Operation (S, Alias (E)); + Set_Overridden_Operation (S, Alias (E)); + Inherit_Subprogram_Contract (S, Alias (E)); -- Normal case of setting entity as overridden @@ -9637,7 +9647,8 @@ package body Sem_Ch6 is -- must check whether the target is an init_proc. elsif not Is_Init_Proc (S) then - Set_Overridden_Operation (S, E); + Set_Overridden_Operation (S, E); + Inherit_Subprogram_Contract (S, E); end if; Check_Overriding_Indicator (S, E, Is_Primitive => True); @@ -9660,7 +9671,8 @@ package body Sem_Ch6 is Is_Predefined_Dispatching_Operation (Alias (E))) then if Present (Alias (E)) then - Set_Overridden_Operation (S, Alias (E)); + Set_Overridden_Operation (S, Alias (E)); + Inherit_Subprogram_Contract (S, Alias (E)); end if; end if; diff --git a/gcc/ada/sem_prag.adb b/gcc/ada/sem_prag.adb index df8ec80b142..b5ca29e4a04 100644 --- a/gcc/ada/sem_prag.adb +++ b/gcc/ada/sem_prag.adb @@ -3842,9 +3842,9 @@ package body Sem_Prag is -- pragma is inserted in its declarative part. elsif From_Aspect_Specification (N) + and then Ent = Current_Scope and then Nkind (Unit_Declaration_Node (Ent)) = N_Subprogram_Body - and then Ent = Current_Scope then OK := True; @@ -5370,7 +5370,9 @@ package body Sem_Prag is --------------- procedure Chain_CTC (PO : Node_Id) is - S : Entity_Id; + Name : constant String_Id := Get_Name_From_CTC_Pragma (N); + CTC : Node_Id; + S : Entity_Id; begin if Nkind (PO) = N_Abstract_Subprogram_Declaration then @@ -5399,31 +5401,23 @@ package body Sem_Prag is -- There should not be another test-case with the same name -- associated to this subprogram. - declare - Name : constant String_Id := Get_Name_From_CTC_Pragma (N); - CTC : Node_Id; + CTC := Contract_Test_Cases (Contract (S)); + while Present (CTC) loop - begin - CTC := Contract_Test_Cases (Contract (S)); - while Present (CTC) loop + -- Omit pragma Contract_Cases because it does not introduce + -- a unique case name and it does not follow the syntax of + -- Test_Case. - -- Omit pragma Contract_Cases because it does not introduce - -- a unique case name and it does not follow the syntax of - -- Test_Case. - - if Pragma_Name (CTC) = Name_Contract_Cases then - null; + if Pragma_Name (CTC) = Name_Contract_Cases then + null; - elsif String_Equal - (Name, Get_Name_From_CTC_Pragma (CTC)) - then - Error_Msg_Sloc := Sloc (CTC); - Error_Pragma ("name for pragma% is already used#"); - end if; + elsif String_Equal (Name, Get_Name_From_CTC_Pragma (CTC)) then + Error_Msg_Sloc := Sloc (CTC); + Error_Pragma ("name for pragma% is already used#"); + end if; - CTC := Next_Pragma (CTC); - end loop; - end; + CTC := Next_Pragma (CTC); + end loop; -- Chain spec CTC pragma to list for subprogram @@ -10518,6 +10512,7 @@ package body Sem_Prag is begin GNAT_Pragma; + Check_No_Identifiers; Check_Arg_Count (1); Ensure_Aggregate_Form (Arg1); @@ -12292,6 +12287,7 @@ package body Sem_Prag is begin GNAT_Pragma; + Check_No_Identifiers; Check_Arg_Count (1); Ensure_Aggregate_Form (Arg1); @@ -12805,12 +12801,11 @@ package body Sem_Prag is Expression => Get_Pragma_Arg (Arg1))))); Analyze (N); - -------------------------------------- - -- Pragma_Default_Initial_Condition -- - -------------------------------------- + ------------------------------- + -- Default_Initial_Condition -- + ------------------------------- - -- pragma Pragma_Default_Initial_Condition - -- [ (null | boolean_EXPRESSION) ]; + -- pragma Default_Initial_Condition [ (null | boolean_EXPRESSION) ]; when Pragma_Default_Initial_Condition => Default_Init_Cond : declare Discard : Boolean; @@ -12819,6 +12814,7 @@ package body Sem_Prag is begin GNAT_Pragma; + Check_No_Identifiers; Check_At_Most_N_Arguments (1); Stmt := Prev (N); @@ -13883,6 +13879,135 @@ package body Sem_Prag is Ada_Version_Pragma := Empty; end if; + ------------------------ + -- Extensions_Visible -- + ------------------------ + + -- pragma Extensions_Visible [ (boolean_EXPRESSION) ]; + + when Pragma_Extensions_Visible => Extensions_Visible : declare + Context : constant Node_Id := Parent (N); + Expr : Node_Id; + Formal : Entity_Id; + Subp : Entity_Id; + Stmt : Node_Id; + + Has_OK_Formal : Boolean := False; + + begin + GNAT_Pragma; + Check_No_Identifiers; + Check_At_Most_N_Arguments (1); + + Subp := Empty; + Stmt := Prev (N); + while Present (Stmt) loop + + -- Skip prior pragmas, but check for duplicates + + if Nkind (Stmt) = N_Pragma then + if Pragma_Name (Stmt) = Pname then + Error_Msg_Name_1 := Pname; + Error_Msg_Sloc := Sloc (Stmt); + Error_Msg_N ("pragma % duplicates pragma declared#", N); + end if; + + -- Skip internally generated code + + elsif not Comes_From_Source (Stmt) then + null; + + -- The associated [generic] subprogram declaration has been + -- found, stop the search. + + elsif Nkind_In (Stmt, N_Generic_Subprogram_Declaration, + N_Subprogram_Declaration) + then + Subp := Defining_Entity (Stmt); + exit; + + -- The pragma does not apply to a legal construct, issue an + -- error and stop the analysis. + + else + Error_Pragma ("pragma % must apply to a subprogram"); + return; + end if; + + Stmt := Prev (Stmt); + end loop; + + -- When the pragma applies to a stand alone subprogram body, it + -- appears within the declarations of the body. In that case the + -- enclosing construct is the proper context. This check is done + -- after the traversal above to allow for duplicate detection. + + if Nkind (Context) = N_Subprogram_Body + and then No (Corresponding_Spec (Context)) + then + Subp := Defining_Entity (Context); + end if; + + if No (Subp) then + Error_Pragma ("pragma % must apply to a subprogram"); + return; + end if; + + -- Examine the formals of the related subprogram + + Formal := First_Formal (Subp); + while Present (Formal) loop + + -- At least one of the formals is of a specific tagged type, + -- the pragma is legal. + + if Is_Specific_Tagged_Type (Etype (Formal)) then + Has_OK_Formal := True; + exit; + + -- A generic subprogram with at least one formal of a private + -- type ensures the legality of the pragma because the actual + -- may be specifically tagged. Note that this is verified by + -- the check above at instantiation time. + + elsif Is_Private_Type (Etype (Formal)) + and then Is_Generic_Type (Etype (Formal)) + then + Has_OK_Formal := True; + exit; + end if; + + Next_Formal (Formal); + end loop; + + if not Has_OK_Formal then + Error_Msg_Name_1 := Pname; + Error_Msg_N (Fix_Error ("incorrect placement of pragma %"), N); + Error_Msg_NE + ("\subprogram & lacks parameter of specific tagged or " + & "generic private type", N, Subp); + return; + end if; + + -- Analyze the Boolean expression (if any) + + if Present (Arg1) then + Expr := Get_Pragma_Arg (Arg1); + + Analyze_And_Resolve (Expr, Standard_Boolean); + + if not Is_OK_Static_Expression (Expr) then + Error_Pragma_Arg + ("expression of pragma % must be static", Expr); + return; + end if; + end if; + + -- Chain the pragma on the contract for further processing + + Add_Contract_Item (N, Subp); + end Extensions_Visible; + -------------- -- External -- -------------- @@ -14713,6 +14838,7 @@ package body Sem_Prag is begin GNAT_Pragma; + Check_No_Identifiers; Check_Arg_Count (1); -- Ensure the proper placement of the pragma. Initial_Condition @@ -14827,6 +14953,7 @@ package body Sem_Prag is begin GNAT_Pragma; + Check_No_Identifiers; Check_Arg_Count (1); Ensure_Aggregate_Form (Arg1); @@ -15760,6 +15887,15 @@ package body Sem_Prag is when Pragma_License => GNAT_Pragma; + + -- Do not analyze pragma any further in CodePeer mode, to avoid + -- extraneous errors in this implementation-dependent pragma, + -- which has a different profile on other compilers. + + if CodePeer_Mode then + return; + end if; + Check_Arg_Count (1); Check_No_Identifiers; Check_Valid_Configuration_Pragma; @@ -17296,6 +17432,7 @@ package body Sem_Prag is begin GNAT_Pragma; + Check_No_Identifiers; Check_Arg_Count (1); -- Ensure the proper placement of the pragma. Part_Of must appear @@ -18675,6 +18812,7 @@ package body Sem_Prag is begin GNAT_Pragma; + Check_No_Identifiers; Check_Arg_Count (1); -- Ensure the proper placement of the pragma. Refined states must @@ -24918,6 +25056,7 @@ package body Sem_Prag is Pragma_Export_Valued_Procedure => -1, Pragma_Extend_System => -1, Pragma_Extensions_Allowed => 0, + Pragma_Extensions_Visible => 0, Pragma_External => -1, Pragma_Favor_Top_Level => 0, Pragma_External_Name_Casing => 0, diff --git a/gcc/ada/sem_res.adb b/gcc/ada/sem_res.adb index f300e7099b3..e26ff704908 100644 --- a/gcc/ada/sem_res.adb +++ b/gcc/ada/sem_res.adb @@ -3260,8 +3260,8 @@ package body Sem_Res is if not Is_Aliased_View (Act) then Error_Msg_NE - ("object in prefixed call to& must be aliased" - & " (RM-2005 4.3.1 (13))", + ("object in prefixed call to& must be aliased " + & "(RM-2005 4.3.1 (13))", Prefix (Act), Nam); end if; @@ -4418,6 +4418,22 @@ package body Sem_Res is end if; end if; + -- A formal parameter of a specific tagged type whose related + -- subprogram is subject to pragma Extensions_Visible with value + -- "False" cannot act as an actual in a subprogram with value + -- "True". + + if Is_EVF_Expression (A) + and then Extensions_Visible_Status (Nam) = + Extensions_Visible_True + then + Error_Msg_N + ("formal parameter with Extensions_Visible False cannot act " + & "as actual parameter", A); + Error_Msg_NE + ("\subprogram & has Extensions_Visible True", A, Nam); + end if; + Next_Actual (A); -- Case where actual is not present diff --git a/gcc/ada/sem_util.adb b/gcc/ada/sem_util.adb index 1f1128c2437..db8cdd717bd 100644 --- a/gcc/ada/sem_util.adb +++ b/gcc/ada/sem_util.adb @@ -251,8 +251,52 @@ package body Sem_Util is procedure Add_Contract_Item (Prag : Node_Id; Id : Entity_Id) is Items : constant Node_Id := Contract (Id); - Nam : Name_Id; - N : Node_Id; + + procedure Add_Classification; + -- Prepend Prag to the list of classifications + + procedure Add_Contract_Test_Case; + -- Prepend Prag to the list of contract and test cases + + procedure Add_Pre_Post_Condition; + -- Prepend Prag to the list of pre- and postconditions + + ------------------------ + -- Add_Classification -- + ------------------------ + + procedure Add_Classification is + begin + Set_Next_Pragma (Prag, Classifications (Items)); + Set_Classifications (Items, Prag); + end Add_Classification; + + ---------------------------- + -- Add_Contract_Test_Case -- + ---------------------------- + + procedure Add_Contract_Test_Case is + begin + Set_Next_Pragma (Prag, Contract_Test_Cases (Items)); + Set_Contract_Test_Cases (Items, Prag); + end Add_Contract_Test_Case; + + ---------------------------- + -- Add_Pre_Post_Condition -- + ---------------------------- + + procedure Add_Pre_Post_Condition is + begin + Set_Next_Pragma (Prag, Pre_Post_Conditions (Items)); + Set_Pre_Post_Conditions (Items, Prag); + end Add_Pre_Post_Condition; + + -- Local variables + + Nam : Name_Id; + PPC : Node_Id; + + -- Start of processing for Add_Contract_Item begin -- The related context must have a contract and the item to be added @@ -275,14 +319,12 @@ package body Sem_Util is Name_Initial_Condition, Name_Initializes) then - Set_Next_Pragma (Prag, Classifications (Items)); - Set_Classifications (Items, Prag); + Add_Classification; -- Indicator Part_Of must be associated with a package instantiation elsif Nam = Name_Part_Of and then Is_Generic_Instance (Id) then - Set_Next_Pragma (Prag, Classifications (Items)); - Set_Classifications (Items, Prag); + Add_Classification; -- The pragma is not a proper contract item @@ -295,8 +337,7 @@ package body Sem_Util is elsif Ekind (Id) = E_Package_Body then if Nam = Name_Refined_State then - Set_Next_Pragma (Prag, Classifications (Items)); - Set_Classifications (Items, Prag); + Add_Classification; -- The pragma is not a proper contract item @@ -308,6 +349,7 @@ package body Sem_Util is -- applicable pragmas are: -- Contract_Cases -- Depends + -- Extensions_Visible -- Global -- Post -- Postcondition @@ -319,51 +361,49 @@ package body Sem_Util is or else Is_Generic_Subprogram (Id) or else Is_Subprogram (Id) then - if Nam_In (Nam, Name_Precondition, - Name_Postcondition, - Name_Pre, - Name_Post, + if Nam_In (Nam, Name_Pre, + Name_Precondition, Name_uPre, + Name_Post, + Name_Postcondition, Name_uPost) then - -- Before we add a precondition or postcondition to the list, - -- make sure we do not have a disallowed duplicate, which can - -- happen if we use a pragma for Pre[_Class] or Post[_Class] - -- instead of the corresponding aspect. + -- Before we add a precondition or postcondition to the list, make + -- sure we do not have a disallowed duplicate, which can happen if + -- we use a pragma for Pre[_Class] or Post[_Class] instead of the + -- corresponding aspect. if not From_Aspect_Specification (Prag) - and then Nam_In (Nam, Name_Pre_Class, - Name_Pre, + and then Nam_In (Nam, Name_Pre, Name_uPre, - Name_Post_Class, Name_Post, - Name_uPost) + Name_Post_Class) then - N := Pre_Post_Conditions (Items); - while Present (N) loop - if not Split_PPC (N) - and then Original_Aspect_Name (N) = Nam + PPC := Pre_Post_Conditions (Items); + while Present (PPC) loop + if not Split_PPC (PPC) + and then Original_Aspect_Name (PPC) = Nam then - Error_Msg_Sloc := Sloc (N); + Error_Msg_Sloc := Sloc (PPC); Error_Msg_NE ("duplication of aspect for & given#", Prag, Id); return; - else - N := Next_Pragma (N); end if; + + PPC := Next_Pragma (PPC); end loop; end if; - Set_Next_Pragma (Prag, Pre_Post_Conditions (Items)); - Set_Pre_Post_Conditions (Items, Prag); + Add_Pre_Post_Condition; elsif Nam_In (Nam, Name_Contract_Cases, Name_Test_Case) then - Set_Next_Pragma (Prag, Contract_Test_Cases (Items)); - Set_Contract_Test_Cases (Items, Prag); + Add_Contract_Test_Case; - elsif Nam_In (Nam, Name_Depends, Name_Global) then - Set_Next_Pragma (Prag, Classifications (Items)); - Set_Classifications (Items, Prag); + elsif Nam_In (Nam, Name_Depends, + Name_Extensions_Visible, + Name_Global) + then + Add_Classification; -- The pragma is not a proper contract item @@ -377,13 +417,11 @@ package body Sem_Util is -- Refined_Post elsif Ekind (Id) = E_Subprogram_Body then - if Nam = Name_Refined_Post then - Set_Next_Pragma (Prag, Pre_Post_Conditions (Items)); - Set_Pre_Post_Conditions (Items, Prag); + if Nam_In (Nam, Name_Refined_Depends, Name_Refined_Global) then + Add_Classification; - elsif Nam_In (Nam, Name_Refined_Depends, Name_Refined_Global) then - Set_Next_Pragma (Prag, Classifications (Items)); - Set_Classifications (Items, Prag); + elsif Nam = Name_Refined_Post then + Add_Pre_Post_Condition; -- The pragma is not a proper contract item @@ -405,8 +443,7 @@ package body Sem_Util is Name_Effective_Writes, Name_Part_Of) then - Set_Next_Pragma (Prag, Classifications (Items)); - Set_Classifications (Items, Prag); + Add_Classification; -- The pragma is not a proper contract item @@ -5772,6 +5809,84 @@ package body Sem_Util is end if; end Explain_Limited_Type; + ------------------------------- + -- Extensions_Visible_Status -- + ------------------------------- + + function Extensions_Visible_Status + (Id : Entity_Id) return Extensions_Visible_Mode + is + Arg1 : Node_Id; + Expr : Node_Id; + Prag : Node_Id; + Subp : Entity_Id; + + begin + if SPARK_Mode = On then + + -- When a formal parameter is subject to Extensions_Visible, the + -- pragma is stored in the contract of related subprogram. + + if Is_Formal (Id) then + Subp := Scope (Id); + + elsif Is_Subprogram_Or_Generic_Subprogram (Id) then + Subp := Id; + + -- No other construct carries this pragma + + else + return Extensions_Visible_None; + end if; + + Prag := Get_Pragma (Subp, Pragma_Extensions_Visible); + + -- Extract the value from the Boolean expression (if any) + + if Present (Prag) then + Arg1 := First (Pragma_Argument_Associations (Prag)); + + -- The pragma appears with an argument + + if Present (Arg1) then + Expr := Get_Pragma_Arg (Arg1); + + -- Guarg against cascading errors when the argument of pragma + -- Extensions_Visible is not a valid static Boolean expression. + + if Error_Posted (Expr) then + return Extensions_Visible_None; + + elsif Is_True (Expr_Value (Expr)) then + return Extensions_Visible_True; + + else + return Extensions_Visible_False; + end if; + + -- Otherwise the pragma defaults to True + + else + return Extensions_Visible_True; + end if; + + -- Otherwise pragma Expresions_Visible is not inherited or directly + -- specified, its value defaults to "False". + + else + return Extensions_Visible_False; + end if; + + -- When SPARK_Mode is disabled, all semantic checks related to pragma + -- Extensions_Visible are disabled as well. Instead of saturating the + -- code with "if SPARK_Mode /= Off then" checks, the predicate returns + -- a default value. + + else + return Extensions_Visible_None; + end if; + end Extensions_Visible_Status; + ----------------- -- Find_Actual -- ----------------- @@ -9330,6 +9445,51 @@ package body Sem_Util is end if; end Inherit_Rep_Item_Chain; + --------------------------------- + -- Inherit_Subprogram_Contract -- + --------------------------------- + + procedure Inherit_Subprogram_Contract + (Subp : Entity_Id; + From_Subp : Entity_Id) + is + procedure Inherit_Pragma (Prag_Id : Pragma_Id); + -- Propagate a pragma denoted by Prag_Id from From_Subp's contract to + -- Subp's contract. + + -------------------- + -- Inherit_Pragma -- + -------------------- + + procedure Inherit_Pragma (Prag_Id : Pragma_Id) is + Prag : constant Node_Id := Get_Pragma (From_Subp, Prag_Id); + New_Prag : Node_Id; + + begin + -- A pragma cannot be part of more than one First_Pragma/Next_Pragma + -- chains, therefore the node must be replicated. The new pragma is + -- flagged is inherited for distrinction purposes. + + if Present (Prag) then + New_Prag := New_Copy_Tree (Prag); + Set_Is_Inherited (New_Prag); + + Add_Contract_Item (New_Prag, Subp); + end if; + end Inherit_Pragma; + + -- Start of processing for Inherit_Subprogram_Contract + + begin + -- Inheritance is carried out only when both subprograms have contracts + + if Present (Contract (Subp)) + and then Present (Contract (From_Subp)) + then + Inherit_Pragma (Pragma_Extensions_Visible); + end if; + end Inherit_Subprogram_Contract; + --------------------------------- -- Insert_Explicit_Dereference -- --------------------------------- @@ -10516,6 +10676,71 @@ package body Sem_Util is end if; end Is_Expression_Function; + ----------------------- + -- Is_EVF_Expression -- + ----------------------- + + function Is_EVF_Expression (N : Node_Id) return Boolean is + Orig_N : constant Node_Id := Original_Node (N); + Alt : Node_Id; + Expr : Node_Id; + Id : Entity_Id; + + begin + -- Detect a reference to a formal parameter of a specific tagged type + -- whose related subprogram is subject to pragma Expresions_Visible with + -- value "False". + + if Is_Entity_Name (N) and then Present (Entity (N)) then + Id := Entity (N); + + return + Is_Formal (Id) + and then Is_Specific_Tagged_Type (Etype (Id)) + and then Extensions_Visible_Status (Id) = + Extensions_Visible_False; + + -- A case expression is an EVF expression when it contains at least one + -- EVF dependent_expression. Note that a case expression may have been + -- expanded, hence the use of Original_Node. + + elsif Nkind (Orig_N) = N_Case_Expression then + Alt := First (Alternatives (Orig_N)); + while Present (Alt) loop + if Is_EVF_Expression (Expression (Alt)) then + return True; + end if; + + Next (Alt); + end loop; + + -- An if expression is an EVF expression when it contains at least one + -- EVF dependent_expression. Note that an if expression may have been + -- expanded, hence the use of Original_Node. + + elsif Nkind (Orig_N) = N_If_Expression then + Expr := Next (First (Expressions (Orig_N))); + while Present (Expr) loop + if Is_EVF_Expression (Expr) then + return True; + end if; + + Next (Expr); + end loop; + + -- A qualified expression or a type conversion is an EVF expression when + -- its operand is an EVF expression. + + elsif Nkind_In (N, N_Qualified_Expression, + N_Unchecked_Type_Conversion, + N_Type_Conversion) + then + return Is_EVF_Expression (Expression (N)); + end if; + + return False; + end Is_EVF_Expression; + -------------- -- Is_False -- -------------- @@ -11885,6 +12110,27 @@ package body Sem_Util is end if; end Is_SPARK_05_Object_Reference; + ----------------------------- + -- Is_Specific_Tagged_Type -- + ----------------------------- + + function Is_Specific_Tagged_Type (Typ : Entity_Id) return Boolean is + Full_Typ : Entity_Id; + + begin + -- Handle private types + + if Is_Private_Type (Typ) and then Present (Full_View (Typ)) then + Full_Typ := Full_View (Typ); + else + Full_Typ := Typ; + end if; + + -- A specific tagged type is a non-class-wide tagged type + + return Is_Tagged_Type (Full_Typ) and not Is_Class_Wide_Type (Full_Typ); + end Is_Specific_Tagged_Type; + ------------------ -- Is_Statement -- ------------------ diff --git a/gcc/ada/sem_util.ads b/gcc/ada/sem_util.ads index 4ddbe615762..55825575141 100644 --- a/gcc/ada/sem_util.ads +++ b/gcc/ada/sem_util.ads @@ -60,6 +60,7 @@ package Sem_Util is -- Depends -- Effective_Reads -- Effective_Writes + -- Extensions_Visible -- Global -- Initial_Condition -- Initializes @@ -566,6 +567,26 @@ package Sem_Util is -- continuation lines to the message explaining why type T is limited. -- Messages are placed at node N. + type Extensions_Visible_Mode is + (Extensions_Visible_None, + -- Extensions_Visible does not yield a mode when SPARK_Mode is off. This + -- value acts as a default in a non-SPARK compilation. + + Extensions_Visible_False, + -- A value of "False" signifies that Extensions_Visible is either + -- missing or the pragma is present and the value of its Boolean + -- expression is False. + + Extensions_Visible_True); + -- A value of "True" signifies that Extensions_Visible is present and + -- the value of its Boolean expression is True. + + function Extensions_Visible_Status + (Id : Entity_Id) return Extensions_Visible_Mode; + -- Given the entity of a subprogram or formal parameter subject to pragma + -- Extensions_Visible, return the Boolean value denoted by the expression + -- of the pragma. + procedure Find_Actual (N : Node_Id; Formal : out Entity_Id; @@ -1087,6 +1108,14 @@ package Sem_Util is -- Inherit the rep item chain of type From_Typ without clobbering any -- existing rep items on Typ's chain. Typ is the destination type. + procedure Inherit_Subprogram_Contract + (Subp : Entity_Id; + From_Subp : Entity_Id); + -- Inherit relevant contract items from source subprogram From_Subp. Subp + -- denotes the destination subprogram. The inherited items are: + -- Extensions_Visible + -- ??? it would be nice if this routine handles Pre'Class and Post'Class + procedure Insert_Explicit_Dereference (N : Node_Id); -- In a context that requires a composite or subprogram type and where a -- prefix is an access type, rewrite the access type node N (which is the @@ -1208,6 +1237,16 @@ package Sem_Util is -- expression function call, and should be inlined unconditionally. Also -- used to determine that such a call does not constitute a freeze point. + function Is_EVF_Expression (N : Node_Id) return Boolean; + -- Determine whether node N denotes a reference to a formal parameter of + -- a specific tagged type whose related subprogram is subject to pragma + -- Extensions_Visible with value "False". Several other constructs fall + -- under this category: + -- 1) A qualified expression whose operand is EVF + -- 2) A type conversion whose operand is EVF + -- 3) An if expression with at least one EVF dependent_expression + -- 4) A case expression with at least one EVF dependent_expression + function Is_False (U : Uint) return Boolean; pragma Inline (Is_False); -- The argument is a Uint value which is the Boolean'Pos value of a Boolean @@ -1345,6 +1384,9 @@ package Sem_Util is -- constants, formal parameters, and selected_components of those are -- valid objects in SPARK 2005. + function Is_Specific_Tagged_Type (Typ : Entity_Id) return Boolean; + -- Determine whether an arbitrary [private] type is specifically tagged + function Is_Statement (N : Node_Id) return Boolean; pragma Inline (Is_Statement); -- Check if the node N is a statement node. Note that this includes diff --git a/gcc/ada/sinfo.adb b/gcc/ada/sinfo.adb index 83023a48ebc..e9f6dd7ab9d 100644 --- a/gcc/ada/sinfo.adb +++ b/gcc/ada/sinfo.adb @@ -1889,6 +1889,14 @@ package body Sinfo is return Flag11 (N); end Is_In_Discriminant_Check; + function Is_Inherited + (N : Node_Id) return Boolean is + begin + pragma Assert (False + or else NT (N).Nkind = N_Pragma); + return Flag4 (N); + end Is_Inherited; + function Is_Machine_Number (N : Node_Id) return Boolean is begin @@ -5078,6 +5086,14 @@ package body Sinfo is Set_Flag11 (N, Val); end Set_Is_In_Discriminant_Check; + procedure Set_Is_Inherited + (N : Node_Id; Val : Boolean := True) is + begin + pragma Assert (False + or else NT (N).Nkind = N_Pragma); + Set_Flag4 (N, Val); + end Set_Is_Inherited; + procedure Set_Is_Machine_Number (N : Node_Id; Val : Boolean := True) is begin diff --git a/gcc/ada/sinfo.ads b/gcc/ada/sinfo.ads index 613760e15f3..7a3bc6ff016 100644 --- a/gcc/ada/sinfo.ads +++ b/gcc/ada/sinfo.ads @@ -1573,6 +1573,10 @@ package Sinfo is -- discriminant check has a correct value cannot be performed in this -- case (or the discriminant check may be optimized away). + -- Is_Inherited (Flag4-Sem) + -- This flag is set in an N_Pragma node that appears in a N_Contract node + -- to indicate that the pragma has been inherited from a parent context. + -- Is_Machine_Number (Flag11-Sem) -- This flag is set in an N_Real_Literal node to indicate that the value -- is a machine number. This avoids some unnecessary cases of converting @@ -2384,11 +2388,12 @@ package Sinfo is -- Next_Rep_Item (Node5-Sem) -- Class_Present (Flag6) set if from Aspect with 'Class -- From_Aspect_Specification (Flag13-Sem) + -- Import_Interface_Present (Flag16-Sem) + -- Is_Checked (Flag11-Sem) -- Is_Delayed_Aspect (Flag14-Sem) -- Is_Disabled (Flag15-Sem) -- Is_Ignored (Flag9-Sem) - -- Is_Checked (Flag11-Sem) - -- Import_Interface_Present (Flag16-Sem) + -- Is_Inherited (Flag4-Sem) -- Split_PPC (Flag17) set if corresponding aspect had Split_PPC set -- Uneval_Old_Accept (Flag7-Sem) -- Uneval_Old_Warn (Flag18-Sem) @@ -9229,6 +9234,9 @@ package Sinfo is function Is_In_Discriminant_Check (N : Node_Id) return Boolean; -- Flag11 + function Is_Inherited + (N : Node_Id) return Boolean; -- Flag4 + function Is_Machine_Number (N : Node_Id) return Boolean; -- Flag11 @@ -10246,6 +10254,9 @@ package Sinfo is procedure Set_Is_In_Discriminant_Check (N : Node_Id; Val : Boolean := True); -- Flag11 + procedure Set_Is_Inherited + (N : Node_Id; Val : Boolean := True); -- Flag4 + procedure Set_Is_Machine_Number (N : Node_Id; Val : Boolean := True); -- Flag11 @@ -12629,6 +12640,7 @@ package Sinfo is pragma Inline (Is_Folded_In_Parser); pragma Inline (Is_Ignored); pragma Inline (Is_In_Discriminant_Check); + pragma Inline (Is_Inherited); pragma Inline (Is_Machine_Number); pragma Inline (Is_Null_Loop); pragma Inline (Is_Overloaded); @@ -12963,6 +12975,7 @@ package Sinfo is pragma Inline (Set_Is_Folded_In_Parser); pragma Inline (Set_Is_Ignored); pragma Inline (Set_Is_In_Discriminant_Check); + pragma Inline (Set_Is_Inherited); pragma Inline (Set_Is_Machine_Number); pragma Inline (Set_Is_Null_Loop); pragma Inline (Set_Is_Overloaded); diff --git a/gcc/ada/snames.ads-tmpl b/gcc/ada/snames.ads-tmpl index cd68f11376c..42a9984a1c4 100644 --- a/gcc/ada/snames.ads-tmpl +++ b/gcc/ada/snames.ads-tmpl @@ -494,6 +494,7 @@ package Snames is Name_Export_Procedure : constant Name_Id := N + $; -- GNAT Name_Export_Value : constant Name_Id := N + $; -- GNAT Name_Export_Valued_Procedure : constant Name_Id := N + $; -- GNAT + Name_Extensions_Visible : constant Name_Id := N + $; -- GNAT Name_External : constant Name_Id := N + $; -- GNAT Name_Finalize_Storage_Only : constant Name_Id := N + $; -- GNAT Name_Global : constant Name_Id := N + $; -- GNAT @@ -1828,6 +1829,7 @@ package Snames is Pragma_Export_Procedure, Pragma_Export_Value, Pragma_Export_Valued_Procedure, + Pragma_Extensions_Visible, Pragma_External, Pragma_Finalize_Storage_Only, Pragma_Global, -- 2.30.2