From 539ca5ec98443a3140523337f1dc131fd709f17a Mon Sep 17 00:00:00 2001 From: Arnaud Charlet Date: Mon, 18 Apr 2016 12:17:17 +0200 Subject: [PATCH] [multiple changes] 2016-04-18 Ed Schonberg * sem_ch6.adb (Analyze_Subprogram_Body_Helper): In GNATprove mode, collect inherited class-wide conditions to generate the corresponding pragmas. * sem_prag.ads (Build_Pragma_Check_Equivalent): Moved from contracts * contracts.adb (Collect_Inherited_Class_Wide_Conditions): New procedure for overriding subprograms, used to generate the pragmas corresponding to an inherited class- wide pre- or postcondition. * sem_prag.adb (Build_Pragma_Check_Equivalent): moved here from contracts.adb (Replace_Condition_Entities): Subsidiary Build_Pragma_Check_Equivalent, to implement the proper semantics of inherited class-wide conditions, as given in AI12-0113. (Process_Class_Wide_Condition): Removed. (Collect_Inherited_Class_Wide_Conditions): Iterate over pragmas in contract of subprogram, to collect inherited class-wide conditions. (Build_Pragma_Check_Equivalent): Moved to sem_prag.adb 2016-04-18 Yannick Moy * a-calend.adb (Ada.Calendar): Mark package body as SPARK_Mode Off. * a-calend.ads (Ada.Calendar): Mark package spec as SPARK_Mode and add synchronous external abstract state Clock_Time. From-SVN: r235113 --- gcc/ada/ChangeLog | 25 +++ gcc/ada/a-calend.adb | 6 +- gcc/ada/a-calend.ads | 17 +- gcc/ada/contracts.adb | 158 -------------- gcc/ada/sem_ch6.adb | 11 + gcc/ada/sem_prag.adb | 498 +++++++++++++++++++++++++++++------------- gcc/ada/sem_prag.ads | 17 ++ 7 files changed, 418 insertions(+), 314 deletions(-) diff --git a/gcc/ada/ChangeLog b/gcc/ada/ChangeLog index c8e9141ff32..3e329a87b49 100644 --- a/gcc/ada/ChangeLog +++ b/gcc/ada/ChangeLog @@ -1,3 +1,28 @@ +2016-04-18 Ed Schonberg + + * sem_ch6.adb (Analyze_Subprogram_Body_Helper): In GNATprove + mode, collect inherited class-wide conditions to generate the + corresponding pragmas. + * sem_prag.ads (Build_Pragma_Check_Equivalent): Moved from contracts + * contracts.adb (Collect_Inherited_Class_Wide_Conditions): New + procedure for overriding subprograms, used to generate the pragmas + corresponding to an inherited class- wide pre- or postcondition. + * sem_prag.adb (Build_Pragma_Check_Equivalent): moved here + from contracts.adb (Replace_Condition_Entities): Subsidiary + Build_Pragma_Check_Equivalent, to implement the proper semantics + of inherited class-wide conditions, as given in AI12-0113. + (Process_Class_Wide_Condition): Removed. + (Collect_Inherited_Class_Wide_Conditions): Iterate over pragmas + in contract of subprogram, to collect inherited class-wide + conditions. + (Build_Pragma_Check_Equivalent): Moved to sem_prag.adb + +2016-04-18 Yannick Moy + + * a-calend.adb (Ada.Calendar): Mark package body as SPARK_Mode Off. + * a-calend.ads (Ada.Calendar): Mark package spec as + SPARK_Mode and add synchronous external abstract state Clock_Time. + 2016-04-18 Yannick Moy * sem_res.adb (Resolve_Call): Prevent inlining of diff --git a/gcc/ada/a-calend.adb b/gcc/ada/a-calend.adb index 9fcc2996702..f5076f23277 100644 --- a/gcc/ada/a-calend.adb +++ b/gcc/ada/a-calend.adb @@ -6,7 +6,7 @@ -- -- -- B o d y -- -- -- --- Copyright (C) 1992-2014, Free Software Foundation, Inc. -- +-- Copyright (C) 1992-2015, Free Software Foundation, Inc. -- -- -- -- GNAT is free software; you can redistribute it and/or modify it under -- -- terms of the GNU General Public License as published by the Free Soft- -- @@ -35,7 +35,9 @@ with Interfaces.C; with System.OS_Primitives; -package body Ada.Calendar is +package body Ada.Calendar with + SPARK_Mode => Off +is -------------------------- -- Implementation Notes -- diff --git a/gcc/ada/a-calend.ads b/gcc/ada/a-calend.ads index 55efe115f5d..0eed8badf49 100644 --- a/gcc/ada/a-calend.ads +++ b/gcc/ada/a-calend.ads @@ -6,7 +6,7 @@ -- -- -- S p e c -- -- -- --- Copyright (C) 1992-2014, Free Software Foundation, Inc. -- +-- Copyright (C) 1992-2015, Free Software Foundation, Inc. -- -- -- -- This specification is derived from the Ada Reference Manual for use with -- -- GNAT. The copyright notice above, and the license provisions that follow -- @@ -33,7 +33,12 @@ -- -- ------------------------------------------------------------------------------ -package Ada.Calendar is +package Ada.Calendar with + SPARK_Mode, + Abstract_State => (Clock_Time with Synchronous, + External => (Async_Readers, + Async_Writers)) +is type Time is private; @@ -49,7 +54,9 @@ package Ada.Calendar is subtype Day_Duration is Duration range 0.0 .. 86_400.0; - function Clock return Time; + function Clock return Time with + Volatile_Function, + Global => Clock_Time; -- The returned time value is the number of nanoseconds since the start -- of Ada time (1901-01-01 00:00:00.0 UTC). If leap seconds are enabled, -- the result will contain all elapsed leap seconds since the start of @@ -108,6 +115,10 @@ package Ada.Calendar is Time_Error : exception; private + -- Mark private part as SPARK_Mode Off to avoid accounting for variable + -- Invalid_Time_Zone_Offset in abstract state. + pragma SPARK_Mode (Off); + pragma Inline (Clock); pragma Inline (Year); diff --git a/gcc/ada/contracts.adb b/gcc/ada/contracts.adb index ebaecc09512..4eb6d26adba 100644 --- a/gcc/ada/contracts.adb +++ b/gcc/ada/contracts.adb @@ -1432,15 +1432,6 @@ package body Contracts is -- of statements to be checked on exit. Parameter Result is the entity -- of parameter _Result when Subp_Id denotes a function. - function Build_Pragma_Check_Equivalent - (Prag : Node_Id; - Subp_Id : Entity_Id := Empty; - Inher_Id : Entity_Id := Empty) return Node_Id; - -- Transform a [refined] pre- or postcondition denoted by Prag into an - -- equivalent pragma Check. When the pre- or postcondition is inherited, - -- the routine corrects the references of all formals of Inher_Id to - -- point to the formals of Subp_Id. - procedure Process_Contract_Cases (Stmts : in out List_Id); -- Process pragma Contract_Cases. This routine prepends items to the -- body declarations and appends items to list Stmts. @@ -1860,155 +1851,6 @@ package body Contracts is Analyze (Proc_Bod); end Build_Postconditions_Procedure; - ----------------------------------- - -- Build_Pragma_Check_Equivalent -- - ----------------------------------- - - function Build_Pragma_Check_Equivalent - (Prag : Node_Id; - Subp_Id : Entity_Id := Empty; - Inher_Id : Entity_Id := Empty) return Node_Id - is - function Suppress_Reference (N : Node_Id) return Traverse_Result; - -- Detect whether node N references a formal parameter subject to - -- pragma Unreferenced. If this is the case, set Comes_From_Source - -- to False to suppress the generation of a reference when analyzing - -- N later on. - - ------------------------ - -- Suppress_Reference -- - ------------------------ - - function Suppress_Reference (N : Node_Id) return Traverse_Result is - Formal : Entity_Id; - - begin - if Is_Entity_Name (N) and then Present (Entity (N)) then - Formal := Entity (N); - - -- The formal parameter is subject to pragma Unreferenced. - -- Prevent the generation of a reference by resetting the - -- Comes_From_Source flag. - - if Is_Formal (Formal) - and then Has_Pragma_Unreferenced (Formal) - then - Set_Comes_From_Source (N, False); - end if; - end if; - - return OK; - end Suppress_Reference; - - procedure Suppress_References is - new Traverse_Proc (Suppress_Reference); - - -- Local variables - - Loc : constant Source_Ptr := Sloc (Prag); - Prag_Nam : constant Name_Id := Pragma_Name (Prag); - Check_Prag : Node_Id; - Formals_Map : Elist_Id; - Inher_Formal : Entity_Id; - Msg_Arg : Node_Id; - Nam : Name_Id; - Subp_Formal : Entity_Id; - - -- Start of processing for Build_Pragma_Check_Equivalent - - begin - Formals_Map := No_Elist; - - -- When the pre- or postcondition is inherited, map the formals of - -- the inherited subprogram to those of the current subprogram. - - if Present (Inher_Id) then - pragma Assert (Present (Subp_Id)); - - Formals_Map := New_Elmt_List; - - -- Create a relation => - - Inher_Formal := First_Formal (Inher_Id); - Subp_Formal := First_Formal (Subp_Id); - while Present (Inher_Formal) and then Present (Subp_Formal) loop - Append_Elmt (Inher_Formal, Formals_Map); - Append_Elmt (Subp_Formal, Formals_Map); - - Next_Formal (Inher_Formal); - Next_Formal (Subp_Formal); - end loop; - end if; - - -- Copy the original pragma while performing substitutions (if - -- applicable). - - Check_Prag := - New_Copy_Tree - (Source => Prag, - Map => Formals_Map, - New_Scope => Current_Scope); - - -- Mark the pragma as being internally generated and reset the - -- Analyzed flag. - - Set_Analyzed (Check_Prag, False); - Set_Comes_From_Source (Check_Prag, False); - - -- The tree of the original pragma may contain references to the - -- formal parameters of the related subprogram. At the same time - -- the corresponding body may mark the formals as unreferenced: - - -- procedure Proc (Formal : ...) - -- with Pre => Formal ...; - - -- procedure Proc (Formal : ...) is - -- pragma Unreferenced (Formal); - -- ... - - -- This creates problems because all pragma Check equivalents are - -- analyzed at the end of the body declarations. Since all source - -- references have already been accounted for, reset any references - -- to such formals in the generated pragma Check equivalent. - - Suppress_References (Check_Prag); - - if Present (Corresponding_Aspect (Prag)) then - Nam := Chars (Identifier (Corresponding_Aspect (Prag))); - else - Nam := Prag_Nam; - end if; - - -- Convert the copy into pragma Check by correcting the name and - -- adding a check_kind argument. - - Set_Pragma_Identifier - (Check_Prag, Make_Identifier (Loc, Name_Check)); - - Prepend_To (Pragma_Argument_Associations (Check_Prag), - Make_Pragma_Argument_Association (Loc, - Expression => Make_Identifier (Loc, Nam))); - - -- Update the error message when the pragma is inherited - - if Present (Inher_Id) then - Msg_Arg := Last (Pragma_Argument_Associations (Check_Prag)); - - if Chars (Msg_Arg) = Name_Message then - String_To_Name_Buffer (Strval (Expression (Msg_Arg))); - - -- Insert "inherited" to improve the error message - - if Name_Buffer (1 .. 8) = "failed p" then - Insert_Str_In_Name_Buffer ("inherited ", 8); - Set_Strval (Expression (Msg_Arg), String_From_Name_Buffer); - end if; - end if; - end if; - - return Check_Prag; - end Build_Pragma_Check_Equivalent; - ---------------------------- -- Process_Contract_Cases -- ---------------------------- diff --git a/gcc/ada/sem_ch6.adb b/gcc/ada/sem_ch6.adb index a0a75b2ef8d..c1e57471c79 100644 --- a/gcc/ada/sem_ch6.adb +++ b/gcc/ada/sem_ch6.adb @@ -3754,6 +3754,17 @@ package body Sem_Ch6 is Build_Body_To_Inline (N, Spec_Id); end if; + -- When generating code, inherited pre/postconditions are handled + -- when expanding the corresponding contract. If GNATprove mode we + -- must process them when the body is analyzed. + + if GNATprove_Mode + and then Present (Spec_Id) + and then Present (Overridden_Operation (Spec_Id)) + then + Collect_Inherited_Class_Wide_Conditions (Spec_Id, N); + end if; + -- Ada 2005 (AI-262): In library subprogram bodies, after the analysis -- of the specification we have to install the private withed units. -- This holds for child units as well. diff --git a/gcc/ada/sem_prag.adb b/gcc/ada/sem_prag.adb index 1d64de503f4..01f498847bf 100644 --- a/gcc/ada/sem_prag.adb +++ b/gcc/ada/sem_prag.adb @@ -23141,151 +23141,6 @@ package body Sem_Prag is (N : Node_Id; Freeze_Id : Entity_Id := Empty) is - procedure Process_Class_Wide_Condition - (Expr : Node_Id; - Spec_Id : Entity_Id; - Subp_Decl : Node_Id); - -- Replace the type of all references to the controlling formal of - -- subprogram Spec_Id found in expression Expr with the corresponding - -- class-wide type. Subp_Decl is the subprogram [body] declaration - -- where the pragma resides. - - ---------------------------------- - -- Process_Class_Wide_Condition -- - ---------------------------------- - - procedure Process_Class_Wide_Condition - (Expr : Node_Id; - Spec_Id : Entity_Id; - Subp_Decl : Node_Id) - is - Disp_Typ : constant Entity_Id := Find_Dispatching_Type (Spec_Id); - - ACW : Entity_Id := Empty; - -- Access to Disp_Typ'Class, created if there is a controlling formal - -- that is an access parameter. - - function Access_Class_Wide_Type return Entity_Id; - -- If expression Expr contains a reference to a controlling access - -- parameter, create an access to Disp_Typ'Class for the necessary - -- conversions if one does not exist. - - function Replace_Type (N : Node_Id) return Traverse_Result; - -- ARM 6.1.1: Within the expression for a Pre'Class or Post'Class - -- aspect for a primitive subprogram of a tagged type Disp_Typ, a - -- name that denotes a formal parameter of type Disp_Typ is treated - -- as having type Disp_Typ'Class. Similarly, a name that denotes a - -- formal access parameter of type access-to-Disp_Typ is interpreted - -- as with type access-to-Disp_Typ'Class. This ensures the expression - -- is well defined for a primitive subprogram of a type descended - -- from Disp_Typ. - - ---------------------------- - -- Access_Class_Wide_Type -- - ---------------------------- - - function Access_Class_Wide_Type return Entity_Id is - Loc : constant Source_Ptr := Sloc (N); - - begin - if No (ACW) then - ACW := Make_Temporary (Loc, 'T'); - - Insert_Before_And_Analyze (Subp_Decl, - Make_Full_Type_Declaration (Loc, - Defining_Identifier => ACW, - Type_Definition => - Make_Access_To_Object_Definition (Loc, - Subtype_Indication => - New_Occurrence_Of (Class_Wide_Type (Disp_Typ), Loc), - All_Present => True))); - - Freeze_Before (Subp_Decl, ACW); - end if; - - return ACW; - end Access_Class_Wide_Type; - - ------------------ - -- Replace_Type -- - ------------------ - - function Replace_Type (N : Node_Id) return Traverse_Result is - Context : constant Node_Id := Parent (N); - Loc : constant Source_Ptr := Sloc (N); - CW_Typ : Entity_Id := Empty; - Ent : Entity_Id; - Typ : Entity_Id; - - begin - if Is_Entity_Name (N) - and then Present (Entity (N)) - and then Is_Formal (Entity (N)) - then - Ent := Entity (N); - Typ := Etype (Ent); - - -- Do not perform the type replacement for selector names in - -- parameter associations. These carry an entity for reference - -- purposes, but semantically they are just identifiers. - - if Nkind (Context) = N_Type_Conversion then - null; - - elsif Nkind (Context) = N_Parameter_Association - and then Selector_Name (Context) = N - then - null; - - elsif Typ = Disp_Typ then - CW_Typ := Class_Wide_Type (Typ); - - elsif Is_Access_Type (Typ) - and then Designated_Type (Typ) = Disp_Typ - then - CW_Typ := Access_Class_Wide_Type; - end if; - - if Present (CW_Typ) then - Rewrite (N, - Make_Type_Conversion (Loc, - Subtype_Mark => New_Occurrence_Of (CW_Typ, Loc), - Expression => New_Occurrence_Of (Ent, Loc))); - Set_Etype (N, CW_Typ); - end if; - end if; - - return OK; - end Replace_Type; - - procedure Replace_Types is new Traverse_Proc (Replace_Type); - - -- Start of processing for Process_Class_Wide_Condition - - begin - -- The subprogram subject to Pre'Class/Post'Class does not have a - -- dispatching type, therefore the aspect/pragma is illegal. - - if No (Disp_Typ) then - Error_Msg_Name_1 := Original_Aspect_Pragma_Name (N); - - if From_Aspect_Specification (N) then - Error_Msg_N - ("aspect % can only be specified for a primitive operation " - & "of a tagged type", Corresponding_Aspect (N)); - - -- The pragma is a source construct - - else - Error_Msg_N - ("pragma % can only be specified for a primitive operation " - & "of a tagged type", N); - end if; - end if; - - Replace_Types (Expr); - end Process_Class_Wide_Condition; - -- Local variables Subp_Decl : constant Node_Id := Find_Related_Declaration_Or_Body (N); @@ -23295,6 +23150,7 @@ package body Sem_Prag is Save_Ghost_Mode : constant Ghost_Mode_Type := Ghost_Mode; Errors : Nat; + Disp_Typ : Entity_Id; Restore_Scope : Boolean := False; -- Start of processing for Analyze_Pre_Post_Condition_In_Decl_Part @@ -23340,13 +23196,29 @@ package body Sem_Prag is Contract_Freeze_Error (Spec_Id, Freeze_Id); end if; - -- For a class-wide condition, a reference to a controlling formal must - -- be interpreted as having the class-wide type (or an access to such) - -- so that the inherited condition can be properly applied to any - -- overriding operation (see ARM12 6.6.1 (7)). - if Class_Present (N) then - Process_Class_Wide_Condition (Expr, Spec_Id, Subp_Decl); + + -- Verify that a class-wide condition is legal, i.e. the operation + -- is a primitive of a tagged type. + + Disp_Typ := Find_Dispatching_Type (Spec_Id); + + if No (Disp_Typ) then + Error_Msg_Name_1 := Original_Aspect_Pragma_Name (N); + + if From_Aspect_Specification (N) then + Error_Msg_N + ("aspect % can only be specified for a primitive operation " + & "of a tagged type", Corresponding_Aspect (N)); + + -- The pragma is a source construct + + else + Error_Msg_N + ("pragma % can only be specified for a primitive operation " + & "of a tagged type", N); + end if; + end if; end if; if Restore_Scope then @@ -26164,6 +26036,294 @@ package body Sem_Prag is return False; end Appears_In; + ----------------------------------- + -- Build_Pragma_Check_Equivalent -- + ----------------------------------- + + function Build_Pragma_Check_Equivalent + (Prag : Node_Id; + Subp_Id : Entity_Id := Empty; + Inher_Id : Entity_Id := Empty) return Node_Id + is + function Suppress_Reference (N : Node_Id) return Traverse_Result; + -- Detect whether node N references a formal parameter subject to + -- pragma Unreferenced. If this is the case, set Comes_From_Source + -- to False to suppress the generation of a reference when analyzing + -- N later on. + + ------------------------ + -- Suppress_Reference -- + ------------------------ + + function Suppress_Reference (N : Node_Id) return Traverse_Result is + Formal : Entity_Id; + + begin + if Is_Entity_Name (N) and then Present (Entity (N)) then + Formal := Entity (N); + + -- The formal parameter is subject to pragma Unreferenced. + -- Prevent the generation of a reference by resetting the + -- Comes_From_Source flag. + + if Is_Formal (Formal) + and then Has_Pragma_Unreferenced (Formal) + then + Set_Comes_From_Source (N, False); + end if; + end if; + + return OK; + end Suppress_Reference; + + procedure Suppress_References is + new Traverse_Proc (Suppress_Reference); + + -- Local variables + + Loc : constant Source_Ptr := Sloc (Prag); + Prag_Nam : constant Name_Id := Pragma_Name (Prag); + Check_Prag : Node_Id; + Formals_Map : Elist_Id; + Inher_Formal : Entity_Id; + Msg_Arg : Node_Id; + Nam : Name_Id; + Subp_Formal : Entity_Id; + + function Replace_Entity (N : Node_Id) return Traverse_Result; + -- Replace reference to formal of inherited operation or to primitive + -- operation of root type, with corresponding entity for derived type. + + -------------------- + -- Replace_Entity -- + -------------------- + + function Replace_Entity (N : Node_Id) return Traverse_Result + is + Elmt : Elmt_Id; + New_E : Entity_Id; + + begin + if Nkind (N) = N_Identifier + and then Present (Entity (N)) + and then + (Is_Formal (Entity (N)) or else Is_Subprogram (Entity (N))) + and then + (Nkind (Parent (N)) /= N_Attribute_Reference + or else Attribute_Name (Parent (N)) /= Name_Class) + then + -- The replacement does not apply to dispatching calls within + -- the condition, but only to calls whose static tag is that + -- of the parent type. + + if Is_Subprogram (Entity (N)) + and then Nkind (Parent (N)) = N_Function_Call + and then Present (Controlling_Argument (Parent (N))) + then + return OK; + end if; + + -- Loop to find out if entity has a renaming + + New_E := Empty; + Elmt := First_Elmt (Formals_Map); + while Present (Elmt) loop + if Node (Elmt) = Entity (N) then + New_E := Node (Next_Elmt (Elmt)); + exit; + end if; + + Next_Elmt (Elmt); + end loop; + + if Present (New_E) then + Rewrite (N, New_Occurrence_Of (New_E, Sloc (N))); + end if; + end if; + + if not Is_Abstract_Subprogram (Inher_Id) + and then Nkind (N) = N_Function_Call + and then Present (Entity (Name (N))) + and then Is_Abstract_Subprogram (Entity (Name (N))) + then + Error_Msg_N ("cannot call abstract subprogram", N); + + -- The whole expression will be reanalyzed + + elsif Nkind (N) in N_Has_Etype then + Set_Analyzed (N, False); + end if; + + return OK; + end Replace_Entity; + + procedure Replace_Condition_Entities is + new Traverse_Proc (Replace_Entity); + + -- Start of processing for Build_Pragma_Check_Equivalent + + begin + Formals_Map := No_Elist; + + -- When the pre- or postcondition is inherited, map the formals of + -- the inherited subprogram to those of the current subprogram. + -- In addition, map primitive operations of the parent type into the + -- corresponding primitive operations of the descendant. + + if Present (Inher_Id) then + pragma Assert (Present (Subp_Id)); + + Formals_Map := New_Elmt_List; + + -- Create a mapping => + + Inher_Formal := First_Formal (Inher_Id); + Subp_Formal := First_Formal (Subp_Id); + while Present (Inher_Formal) and then Present (Subp_Formal) loop + Append_Elmt (Inher_Formal, Formals_Map); + Append_Elmt (Subp_Formal, Formals_Map); + + Next_Formal (Inher_Formal); + Next_Formal (Subp_Formal); + end loop; + + -- Map primitive operations of the parent type into the corresponding + -- operations of the descendant. The descendant type might not be + -- frozen yet, so we cannot use the dispatch table directly. + + declare + T : constant Entity_Id := Find_Dispatching_Type (Subp_Id); + Old_T : constant Entity_Id := Find_Dispatching_Type (Inher_Id); + D : Node_Id; + E : Entity_Id; + Old_E : Entity_Id; + + begin + D := First (List_Containing (Unit_Declaration_Node (Subp_Id))); + + -- Look for primitive operations of the current type that have + -- overridden an operation of the type related to the original + -- class-wide precondition. There may be several intermediate + -- overridings between them. + + while Present (D) loop + if Nkind (D) = N_Subprogram_Declaration then + E := Defining_Entity (D); + if Is_Subprogram (E) + and then Present (Overridden_Operation (E)) + and then Find_Dispatching_Type (E) = T + then + Old_E := Overridden_Operation (E); + while Present (Overridden_Operation (Old_E)) + and then Scope (Old_E) /= Scope (Inher_Id) + loop + Old_E := Overridden_Operation (Old_E); + end loop; + + Append_Elmt (Old_E, Formals_Map); + Append_Elmt (E, Formals_Map); + end if; + end if; + + Next (D); + end loop; + + E := First_Entity (Scope (Subp_Id)); + while Present (E) loop + if not Comes_From_Source (E) + and then Ekind (E) = E_Function + and then Present (Alias (E)) + then + Old_E := Alias (E); + while Present (Alias (Old_E)) + and then Scope (Old_E) /= Scope (Inher_Id) + loop + Old_E := Alias (Old_E); + end loop; + + Append_Elmt (Old_E, Formals_Map); + Append_Elmt (E, Formals_Map); + end if; + Next_Entity (E); + end loop; + + if Formals_Map /= No_Elist then + Append_Elmt (Old_T, Formals_Map); + Append_Elmt (T, Formals_Map); + end if; + end; + end if; + + -- Copy the original pragma while performing substitutions (if + -- applicable). + + Check_Prag := New_Copy_Tree (Source => Prag); + + if Formals_Map /= No_Elist then + Replace_Condition_Entities (Check_Prag); + end if; + + -- Mark the pragma as being internally generated and reset the + -- Analyzed flag. + + Set_Analyzed (Check_Prag, False); + Set_Comes_From_Source (Check_Prag, False); + Set_Class_Present (Check_Prag, False); + + -- The tree of the original pragma may contain references to the + -- formal parameters of the related subprogram. At the same time + -- the corresponding body may mark the formals as unreferenced: + + -- procedure Proc (Formal : ...) + -- with Pre => Formal ...; + + -- procedure Proc (Formal : ...) is + -- pragma Unreferenced (Formal); + -- ... + + -- This creates problems because all pragma Check equivalents are + -- analyzed at the end of the body declarations. Since all source + -- references have already been accounted for, reset any references + -- to such formals in the generated pragma Check equivalent. + + Suppress_References (Check_Prag); + + if Present (Corresponding_Aspect (Prag)) then + Nam := Chars (Identifier (Corresponding_Aspect (Prag))); + else + Nam := Prag_Nam; + end if; + + -- Convert the copy into pragma Check by correcting the name and + -- adding a check_kind argument. + + Set_Pragma_Identifier + (Check_Prag, Make_Identifier (Loc, Name_Check)); + + Prepend_To (Pragma_Argument_Associations (Check_Prag), + Make_Pragma_Argument_Association (Loc, + Expression => Make_Identifier (Loc, Nam))); + + -- Update the error message when the pragma is inherited + + if Present (Inher_Id) then + Msg_Arg := Last (Pragma_Argument_Associations (Check_Prag)); + + if Chars (Msg_Arg) = Name_Message then + String_To_Name_Buffer (Strval (Expression (Msg_Arg))); + + -- Insert "inherited" to improve the error message + + if Name_Buffer (1 .. 8) = "failed p" then + Insert_Str_In_Name_Buffer ("inherited ", 8); + Set_Strval (Expression (Msg_Arg), String_From_Name_Buffer); + end if; + end if; + end if; + + return Check_Prag; + end Build_Pragma_Check_Equivalent; + ----------------------------- -- Check_Applicable_Policy -- ----------------------------- @@ -26626,6 +26786,42 @@ package body Sem_Prag is end loop; end Check_State_And_Constituent_Use; + --------------------------------------------- + -- Collect_Inherited_Class_Wide_Conditions -- + --------------------------------------------- + + procedure Collect_Inherited_Class_Wide_Conditions + (Subp : Entity_Id; + Bod : Node_Id) + is + Parent_Subp : constant Entity_Id := Overridden_Operation (Subp); + Prags : constant Node_Id := Contract (Parent_Subp); + Prag : Node_Id; + + begin + -- Iterate over the contract to find inherited class-wide pre- and + -- postconditions. + + if Present (Prags) then + Prag := Pre_Post_Conditions (Prags); + + while Present (Prag) loop + if Pragma_Name (Prag) = Name_Precondition + or else Pragma_Name (Prag) = Name_Postcondition + then + if No (Declarations (Bod)) then + Set_Declarations (Bod, Empty_List); + end if; + + Append (Build_Pragma_Check_Equivalent (Prag, Subp, Parent_Subp), + To => Declarations (Bod)); + end if; + + Prag := Next_Pragma (Prag); + end loop; + end if; + end Collect_Inherited_Class_Wide_Conditions; + --------------------------------------- -- Collect_Subprogram_Inputs_Outputs -- --------------------------------------- diff --git a/gcc/ada/sem_prag.ads b/gcc/ada/sem_prag.ads index 3bc2f65ae92..063e7df528f 100644 --- a/gcc/ada/sem_prag.ads +++ b/gcc/ada/sem_prag.ads @@ -244,6 +244,16 @@ package Sem_Prag is procedure Analyze_Test_Case_In_Decl_Part (N : Node_Id); -- Perform preanalysis of pragma Test_Case + function Build_Pragma_Check_Equivalent + (Prag : Node_Id; + Subp_Id : Entity_Id := Empty; + Inher_Id : Entity_Id := Empty) return Node_Id; + -- Transform a [refined] pre- or postcondition denoted by Prag into an + -- equivalent pragma Check. When the pre- or postcondition is inherited, + -- the routine replaces the references of all formals of Inher_Id and + -- primitive operations of its controlling type by references to the + -- corresponding entities of Subp_Id and the descendant type. + procedure Check_Applicable_Policy (N : Node_Id); -- N is either an N_Aspect or an N_Pragma node. There are two cases. If -- the name of the aspect or pragma is not one of those recognized as @@ -301,6 +311,13 @@ package Sem_Prag is -- state, variable or package instantiation denoted by Item_Id requires the -- use of indicator/option Part_Of. If this is the case, emit an error. + procedure Collect_Inherited_Class_Wide_Conditions + (Subp : Entity_Id; + Bod : Node_Id); + -- When analyzing an overriding subprogram, check whether the overridden + -- operations have class-wide pre/postconditions, and generate the + -- corresponding pragmas. + procedure Collect_Subprogram_Inputs_Outputs (Subp_Id : Entity_Id; Synthesize : Boolean := False; -- 2.30.2