From: charlet Date: Mon, 14 Oct 2013 12:34:33 +0000 (+0000) Subject: 2013-10-14 Hristian Kirtchev X-Git-Tag: upstream/4.9.2~3711 X-Git-Url: http://review.tizen.org/git/?a=commitdiff_plain;h=d4e369ad61a93fa5cfddca3be50370465f817580;p=platform%2Fupstream%2Flinaro-gcc.git 2013-10-14 Hristian Kirtchev * aspects.adb: Add an entry in table Canonical_Aspect for Initializes. * aspects.ads: Add entries in tables Aspect_Id, Aspect_Argument, Aspect_Names and Aspect_Delay for Initializes. * atree.ads, atree.adb (Ekind_In): New seven argument versions of the routines. * einfo.adb: Remove Refined_State_Pragma from the list of node usage. Finalizer is now at position 28. (Contract): Package and package bodies now have a contract. (Finalizer): Update the assertion and node usage. (Get_Pragma): Update the Is_CDG flag to include Abstract_State, Initializes and Refined_State. (Refined_State_Pragma): Removed. (Set_Contract): Package and package bodies now have a contract. (Set_Finalizer): Update the assertion and node usage. (Set_Refined_State_Pragma): Removed. (Write_Field8_Name): Remove the output for Refined_State_Pragma. (Write_Field24_Name): Remove the output for Finalizer. Package and package bodies now have a contract. (Write_Field28_Name): Add output for Finalizer. * einfo.ads: Update the documentation and usage in entities of attribute Contract. Update the node position and usage in entities of attribute Finalizer. Remove the documentation and usage in entities for attribute Refined_State_Pragma. (Refined_State_Pragma): Removed along with pragma Inline. (Set_Refined_State_Pragma): Removed along with pragma Inline. * par-prag.adb: Add Initializes to the pragmas that do not require special processing by the parser. * sem_ch3.adb (Analyze_Declarations): Add local variable Prag. Update the retrieval of pragma Refined_State. Analyze aspect/pragma Initializes at the end of the visible declarations of the related package. * sem_ch6.adb (Analyze_Subprogram_Body_Contract): Add local variables Ref_Depends and Ref_Global. Analyze pragmas Refined_Global and Refined_Depends in that order. (Analyze_Subprogram_Contract): Add local variables Depends and Global. Analyze pragmas Global and Depends in that order. * sem_ch7.adb (Analyze_Package_Body_Helper): Package bodies now have a contract. Move the analysis of the aspect specifications after the defining entity has been decorated. (Analyze_Package_Declaration): Packages now have a contract. Move the analysis of the aspect specifications after the defining entity has been decorated. * sem_ch12.adb (Analyze_Generic_Package_Declaration): Packages now have contracts. * sem_ch13.adb (Analyze_Pragma): Code cleanup for aspect Abstract_State. Add processing for aspect Initializes. (Check_Aspect_At_Freeze_Point): Add an entry for Initializes. * sem_prag.adb: Use Get_Pragma_Arg to extract the expression of a pragma argument. Add an entry in table Sig_Flags for Initializes. (Analyze_Initializes_In_Decl_Part): New routine. (Analyze_Pragma): Check the declaration order of pragmas Abstract_State and Initializes. Abstract_State is now part of the package contract. Analyze pragma Initializes. Check for duplicate Refined_State pragma. Refined_State is now part of the package contract. (Check_Declaration_Order): New routine. (Check_Test_Case): Alphabetized. * sem_prag.ads (Analyze_Initializes_In_Decl_Part): New routine. * sem_util.adb (Add_Contract_Item): Rename formal Subp_Id to Id. This routine can now support contracts on packages and package bodies. * sem_util.ads (Add_Contract_Item): Rename formal Subp_Id to Id. Update comment on usage. * sinfo.ads: Update the usage of N_Contract nodes. * snames.ads-tmpl: Add predefined name Initializes. Add new pragma id for Initializes. git-svn-id: svn+ssh://gcc.gnu.org/svn/gcc/trunk@203522 138bc75d-0d04-0410-961f-82ee72b054a4 --- diff --git a/gcc/ada/ChangeLog b/gcc/ada/ChangeLog index 2ec3be4..f9c6ace 100644 --- a/gcc/ada/ChangeLog +++ b/gcc/ada/ChangeLog @@ -1,3 +1,79 @@ +2013-10-14 Hristian Kirtchev + + * aspects.adb: Add an entry in table Canonical_Aspect for + Initializes. + * aspects.ads: Add entries in tables Aspect_Id, Aspect_Argument, + Aspect_Names and Aspect_Delay for Initializes. + * atree.ads, atree.adb (Ekind_In): New seven argument versions of the + routines. + * einfo.adb: Remove Refined_State_Pragma from the list of node + usage. Finalizer is now at position 28. + (Contract): Package + and package bodies now have a contract. + (Finalizer): Update + the assertion and node usage. + (Get_Pragma): Update the Is_CDG + flag to include Abstract_State, Initializes and Refined_State. + (Refined_State_Pragma): Removed. + (Set_Contract): Package and + package bodies now have a contract. + (Set_Finalizer): Update the + assertion and node usage. + (Set_Refined_State_Pragma): Removed. + (Write_Field8_Name): Remove the output for Refined_State_Pragma. + (Write_Field24_Name): Remove the output for Finalizer. Package + and package bodies now have a contract. + (Write_Field28_Name): + Add output for Finalizer. + * einfo.ads: Update the documentation and usage in entities + of attribute Contract. Update the node position and usage in + entities of attribute Finalizer. Remove the documentation + and usage in entities for attribute Refined_State_Pragma. + (Refined_State_Pragma): Removed along with pragma Inline. + (Set_Refined_State_Pragma): Removed along with pragma Inline. + * par-prag.adb: Add Initializes to the pragmas that do not + require special processing by the parser. + * sem_ch3.adb (Analyze_Declarations): Add local variable + Prag. Update the retrieval of pragma Refined_State. Analyze + aspect/pragma Initializes at the end of the visible declarations + of the related package. + * sem_ch6.adb (Analyze_Subprogram_Body_Contract): + Add local variables Ref_Depends and Ref_Global. Analyze + pragmas Refined_Global and Refined_Depends in that order. + (Analyze_Subprogram_Contract): Add local variables Depends and + Global. Analyze pragmas Global and Depends in that order. + * sem_ch7.adb (Analyze_Package_Body_Helper): Package + bodies now have a contract. Move the analysis of the aspect + specifications after the defining entity has been decorated. + (Analyze_Package_Declaration): Packages now have a contract. Move + the analysis of the aspect specifications after the defining + entity has been decorated. + * sem_ch12.adb (Analyze_Generic_Package_Declaration): Packages + now have contracts. + * sem_ch13.adb (Analyze_Pragma): Code cleanup for aspect + Abstract_State. Add processing for aspect Initializes. + (Check_Aspect_At_Freeze_Point): Add an entry for Initializes. + * sem_prag.adb: Use Get_Pragma_Arg to extract the expression + of a pragma argument. Add an entry in table Sig_Flags for + Initializes. + (Analyze_Initializes_In_Decl_Part): New routine. + (Analyze_Pragma): Check the declaration order of pragmas + Abstract_State and Initializes. Abstract_State is now part of + the package contract. Analyze pragma Initializes. Check for + duplicate Refined_State pragma. Refined_State is now part of + the package contract. + (Check_Declaration_Order): New routine. + (Check_Test_Case): Alphabetized. + * sem_prag.ads (Analyze_Initializes_In_Decl_Part): New routine. + * sem_util.adb (Add_Contract_Item): Rename formal Subp_Id + to Id. This routine can now support contracts on packages and + package bodies. + * sem_util.ads (Add_Contract_Item): Rename formal Subp_Id to + Id. Update comment on usage. + * sinfo.ads: Update the usage of N_Contract nodes. + * snames.ads-tmpl: Add predefined name Initializes. Add new + pragma id for Initializes. + 2013-10-13 Nicolas Roche Eric Botcazou diff --git a/gcc/ada/aspects.adb b/gcc/ada/aspects.adb index 2aea7b3..b9f1a56 100644 --- a/gcc/ada/aspects.adb +++ b/gcc/ada/aspects.adb @@ -440,6 +440,7 @@ package body Aspects is Aspect_Independent_Components => Aspect_Independent_Components, Aspect_Inline => Aspect_Inline, Aspect_Inline_Always => Aspect_Inline, + Aspect_Initializes => Aspect_Initializes, Aspect_Input => Aspect_Input, Aspect_Interrupt_Handler => Aspect_Interrupt_Handler, Aspect_Interrupt_Priority => Aspect_Priority, diff --git a/gcc/ada/aspects.ads b/gcc/ada/aspects.ads index 15c6e4c..2325d97 100644 --- a/gcc/ada/aspects.ads +++ b/gcc/ada/aspects.ads @@ -96,6 +96,7 @@ package Aspects is Aspect_External_Tag, Aspect_Global, -- GNAT Aspect_Implicit_Dereference, + Aspect_Initializes, -- GNAT Aspect_Input, Aspect_Interrupt_Priority, Aspect_Invariant, -- GNAT @@ -309,6 +310,7 @@ package Aspects is Aspect_External_Tag => Expression, Aspect_Global => Expression, Aspect_Implicit_Dereference => Name, + Aspect_Initializes => Expression, Aspect_Input => Name, Aspect_Interrupt_Priority => Expression, Aspect_Invariant => Expression, @@ -398,6 +400,7 @@ package Aspects is Aspect_Independent_Components => Name_Independent_Components, Aspect_Inline => Name_Inline, Aspect_Inline_Always => Name_Inline_Always, + Aspect_Initializes => Name_Initializes, Aspect_Input => Name_Input, Aspect_Interrupt_Handler => Name_Interrupt_Handler, Aspect_Interrupt_Priority => Name_Interrupt_Priority, @@ -597,6 +600,7 @@ package Aspects is Aspect_Independent_Components => Always_Delay, Aspect_Inline => Always_Delay, Aspect_Inline_Always => Always_Delay, + Aspect_Initializes => Always_Delay, Aspect_Input => Always_Delay, Aspect_Interrupt_Handler => Always_Delay, Aspect_Interrupt_Priority => Always_Delay, diff --git a/gcc/ada/atree.adb b/gcc/ada/atree.adb index a6105e2..a44a247 100644 --- a/gcc/ada/atree.adb +++ b/gcc/ada/atree.adb @@ -979,6 +979,26 @@ package body Atree is end Ekind_In; function Ekind_In + (T : Entity_Kind; + V1 : Entity_Kind; + V2 : Entity_Kind; + V3 : Entity_Kind; + V4 : Entity_Kind; + V5 : Entity_Kind; + V6 : Entity_Kind; + V7 : Entity_Kind) return Boolean + is + begin + return T = V1 or else + T = V2 or else + T = V3 or else + T = V4 or else + T = V5 or else + T = V6 or else + T = V7; + end Ekind_In; + + function Ekind_In (E : Entity_Id; V1 : Entity_Kind; V2 : Entity_Kind) return Boolean @@ -1033,6 +1053,20 @@ package body Atree is return Ekind_In (Ekind (E), V1, V2, V3, V4, V5, V6); end Ekind_In; + function Ekind_In + (E : Entity_Id; + V1 : Entity_Kind; + V2 : Entity_Kind; + V3 : Entity_Kind; + V4 : Entity_Kind; + V5 : Entity_Kind; + V6 : Entity_Kind; + V7 : Entity_Kind) return Boolean + is + begin + return Ekind_In (Ekind (E), V1, V2, V3, V4, V5, V6, V7); + end Ekind_In; + ------------------------ -- Set_Reporting_Proc -- ------------------------ diff --git a/gcc/ada/atree.ads b/gcc/ada/atree.ads index 123beb3..5465554 100644 --- a/gcc/ada/atree.ads +++ b/gcc/ada/atree.ads @@ -736,6 +736,16 @@ package Atree is V6 : Entity_Kind) return Boolean; function Ekind_In + (E : Entity_Id; + V1 : Entity_Kind; + V2 : Entity_Kind; + V3 : Entity_Kind; + V4 : Entity_Kind; + V5 : Entity_Kind; + V6 : Entity_Kind; + V7 : Entity_Kind) return Boolean; + + function Ekind_In (T : Entity_Kind; V1 : Entity_Kind; V2 : Entity_Kind) return Boolean; @@ -770,6 +780,16 @@ package Atree is V5 : Entity_Kind; V6 : Entity_Kind) return Boolean; + function Ekind_In + (T : Entity_Kind; + V1 : Entity_Kind; + V2 : Entity_Kind; + V3 : Entity_Kind; + V4 : Entity_Kind; + V5 : Entity_Kind; + V6 : Entity_Kind; + V7 : Entity_Kind) return Boolean; + pragma Inline (Ekind_In); -- Inline all above functions diff --git a/gcc/ada/einfo.adb b/gcc/ada/einfo.adb index fa0daa9..2c1a094 100644 --- a/gcc/ada/einfo.adb +++ b/gcc/ada/einfo.adb @@ -80,7 +80,6 @@ package body Einfo is -- Mechanism Uint8 (but returns Mechanism_Type) -- Normalized_First_Bit Uint8 -- Postcondition_Proc Node8 - -- Refined_State_Pragma Node8 -- Refinement_Constituents Elist8 -- Return_Applies_To Node8 -- First_Exit_Statement Node8 @@ -213,7 +212,6 @@ package body Einfo is -- Protection_Object Node23 -- Stored_Constraint Elist23 - -- Finalizer Node24 -- Related_Expression Node24 -- Contract Node24 @@ -238,6 +236,7 @@ package body Einfo is -- Wrapped_Entity Node27 -- Extra_Formals Node28 + -- Finalizer Node28 -- Initialization_Statements Node28 -- Underlying_Record_View Node28 @@ -1068,9 +1067,14 @@ package body Einfo is function Contract (Id : E) return N is begin pragma Assert - (Ekind_In (Id, E_Entry, E_Entry_Family, E_Subprogram_Body) - or else Is_Subprogram (Id) - or else Is_Generic_Subprogram (Id)); + (Ekind_In (Id, E_Entry, + E_Entry_Family, + E_Generic_Package, + E_Package, + E_Package_Body, + E_Subprogram_Body) + or else Is_Generic_Subprogram (Id) + or else Is_Subprogram (Id)); return Node24 (Id); end Contract; @@ -1180,10 +1184,8 @@ package body Einfo is function Finalizer (Id : E) return E is begin - pragma Assert - (Ekind (Id) = E_Package - or else Ekind (Id) = E_Package_Body); - return Node24 (Id); + pragma Assert (Ekind_In (Id, E_Package, E_Package_Body)); + return Node28 (Id); end Finalizer; function First_Entity (Id : E) return E is @@ -2656,12 +2658,6 @@ package body Einfo is return Node10 (Id); end Refined_State; - function Refined_State_Pragma (Id : E) return N is - begin - pragma Assert (Ekind (Id) = E_Package_Body); - return Node8 (Id); - end Refined_State_Pragma; - function Refinement_Constituents (Id : E) return L is begin pragma Assert (Ekind (Id) = E_Abstract_State); @@ -3666,9 +3662,15 @@ package body Einfo is procedure Set_Contract (Id : E; V : N) is begin pragma Assert - (Ekind_In (Id, E_Entry, E_Entry_Family, E_Subprogram_Body, E_Void) - or else Is_Subprogram (Id) - or else Is_Generic_Subprogram (Id)); + (Ekind_In (Id, E_Entry, + E_Entry_Family, + E_Generic_Package, + E_Package, + E_Package_Body, + E_Subprogram_Body, + E_Void) + or else Is_Generic_Subprogram (Id) + or else Is_Subprogram (Id)); Set_Node24 (Id, V); end Set_Contract; @@ -3779,10 +3781,8 @@ package body Einfo is procedure Set_Finalizer (Id : E; V : E) is begin - pragma Assert - (Ekind (Id) = E_Package - or else Ekind (Id) = E_Package_Body); - Set_Node24 (Id, V); + pragma Assert (Ekind_In (Id, E_Package, E_Package_Body)); + Set_Node28 (Id, V); end Set_Finalizer; procedure Set_First_Entity (Id : E; V : E) is @@ -5328,12 +5328,6 @@ package body Einfo is Set_Node10 (Id, V); end Set_Refined_State; - procedure Set_Refined_State_Pragma (Id : E; V : N) is - begin - pragma Assert (Ekind (Id) = E_Package_Body); - Set_Node8 (Id, V); - end Set_Refined_State_Pragma; - procedure Set_Refinement_Constituents (Id : E; V : L) is begin pragma Assert (Ekind (Id) = E_Abstract_State); @@ -6293,15 +6287,18 @@ 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_Depends or else Id = Pragma_Global or else + Id = Pragma_Initializes or else Id = Pragma_Refined_Depends or else - Id = Pragma_Refined_Global; + Id = Pragma_Refined_Global or else + Id = Pragma_Refined_State; Is_CTC : constant Boolean := Id = Pragma_Contract_Cases or else Id = Pragma_Test_Case; Is_PPC : constant Boolean := - Id = Pragma_Precondition or else + Id = Pragma_Precondition or else Id = Pragma_Postcondition; In_Contract : constant Boolean := Is_CDG or Is_CTC or Is_PPC; @@ -8339,9 +8336,6 @@ package body Einfo is when E_Procedure => Write_Str ("Postcondition_Proc"); - when E_Package_Body => - Write_Str ("Refined_State_Pragma"); - when E_Abstract_State => Write_Str ("Refinement_Constituents"); @@ -9055,10 +9049,6 @@ package body Einfo is procedure Write_Field24_Name (Id : Entity_Id) is begin case Ekind (Id) is - when E_Package | - E_Package_Body => - Write_Str ("Finalizer"); - when E_Constant | E_Variable | Type_Kind => @@ -9066,9 +9056,12 @@ package body Einfo is when E_Entry | E_Entry_Family | + E_Generic_Package | + E_Package | + E_Package_Body | E_Subprogram_Body | - Subprogram_Kind | - Generic_Subprogram_Kind => + Generic_Subprogram_Kind | + Subprogram_Kind => Write_Str ("Contract"); when others => @@ -9202,7 +9195,12 @@ package body Einfo is E_Subprogram_Type => Write_Str ("Extra_Formals"); - when E_Constant | E_Variable => + when E_Package | + E_Package_Body => + Write_Str ("Finalizer"); + + when E_Constant | + E_Variable => Write_Str ("Initialization_Statements"); when E_Record_Type => diff --git a/gcc/ada/einfo.ads b/gcc/ada/einfo.ads index 4843b9e..4895763 100644 --- a/gcc/ada/einfo.ads +++ b/gcc/ada/einfo.ads @@ -1022,9 +1022,10 @@ package Einfo is -- 'COUNT when it applies to a family member. -- Contract (Node24) --- Defined in entry and entry family entities, subprogram body entities, --- subprograms, and generic subprograms. Points to the contract of the --- entity, holding both preconditions, postconditions, and test cases. +-- Defined in entry, entry family, package, package body, subprogram and +-- subprogram body entities as well as their respective generic forms. +-- Points to the contract of the entity, holding various assertion items +-- and data classifiers. -- Entry_Parameters_Type (Node15) -- Defined in entries. Points to the access-to-record type that is @@ -1181,7 +1182,7 @@ package Einfo is -- the Finalize_Storage_Only pragma is required at each level of -- derivation. --- Finalizer (Node24) +-- Finalizer (Node28) -- Applies to package declarations and bodies. Contains the entity of the -- library-level program which finalizes all package-level controlled -- objects. @@ -3541,10 +3542,6 @@ package Einfo is -- Defined in abstract states and variables. Contains the entity of an -- ancestor state whose refinement mentions this item. --- Refined_State_Pragma (Node8) --- Defined in [generic] package bodies. Contains the pragma that refines --- all abstract states defined in the corresponding package declaration. - -- Refinement_Constituents (Elist8) -- Present in abstract state entities. Contains all the constituents that -- refine the state, in other words, all the hidden states that appear in @@ -5626,10 +5623,11 @@ package Einfo is -- Generic_Renamings (Elist23) (for an instance) -- Inner_Instances (Elist23) (generic case only) -- Limited_View (Node23) (non-generic/instance) - -- Finalizer (Node24) (non-generic case only) + -- Contract (Node24) -- Abstract_States (Elist25) -- Package_Instantiation (Node26) -- Current_Use_Clause (Node27) + -- Finalizer (Node28) (non-generic case only) -- SPARK_Mode_Pragmas (Node32) -- Delay_Subprogram_Descriptors (Flag50) -- Body_Needed_For_SAL (Flag40) @@ -5655,14 +5653,14 @@ package Einfo is -- Scope_Depth (synth) -- E_Package_Body - -- Refined_State_Pragma (Node8) -- Handler_Records (List10) (non-generic case only) -- Related_Instance (Node15) (non-generic case only) -- First_Entity (Node17) -- Spec_Entity (Node19) -- Last_Entity (Node20) -- Scope_Depth_Value (Uint22) - -- Finalizer (Node24) (non-generic case only) + -- Contract (Node24) + -- Finalizer (Node28) (non-generic case only) -- SPARK_Mode_Pragmas (Node32) -- Delay_Subprogram_Descriptors (Flag50) -- Has_Anonymous_Master (Flag253) @@ -6553,7 +6551,6 @@ package Einfo is function Referenced_As_LHS (Id : E) return B; function Referenced_As_Out_Parameter (Id : E) return B; function Refined_State (Id : E) return E; - function Refined_State_Pragma (Id : E) return E; function Refinement_Constituents (Id : E) return L; function Register_Exception_Call (Id : E) return N; function Related_Array_Object (Id : E) return E; @@ -7173,7 +7170,6 @@ package Einfo is procedure Set_Referenced_As_LHS (Id : E; V : B := True); procedure Set_Referenced_As_Out_Parameter (Id : E; V : B := True); procedure Set_Refined_State (Id : E; V : E); - procedure Set_Refined_State_Pragma (Id : E; V : N); procedure Set_Refinement_Constituents (Id : E; V : L); procedure Set_Register_Exception_Call (Id : E; V : N); procedure Set_Related_Array_Object (Id : E; V : E); @@ -7931,7 +7927,6 @@ package Einfo is pragma Inline (Referenced_As_LHS); pragma Inline (Referenced_As_Out_Parameter); pragma Inline (Refined_State); - pragma Inline (Refined_State_Pragma); pragma Inline (Refinement_Constituents); pragma Inline (Register_Exception_Call); pragma Inline (Related_Array_Object); @@ -8349,7 +8344,6 @@ package Einfo is pragma Inline (Set_Referenced_As_LHS); pragma Inline (Set_Referenced_As_Out_Parameter); pragma Inline (Set_Refined_State); - pragma Inline (Set_Refined_State_Pragma); pragma Inline (Set_Refinement_Constituents); pragma Inline (Set_Register_Exception_Call); pragma Inline (Set_Related_Array_Object); diff --git a/gcc/ada/par-prag.adb b/gcc/ada/par-prag.adb index aed45f9..22e79d7 100644 --- a/gcc/ada/par-prag.adb +++ b/gcc/ada/par-prag.adb @@ -1186,6 +1186,7 @@ begin Pragma_Independent | Pragma_Independent_Components | Pragma_Initialize_Scalars | + Pragma_Initializes | Pragma_Inline | Pragma_Inline_Always | Pragma_Inline_Generic | diff --git a/gcc/ada/sem_ch12.adb b/gcc/ada/sem_ch12.adb index df80232..d5c5ce7 100644 --- a/gcc/ada/sem_ch12.adb +++ b/gcc/ada/sem_ch12.adb @@ -3022,6 +3022,15 @@ package body Sem_Ch12 is Id := Defining_Entity (N); Generate_Definition (Id); + -- Expansion is not applied to generic units + + Start_Generic; + + Enter_Name (Id); + Set_Ekind (Id, E_Generic_Package); + Set_Etype (Id, Standard_Void_Type); + Set_Contract (Id, Make_Contract (Sloc (Id))); + -- Analyze aspects now, so that generated pragmas appear in the -- declarations before building and analyzing the generic copy. @@ -3029,13 +3038,6 @@ package body Sem_Ch12 is Analyze_Aspect_Specifications (N, Id); end if; - -- Expansion is not applied to generic units - - Start_Generic; - - Enter_Name (Id); - Set_Ekind (Id, E_Generic_Package); - Set_Etype (Id, Standard_Void_Type); Push_Scope (Id); Enter_Generic_Scope (Id); Set_Inner_Instances (Id, New_Elmt_List); @@ -3124,7 +3126,7 @@ package body Sem_Ch12 is Aspects : constant List_Id := Aspect_Specifications (N); begin Set_Has_Aspects (N, False); - Move_Aspects (New_N, N); + Move_Aspects (New_N, To => N); Set_Has_Aspects (Original_Node (N), False); Set_Aspect_Specifications (Original_Node (N), Aspects); end; @@ -4756,7 +4758,7 @@ package body Sem_Ch12 is -- pre/postconditions on the instance are analyzed below, in a -- separate step. - Move_Aspects (Act_Tree, Act_Decl); + Move_Aspects (Act_Tree, To => Act_Decl); Set_Categorization_From_Pragmas (Act_Decl); if Parent_Installed then diff --git a/gcc/ada/sem_ch13.adb b/gcc/ada/sem_ch13.adb index 71cc77e..29fc1c7 100644 --- a/gcc/ada/sem_ch13.adb +++ b/gcc/ada/sem_ch13.adb @@ -1883,22 +1883,20 @@ package body Sem_Ch13 is -- Abstract_State + -- Aspect Abstract_State introduces implicit declarations for + -- all state abstraction entities it defines. To emulate this + -- behavior, insert the pragma at the beginning of the visible + -- declarations of the related package so that it is analyzed + -- immediately. + when Aspect_Abstract_State => Abstract_State : declare Decls : List_Id; - Spec : Node_Id; begin - -- Aspect Abstract_State introduces implicit declarations - -- for all state abstraction entities it defines. To emulate - -- this behavior, insert the pragma at the beginning of the - -- visible declarations of the related package so that it is - -- analyzed immediately. - if Nkind_In (N, N_Generic_Package_Declaration, N_Package_Declaration) then - Spec := Specification (N); - Decls := Visible_Declarations (Spec); + Decls := Visible_Declarations (Specification (N)); Make_Aitem_Pragma (Pragma_Argument_Associations => New_List ( @@ -1959,6 +1957,44 @@ package body Sem_Ch13 is Insert_Delayed_Pragma (Aitem); goto Continue; + -- Initializes + + -- Aspect Initializes coverts the visible declarations of a + -- package. As such, it must be evaluated at the end of the + -- said declarations. + + when Aspect_Initializes => Initializes : declare + Decls : List_Id; + + begin + if Nkind_In (N, N_Generic_Package_Declaration, + N_Package_Declaration) + then + Decls := Visible_Declarations (Specification (N)); + + Make_Aitem_Pragma + (Pragma_Argument_Associations => New_List ( + Make_Pragma_Argument_Association (Loc, + Expression => Relocate_Node (Expr))), + Pragma_Name => Name_Initializes); + Decorate_Delayed_Aspect_And_Pragma (Aspect, Aitem); + + if No (Decls) then + Decls := New_List; + Set_Visible_Declarations (N, Decls); + end if; + + Prepend_To (Decls, Aitem); + + else + Error_Msg_NE + ("aspect & must apply to a package declaration", + Aspect, Id); + end if; + + goto Continue; + end Initializes; + -- SPARK_Mode when Aspect_SPARK_Mode => @@ -7708,6 +7744,7 @@ package body Sem_Ch13 is Aspect_Dimension | Aspect_Dimension_System | Aspect_Implicit_Dereference | + Aspect_Initializes | Aspect_Post | Aspect_Postcondition | Aspect_Pre | diff --git a/gcc/ada/sem_ch3.adb b/gcc/ada/sem_ch3.adb index 85872e1..b2e2a92 100644 --- a/gcc/ada/sem_ch3.adb +++ b/gcc/ada/sem_ch3.adb @@ -2086,6 +2086,7 @@ package body Sem_Ch3 is Context : Node_Id; Freeze_From : Entity_Id := Empty; Next_Decl : Node_Id; + Prag : Node_Id; Spec_Id : Entity_Id; -- Start of processing for Analyze_Declarations @@ -2196,24 +2197,38 @@ package body Sem_Ch3 is Decl := Next_Decl; end loop; - -- Analyze the state refinements within a package body now, after all - -- hidden states have been encountered and freely visible. Refinements - -- must be processed before pragmas Refined_Depends and Refined_Global - -- because the last two may mention constituents. - if Present (L) then Context := Parent (L); - if Nkind (Context) = N_Package_Body then + -- Analyze aspect/pragma Initializes of a package at the end of the + -- visible declarations as the aspect/pragma has visibility over the + -- said region. + + if Nkind (Context) = N_Package_Specification + and then L = Visible_Declarations (Context) + then + Spec_Id := Defining_Entity (Parent (Context)); + Prag := Get_Pragma (Spec_Id, Pragma_Initializes); + + if Present (Prag) then + Analyze_Initializes_In_Decl_Part (Prag); + end if; + + -- Analyze the state refinements within a package body now, after + -- all hidden states have been encountered and freely visible. + -- Refinements must be processed before pragmas Refined_Depends and + -- Refined_Global because the last two may mention constituents. + + elsif Nkind (Context) = N_Package_Body then Body_Id := Defining_Entity (Context); Spec_Id := Corresponding_Spec (Context); + Prag := Get_Pragma (Body_Id, Pragma_Refined_State); -- The analysis of pragma Refined_State detects whether the spec -- has abstract states available for refinement. - if Present (Refined_State_Pragma (Body_Id)) then - Analyze_Refined_State_In_Decl_Part - (Refined_State_Pragma (Body_Id)); + if Present (Prag) then + Analyze_Refined_State_In_Decl_Part (Prag); -- State refinement is required when the package declaration has -- abstract states. Null states are not considered. diff --git a/gcc/ada/sem_ch6.adb b/gcc/ada/sem_ch6.adb index acf1aeb..34d0a88 100644 --- a/gcc/ada/sem_ch6.adb +++ b/gcc/ada/sem_ch6.adb @@ -1976,11 +1976,11 @@ package body Sem_Ch6 is -------------------------------------- procedure Analyze_Subprogram_Body_Contract (Body_Id : Entity_Id) is - Body_Decl : constant Node_Id := Parent (Parent (Body_Id)); - Spec_Id : constant Entity_Id := Corresponding_Spec (Body_Decl); - Prag : Node_Id; - - Has_Refined_Global : Boolean := False; + Body_Decl : constant Node_Id := Parent (Parent (Body_Id)); + Spec_Id : constant Entity_Id := Corresponding_Spec (Body_Decl); + Prag : Node_Id; + Ref_Depends : Node_Id := Empty; + Ref_Global : Node_Id := Empty; begin -- When a subprogram body declaration is erroneous, its defining entity @@ -1991,22 +1991,30 @@ package body Sem_Ch6 is return; end if; + -- Locate and store pragmas Refined_Depends and Refined_Global since + -- their order of analysis matters. + Prag := Classifications (Contract (Body_Id)); while Present (Prag) loop if Pragma_Name (Prag) = Name_Refined_Depends then - Analyze_Refined_Depends_In_Decl_Part (Prag); + Ref_Depends := Prag; elsif Pragma_Name (Prag) = Name_Refined_Global then - Has_Refined_Global := True; - Analyze_Refined_Global_In_Decl_Part (Prag); + Ref_Global := Prag; end if; Prag := Next_Pragma (Prag); end loop; + -- Analyze Refined_Global first as Refined_Depends may mention items + -- classified in the global refinement. + + if Present (Ref_Global) then + Analyze_Refined_Global_In_Decl_Part (Ref_Global); + -- When the corresponding Global aspect/pragma references a state with -- visible refinement, the body requires Refined_Global. - if not Has_Refined_Global and then Present (Spec_Id) then + elsif Present (Spec_Id) then Prag := Get_Pragma (Spec_Id, Pragma_Global); if Present (Prag) and then Contains_Refined_State (Prag) then @@ -2015,6 +2023,13 @@ package body Sem_Ch6 is Body_Decl, Spec_Id); end if; end if; + + -- Refined_Depends must be analyzed after Refined_Global in order to see + -- the modes of all global refinements. + + if Present (Ref_Depends) then + Analyze_Refined_Depends_In_Decl_Part (Ref_Depends); + end if; end Analyze_Subprogram_Body_Contract; ------------------------------------ @@ -3570,17 +3585,16 @@ package body Sem_Ch6 is -- Local variables Items : constant Node_Id := Contract (Subp); - Error_CCase : Node_Id; - Error_Post : Node_Id; + Depends : Node_Id := Empty; + Error_CCase : Node_Id := Empty; + Error_Post : Node_Id := Empty; + Global : Node_Id := Empty; Nam : Name_Id; Prag : Node_Id; -- Start of processing for Analyze_Subprogram_Contract begin - Error_CCase := Empty; - Error_Post := Empty; - if Present (Items) then -- Analyze pre- and postconditions @@ -3635,14 +3649,27 @@ package body Sem_Ch6 is Nam := Pragma_Name (Prag); if Nam = Name_Depends then - Analyze_Depends_In_Decl_Part (Prag); - else - pragma Assert (Nam = Name_Global); - Analyze_Global_In_Decl_Part (Prag); + Depends := Prag; + else pragma Assert (Nam = Name_Global); + Global := Prag; end if; Prag := Next_Pragma (Prag); end loop; + + -- Analyze Global first as Depends may mention items classified in + -- the global categorization. + + if Present (Global) then + Analyze_Global_In_Decl_Part (Global); + end if; + + -- Depends must be analyzed after Global in order to see the modes of + -- all global items. + + if Present (Depends) then + Analyze_Depends_In_Decl_Part (Depends); + end if; end if; -- Emit an error when none of the postconditions or contract-cases diff --git a/gcc/ada/sem_ch7.adb b/gcc/ada/sem_ch7.adb index 5166830..d15add3 100644 --- a/gcc/ada/sem_ch7.adb +++ b/gcc/ada/sem_ch7.adb @@ -224,15 +224,10 @@ package body Sem_Ch7 is Body_Id := Defining_Entity (N); - if Has_Aspects (N) then - Analyze_Aspect_Specifications (N, Body_Id); - end if; + -- Body is body of package instantiation. Corresponding spec has already + -- been set. if Present (Corresponding_Spec (N)) then - - -- Body is body of package instantiation. Corresponding spec has - -- already been set. - Spec_Id := Corresponding_Spec (N); Pack_Decl := Unit_Declaration_Node (Spec_Id); @@ -315,6 +310,7 @@ package body Sem_Ch7 is Set_Ekind (Body_Id, E_Package_Body); Set_Body_Entity (Spec_Id, Body_Id); Set_Spec_Entity (Body_Id, Spec_Id); + Set_Contract (Body_Id, Make_Contract (Sloc (Body_Id))); -- Defining name for the package body is not a visible entity: Only the -- defining name for the declaration is visible. @@ -338,6 +334,10 @@ package body Sem_Ch7 is Set_Has_Completion (Spec_Id); Last_Spec_Entity := Last_Entity (Spec_Id); + if Has_Aspects (N) then + Analyze_Aspect_Specifications (N, Body_Id); + end if; + Push_Scope (Spec_Id); Set_Categorization_From_Pragmas (N); @@ -770,6 +770,21 @@ package body Sem_Ch7 is -- True when this package declaration is not a nested declaration begin + if Debug_Flag_C then + Write_Str ("==> package spec "); + Write_Name (Chars (Id)); + Write_Str (" from "); + Write_Location (Sloc (N)); + Write_Eol; + Indent; + end if; + + Generate_Definition (Id); + Enter_Name (Id); + Set_Ekind (Id, E_Package); + Set_Etype (Id, Standard_Void_Type); + Set_Contract (Id, Make_Contract (Sloc (Id))); + -- Analyze aspect specifications immediately, since we need to recognize -- things like Pure early enough to diagnose violations during analysis. @@ -788,20 +803,6 @@ package body Sem_Ch7 is return; end if; - if Debug_Flag_C then - Write_Str ("==> package spec "); - Write_Name (Chars (Id)); - Write_Str (" from "); - Write_Location (Sloc (N)); - Write_Eol; - Indent; - end if; - - Generate_Definition (Id); - Enter_Name (Id); - Set_Ekind (Id, E_Package); - Set_Etype (Id, Standard_Void_Type); - Push_Scope (Id); PF := Is_Pure (Enclosing_Lib_Unit_Entity); diff --git a/gcc/ada/sem_prag.adb b/gcc/ada/sem_prag.adb index 0bfcf0d..070d7cb 100644 --- a/gcc/ada/sem_prag.adb +++ b/gcc/ada/sem_prag.adb @@ -412,7 +412,7 @@ package body Sem_Prag is Subp_Decl := Find_Related_Subprogram (N); Subp_Id := Defining_Unit_Name (Specification (Subp_Decl)); - All_Cases := Expression (First (Pragma_Argument_Associations (N))); + All_Cases := Get_Pragma_Arg (First (Pragma_Argument_Associations (N))); -- Multiple contract cases appear in aggregate form @@ -1243,7 +1243,7 @@ package body Sem_Prag is Subp_Decl := Find_Related_Subprogram (N); Subp_Id := Defining_Unit_Name (Specification (Subp_Decl)); - Clause := Expression (First (Pragma_Argument_Associations (N))); + Clause := Get_Pragma_Arg (First (Pragma_Argument_Associations (N))); -- Empty dependency list @@ -1701,7 +1701,7 @@ package body Sem_Prag is Subp_Decl := Find_Related_Subprogram (N); Subp_Id := Defining_Unit_Name (Specification (Subp_Decl)); - List := Expression (First (Pragma_Argument_Associations (N))); + List := Get_Pragma_Arg (First (Pragma_Argument_Associations (N))); -- There is nothing to be done for a null global list @@ -1731,6 +1731,337 @@ package body Sem_Prag is end if; end Analyze_Global_In_Decl_Part; + -------------------------------------- + -- Analyze_Initializes_In_Decl_Part -- + -------------------------------------- + + procedure Analyze_Initializes_In_Decl_Part (N : Node_Id) is + Pack_Spec : constant Node_Id := Parent (N); + Pack_Id : constant Entity_Id := Defining_Entity (Parent (Pack_Spec)); + + Items_Seen : Elist_Id := No_Elist; + -- A list of all initialization items processed so far. This list is + -- used to detect duplicate items. + + Non_Null_Seen : Boolean := False; + Null_Seen : Boolean := False; + -- Flags used to check the legality of a null initialization list + + States_And_Vars : Elist_Id := No_Elist; + -- A list of all abstract states and variables declared in the visible + -- declarations of the related package. This list is used to detect the + -- legality of initialization items. + + procedure Analyze_Initialization_Item (Item : Node_Id); + -- Verify the legality of a single initialization item + + procedure Analyze_Initialization_Item_With_Inputs (Item : Node_Id); + -- Verify the legality of a single initialization item followed by a + -- list of input items. + + procedure Collect_States_And_Variables; + -- Inspect the visible declarations of the related package and gather + -- the entities of all abstract states and variables in States_And_Vars. + + --------------------------------- + -- Analyze_Initialization_Item -- + --------------------------------- + + procedure Analyze_Initialization_Item (Item : Node_Id) is + Item_Id : Entity_Id; + + begin + -- A package with null initialization list is not allowed to have + -- additional initializations. + + if Null_Seen then + Error_Msg_NE ("package & has null initialization", Item, Pack_Id); + + -- Null initialization list + + elsif Nkind (Item) = N_Null then + + -- Catch a case where a null initialization item appears in a list + -- of non-null items. + + if Non_Null_Seen then + Error_Msg_NE + ("package & has non-null initialization", Item, Pack_Id); + else + Null_Seen := True; + end if; + + -- Initialization item + + else + Non_Null_Seen := True; + + Analyze (Item); + + if Is_Entity_Name (Item) then + Item_Id := Entity (Item); + + if Ekind_In (Item_Id, E_Abstract_State, E_Variable) then + + -- The state or variable must be declared in the visible + -- declarations of the package. + + if not Contains (States_And_Vars, Item_Id) then + Error_Msg_Name_1 := Chars (Pack_Id); + Error_Msg_NE + ("initialization item & must appear in the visible " + & "declarations of package %", Item, Item_Id); + + -- Detect a duplicate use of the same initialization item + + elsif Contains (Items_Seen, Item_Id) then + Error_Msg_N ("duplicate initialization item", Item); + + -- The item is legal, add it to the list of processed states + -- and variables. + + else + Add_Item (Item_Id, Items_Seen); + end if; + + -- The item references something that is not a state or a + -- variable. + + else + Error_Msg_N + ("initialization item must denote variable or state", + Item); + end if; + + -- Some form of illegal construct masquerading as a name + + else + Error_Msg_N + ("initialization item must denote variable or state", Item); + end if; + end if; + end Analyze_Initialization_Item; + + --------------------------------------------- + -- Analyze_Initialization_Item_With_Inputs -- + --------------------------------------------- + + procedure Analyze_Initialization_Item_With_Inputs (Item : Node_Id) is + Inputs_Seen : Elist_Id := No_Elist; + -- A list of all inputs processed so far. This list is used to detect + -- duplicate uses of an input. + + Non_Null_Seen : Boolean := False; + Null_Seen : Boolean := False; + -- Flags used to check the legality of an input list + + procedure Analyze_Input_Item (Input : Node_Id); + -- Verify the legality of a single input item + + ------------------------ + -- Analyze_Input_Item -- + ------------------------ + + procedure Analyze_Input_Item (Input : Node_Id) is + Input_Id : Entity_Id; + + begin + -- An initialization item with null inputs is not allowed to have + -- assitional inputs. + + if Null_Seen then + Error_Msg_N ("item has null input list", Item); + + -- Null input list + + elsif Nkind (Input) = N_Null then + + -- Catch a case where a null input appears in a list of non- + -- null inpits. + + if Non_Null_Seen then + Error_Msg_N ("item has non-null input list", Item); + else + Null_Seen := True; + end if; + + -- Input item + + else + Non_Null_Seen := True; + + Analyze (Input); + + if Is_Entity_Name (Input) then + Input_Id := Entity (Input); + + if Ekind_In (Input_Id, E_Abstract_State, E_Variable) then + + -- The input cannot denote states or variables declared + -- within the visible declarations of the package. + + if Contains (States_And_Vars, Input_Id) then + Error_Msg_Name_1 := Chars (Pack_Id); + Error_Msg_NE + ("input item & cannot denote a visible variable or " + & "state of package %", Input, Input_Id); + + -- Detect a duplicate use of the same input item + + elsif Contains (Inputs_Seen, Input_Id) then + Error_Msg_N ("duplicate input item", Input); + + -- The input is legal, add it to the list of processed + -- inputs. + + else + Add_Item (Input_Id, Inputs_Seen); + end if; + + -- The input references something that is not a state or a + -- variable. + + else + Error_Msg_N + ("input item must denote variable or state", Input); + end if; + + -- Some form of illegal construct masquerading as a name + + else + Error_Msg_N + ("input item must denote variable or state", Input); + end if; + end if; + end Analyze_Input_Item; + + -- Local variables + + Inputs : constant Node_Id := Expression (Item); + Elmt : Node_Id; + Input : Node_Id; + + Name_Seen : Boolean := False; + -- A flag used to detect multiple item names + + -- Start of processing for Analyze_Initialization_Item_With_Inputs + + begin + -- Inspect the name of an item with inputs + + Elmt := First (Choices (Item)); + while Present (Elmt) loop + if Name_Seen then + Error_Msg_N ("only one item allowed in initialization", Elmt); + + else + Name_Seen := True; + Analyze_Initialization_Item (Elmt); + end if; + + Next (Elmt); + end loop; + + -- Multiple input items appear as an aggregate + + if Nkind (Inputs) = N_Aggregate then + if Present (Expressions (Inputs)) then + Input := First (Expressions (Inputs)); + while Present (Input) loop + Analyze_Input_Item (Input); + + Next (Input); + end loop; + end if; + + if Present (Component_Associations (Inputs)) then + Error_Msg_N + ("inputs must appear in named association form", Inputs); + end if; + + -- Single input item + + else + Analyze_Input_Item (Inputs); + end if; + end Analyze_Initialization_Item_With_Inputs; + + ---------------------------------- + -- Collect_States_And_Variables -- + ---------------------------------- + + procedure Collect_States_And_Variables is + Decl : Node_Id; + + begin + -- Collect the abstract states defined in the package (if any) + + if Present (Abstract_States (Pack_Id)) then + States_And_Vars := New_Copy_Elist (Abstract_States (Pack_Id)); + end if; + + -- Collect all variables the appear in the visible declarations of + -- the related package. + + if Present (Visible_Declarations (Pack_Spec)) then + Decl := First (Visible_Declarations (Pack_Spec)); + while Present (Decl) loop + if Nkind (Decl) = N_Object_Declaration + and then Ekind (Defining_Entity (Decl)) = E_Variable + and then Comes_From_Source (Decl) + then + Add_Item (Defining_Entity (Decl), States_And_Vars); + end if; + + Next (Decl); + end loop; + end if; + end Collect_States_And_Variables; + + -- Local variables + + Inits : constant Node_Id := + Get_Pragma_Arg (First (Pragma_Argument_Associations (N))); + Init : Node_Id; + + -- Start of processing for Analyze_Initializes_In_Decl_Part + + begin + Set_Analyzed (N); + + -- Initialize the various lists used during analysis + + Collect_States_And_Variables; + + -- Multiple initialization clauses appear as an aggregate + + if Nkind (Inits) = N_Aggregate then + if Present (Expressions (Inits)) then + Init := First (Expressions (Inits)); + while Present (Init) loop + Analyze_Initialization_Item (Init); + + Next (Init); + end loop; + end if; + + if Present (Component_Associations (Inits)) then + Init := First (Component_Associations (Inits)); + while Present (Init) loop + Analyze_Initialization_Item_With_Inputs (Init); + + Next (Init); + end loop; + end if; + + -- Various forms of a single initialization clause. Note that these may + -- include malformed initializations. + + else + Analyze_Initialization_Item (Inits); + end if; + end Analyze_Initializes_In_Decl_Part; + -------------------- -- Analyze_Pragma -- -------------------- @@ -1887,16 +2218,11 @@ package body Sem_Prag is -- UU_Typ is the related Unchecked_Union type. Flag In_Variant_Part -- should be set when Comp comes from a record variant. - procedure Check_Test_Case; - -- Called to process a test-case pragma. It starts with checking pragma - -- arguments, and the rest of the treatment is similar to the one for - -- pre- and postcondition in Check_Precondition_Postcondition, except - -- the placement rules for the test-case pragma are stricter. These - -- pragmas may only occur after a subprogram spec declared directly - -- in a package spec unit. In this case, the pragma is chained to the - -- subprogram in question (using Contract_Test_Cases and Next_Pragma) - -- and analysis of the pragma is delayed till the end of the spec. In - -- all other cases, an error message for bad placement is given. + procedure Check_Declaration_Order (States : Node_Id; Inits : Node_Id); + -- Subsidiary routine to the analysis of pragmas Abstract_State and + -- Initializes. Determine whether aspect/pragma Abstract_State denoted + -- by States is defined earlier than aspect/pragma Initializes denoted + -- by Inits. procedure Check_Duplicate_Pragma (E : Entity_Id); -- Check if a rep item of the same name as the current pragma is already @@ -2013,6 +2339,17 @@ package body Sem_Prag is -- that the constraint is static as required by the restrictions for -- Unchecked_Union. + procedure Check_Test_Case; + -- Called to process a test-case pragma. It starts with checking pragma + -- arguments, and the rest of the treatment is similar to the one for + -- pre- and postcondition in Check_Precondition_Postcondition, except + -- the placement rules for the test-case pragma are stricter. These + -- pragmas may only occur after a subprogram spec declared directly + -- in a package spec unit. In this case, the pragma is chained to the + -- subprogram in question (using Contract_Test_Cases and Next_Pragma) + -- and analysis of the pragma is delayed till the end of the spec. In + -- all other cases, an error message for bad placement is given. + procedure Check_Valid_Configuration_Pragma; -- Legality checks for placement of a configuration pragma @@ -2907,6 +3244,109 @@ package body Sem_Prag is end if; end Check_Component; + ----------------------------- + -- Check_Declaration_Order -- + ----------------------------- + + procedure Check_Declaration_Order (States : Node_Id; Inits : Node_Id) is + procedure Check_Aspect_Specification_Order; + -- Inspect the aspect specifications of the context to determine the + -- proper order. + + -------------------------------------- + -- Check_Aspect_Specification_Order -- + -------------------------------------- + + procedure Check_Aspect_Specification_Order is + Asp_I : constant Node_Id := Corresponding_Aspect (Inits); + Asp_S : constant Node_Id := Corresponding_Aspect (States); + Asp : Node_Id; + + States_Seen : Boolean := False; + + begin + -- Both aspects must be part of the same aspect specification list + + pragma Assert (List_Containing (Asp_I) = List_Containing (Asp_S)); + + Asp := First (List_Containing (Asp_I)); + while Present (Asp) loop + if Get_Aspect_Id (Asp) = Aspect_Abstract_State then + States_Seen := True; + + elsif Get_Aspect_Id (Asp) = Aspect_Initializes then + if not States_Seen then + Error_Msg_N + ("aspect % must come before aspect %", States); + end if; + + exit; + end if; + + Next (Asp); + end loop; + end Check_Aspect_Specification_Order; + + -- Local variables + + Stmt : Node_Id; + + -- Start of processing for Check_Declaration_Order + + begin + -- Cannot check the order if one of the pragmas is missing + + if No (States) or else No (Inits) then + return; + end if; + + -- Set up the error names in case the order is incorrect + + Error_Msg_Name_1 := Name_Abstract_State; + Error_Msg_Name_2 := Name_Initializes; + + if From_Aspect_Specification (States) then + + -- Both pragmas are actually aspects, check their declaration + -- order in the associated aspect specification list. Otherwise + -- States is an aspect and Inits a source pragma. + + if From_Aspect_Specification (Inits) then + Check_Aspect_Specification_Order; + end if; + + -- Abstract_States is a source pragma + + else + if From_Aspect_Specification (Inits) then + Error_Msg_N ("pragma % cannot come after aspect %", States); + + -- Both pragmas are source constructs. Try to reach States from + -- Inits by traversing the declarations backwards. + + else + Stmt := Prev (Inits); + while Present (Stmt) loop + + -- The order is ok, Abstract_States is first followed by + -- Initializes. + + if Nkind (Stmt) = N_Pragma + and then Pragma_Name (Stmt) = Name_Abstract_State + then + return; + end if; + + Prev (Stmt); + end loop; + + -- If we get here, then the pragmas are out of order + + Error_Msg_N ("pragma % cannot come after pragma %", States); + end if; + end if; + end Check_Declaration_Order; + ---------------------------- -- Check_Duplicate_Pragma -- ---------------------------- @@ -8655,7 +9095,16 @@ package body Sem_Prag is end if; Pack_Id := Defining_Entity (Context); - State := Expression (Arg1); + Add_Contract_Item (N, Pack_Id); + + -- Verify the declaration order of aspects/pragmas Abstract_State + -- and Initializes. + + Check_Declaration_Order + (States => N, + Inits => Get_Pragma (Pack_Id, Pragma_Initializes)); + + State := Expression (Arg1); -- Multiple abstract states appear as an aggregate @@ -12744,6 +13193,91 @@ package body Sem_Prag is Initialize_Scalars := True; end if; + ----------------- + -- Initializes -- + ----------------- + + -- pragma Initializes (INITIALIZATION_SPEC); + + -- INITIALIZATION_SPEC ::= null | INITIALIZATION_LIST + + -- INITIALIZATION_LIST ::= + -- INITIALIZATION_ITEM + -- | (INITIALIZATION_ITEM {, INITIALIZATION_ITEM}) + + -- INITIALIZATION_ITEM ::= name [=> INPUT_LIST] + + -- INPUT_LIST ::= + -- null + -- | INPUT + -- | (INPUT {, INPUT}) + + -- INPUT ::= name + + when Pragma_Initializes => Initializes : declare + Context : constant Node_Id := Parent (Parent (N)); + Pack_Id : Entity_Id; + Stmt : Node_Id; + + begin + GNAT_Pragma; + S14_Pragma; + Check_Arg_Count (1); + + -- Ensure the proper placement of the pragma. Initializes must be + -- associated with a package declaration. + + if not Nkind_In (Context, N_Generic_Package_Declaration, + N_Package_Declaration) + then + Pragma_Misplaced; + return; + end if; + + 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 pragma does not apply to a legal construct, issue an + -- error and stop the analysis. + + else + Pragma_Misplaced; + return; + end if; + + Stmt := Prev (Stmt); + end loop; + + -- The pragma must be analyzed at the end of the visible + -- declarations of the related package. Save the pragma for later + -- (see Analyze_Initializes_In_Decl_Part) by adding it to the + -- contract of the package. + + Pack_Id := Defining_Entity (Context); + Add_Contract_Item (N, Pack_Id); + + -- Verify the declaration order of aspects/pragmas Abstract_State + -- and Initializes. + + Check_Declaration_Order + (States => Get_Pragma (Pack_Id, Pragma_Abstract_State), + Inits => N); + end Initializes; + ------------ -- Inline -- ------------ @@ -16177,6 +16711,7 @@ package body Sem_Prag is when Pragma_Refined_State => Refined_State : declare Context : constant Node_Id := Parent (N); Spec_Id : Entity_Id; + Stmt : Node_Id; begin GNAT_Pragma; @@ -16191,6 +16726,34 @@ package body Sem_Prag is return; end if; + 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 pragma does not apply to a legal construct, issue an + -- error and stop the analysis. + + else + Pragma_Misplaced; + return; + end if; + + Stmt := Prev (Stmt); + end loop; + -- State refinement is allowed only when the corresponding package -- declaration has a non-null aspect/pragma Abstract_State. @@ -16207,9 +16770,10 @@ package body Sem_Prag is -- The pragma must be analyzed at the end of the declarations as -- it has visibility over the whole declarative region. Save the - -- pragma for later (see Analyze_Refined_Depends_In_Decl_Part). + -- pragma for later (see Analyze_Refined_Depends_In_Decl_Part) by + -- adding it to the contract of the package body. - Set_Refined_State_Pragma (Defining_Entity (Context), N); + Add_Contract_Item (N, Defining_Entity (Context)); end Refined_State; ----------------------- @@ -19647,9 +20211,9 @@ package body Sem_Prag is procedure Analyze_Refinement_Clause (Clause : Node_Id); -- Perform full analysis of a single refinement clause - function Collect_Hidden_States return Elist_Id; + procedure Collect_Hidden_States; -- Gather the entities of all hidden states that appear in the spec and - -- body of the related package. + -- body of the related package in Hidden_States. procedure Report_Unrefined_States; -- Emit errors for all abstract states that have not been refined by @@ -19938,9 +20502,7 @@ package body Sem_Prag is -- Collect_Hidden_States -- --------------------------- - function Collect_Hidden_States return Elist_Id is - Result : Elist_Id := No_Elist; - + procedure Collect_Hidden_States is procedure Collect_Hidden_States_In_Decls (Decls : List_Id); -- Find all hidden states that appear in declarative list Decls and -- append their entities to Result. @@ -19963,7 +20525,7 @@ package body Sem_Prag is begin State_Elmt := First_Elmt (States); while Present (State_Elmt) loop - Add_Item (Node (State_Elmt), Result); + Add_Item (Node (State_Elmt), Hidden_States); Next_Elmt (State_Elmt); end loop; @@ -19985,7 +20547,7 @@ package body Sem_Prag is and then Ekind (Defining_Entity (Decl)) = E_Variable and then Comes_From_Source (Decl) then - Add_Item (Defining_Entity (Decl), Result); + Add_Item (Defining_Entity (Decl), Hidden_States); -- Gather the abstract states of a package along with all -- hidden states in its visible declarations. @@ -20014,8 +20576,6 @@ package body Sem_Prag is Collect_Hidden_States_In_Decls (Private_Declarations (Pack_Spec)); Collect_Hidden_States_In_Decls (Declarations (Pack_Body)); - - return Result; end Collect_Hidden_States; ----------------------------- @@ -20080,7 +20640,7 @@ package body Sem_Prag is -- Local declarations Clauses : constant Node_Id := - Expression (First (Pragma_Argument_Associations (N))); + Get_Pragma_Arg (First (Pragma_Argument_Associations (N))); Clause : Node_Id; -- Start of processing for Analyze_Refined_State_In_Decl_Part @@ -20090,8 +20650,8 @@ package body Sem_Prag is -- Initialize the various lists used during analysis - Abstr_States := New_Copy_Elist (Abstract_States (Spec_Id)); - Hidden_States := Collect_Hidden_States; + Abstr_States := New_Copy_Elist (Abstract_States (Spec_Id)); + Collect_Hidden_States; -- Multiple state refinements appear as an aggregate @@ -20814,6 +21374,7 @@ package body Sem_Prag is Pragma_Independent => 0, Pragma_Independent_Components => 0, Pragma_Initialize_Scalars => -1, + Pragma_Initializes => -1, Pragma_Inline => 0, Pragma_Inline_Always => 0, Pragma_Inline_Generic => 0, diff --git a/gcc/ada/sem_prag.ads b/gcc/ada/sem_prag.ads index a50757b..cef28ca 100644 --- a/gcc/ada/sem_prag.ads +++ b/gcc/ada/sem_prag.ads @@ -62,6 +62,9 @@ package Sem_Prag is procedure Analyze_Global_In_Decl_Part (N : Node_Id); -- Perform full analysis of delayed pragma Global + procedure Analyze_Initializes_In_Decl_Part (N : Node_Id); + -- Perform full analysis of delayed pragma Initializes + procedure Analyze_Pre_Post_Condition_In_Decl_Part (Prag : Node_Id; Subp_Id : Entity_Id); diff --git a/gcc/ada/sem_util.adb b/gcc/ada/sem_util.adb index 80ba002..a5a6f7b 100644 --- a/gcc/ada/sem_util.adb +++ b/gcc/ada/sem_util.adb @@ -212,24 +212,27 @@ package body Sem_Util is -- Add_Contract_Item -- ----------------------- - procedure Add_Contract_Item (Prag : Node_Id; Subp_Id : Entity_Id) is - Items : constant Node_Id := Contract (Subp_Id); + procedure Add_Contract_Item (Prag : Node_Id; Id : Entity_Id) is + Items : constant Node_Id := Contract (Id); Nam : Name_Id; N : Node_Id; begin - -- The related subprogram [body] must have a contract and the item to be - -- added must be a pragma. + -- The related context must have a contract and the item to be added + -- must be a pragma. pragma Assert (Present (Items)); pragma Assert (Nkind (Prag) = N_Pragma); Nam := Original_Aspect_Name (Prag); - -- Contract items related to subprogram bodies + -- Contract items related to [generic] packages. The applicable pragmas + -- are: + -- Abstract_States + -- Initializes - if Ekind (Subp_Id) = E_Subprogram_Body then - if Nam_In (Nam, Name_Refined_Depends, Name_Refined_Global) then + if Ekind_In (Id, E_Generic_Package, E_Package) then + if Nam_In (Nam, Name_Abstract_State, Name_Initializes) then Set_Next_Pragma (Prag, Classifications (Items)); Set_Classifications (Items, Prag); @@ -239,9 +242,35 @@ package body Sem_Util is raise Program_Error; end if; - -- Contract items related to subprogram declarations + -- Contract items related to package bodies. The applicable pragmas are: + -- Refined_States - else + elsif Ekind (Id) = E_Package_Body then + if Nam = Name_Refined_State then + Set_Next_Pragma (Prag, Classifications (Items)); + Set_Classifications (Items, Prag); + + -- The pragma is not a proper contract item + + else + raise Program_Error; + end if; + + -- Contract items related to subprogram or entry declarations. The + -- applicable pragmas are: + -- Contract_Cases + -- Depends + -- Global + -- Post + -- Postcondition + -- Pre + -- Precondition + -- Test_Case + + elsif Ekind_In (Id, E_Entry, E_Entry_Family) + or else Is_Generic_Subprogram (Id) + or else Is_Subprogram (Id) + then if Nam_In (Nam, Name_Precondition, Name_Postcondition, Name_Pre, @@ -251,7 +280,7 @@ package body Sem_Util is 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] + -- happen if we use a pragma for Pre[_Class] or Post[_Class] -- instead of the corresponding aspect. if not From_Aspect_Specification (Prag) @@ -269,7 +298,7 @@ package body Sem_Util is then Error_Msg_Sloc := Sloc (N); Error_Msg_NE - ("duplication of aspect for & given#", Prag, Subp_Id); + ("duplication of aspect for & given#", Prag, Id); return; else N := Next_Pragma (N); @@ -293,6 +322,22 @@ package body Sem_Util is else raise Program_Error; end if; + + -- Contract items related to subprogram bodies. The applicable pragmas + -- are: + -- Refined_Depends + -- Refined_Global + + elsif Ekind (Id) = E_Subprogram_Body then + if Nam_In (Nam, Name_Refined_Depends, Name_Refined_Global) then + Set_Next_Pragma (Prag, Classifications (Items)); + Set_Classifications (Items, Prag); + + -- The pragma is not a proper contract item + + else + raise Program_Error; + end if; end if; end Add_Contract_Item; diff --git a/gcc/ada/sem_util.ads b/gcc/ada/sem_util.ads index 13ee3b3..d19ba57 100644 --- a/gcc/ada/sem_util.ads +++ b/gcc/ada/sem_util.ads @@ -43,16 +43,19 @@ package Sem_Util is -- Add A to the list of access types to process when expanding the -- freeze node of E. - procedure Add_Contract_Item (Prag : Node_Id; Subp_Id : Entity_Id); - -- Add one of the following contract item to the contract of a subprogram. - -- Prag denotes a pragma and Subp_Id is the related subprogram [body]. + procedure Add_Contract_Item (Prag : Node_Id; Id : Entity_Id); + -- Add pragma Prag to the contract of an entry, a package [body] or a + -- subprogram [body] denoted by Id. The following are valid pragmas: + -- Abstract_States -- Contract_Cases -- Depends -- Global + -- Initializes -- Postcondition -- Precondition -- Refined_Depends -- Refined_Global + -- Refined_States -- Test_Case procedure Add_Global_Declaration (N : Node_Id); diff --git a/gcc/ada/sinfo.ads b/gcc/ada/sinfo.ads index 2670c6a..5abe922 100644 --- a/gcc/ada/sinfo.ads +++ b/gcc/ada/sinfo.ads @@ -7151,9 +7151,14 @@ package Sinfo is -- Contract -- -------------- - -- This node is used to hold the various parts of an entry or subprogram - -- [body] contract, consisting of precondition, postconditions, contract - -- cases, test cases and global dependencies. + -- This node is used to hold the various parts of an entry, subprogram + -- [body] or package [body] contract, in particular: + -- Abstract states declared by a package declaration + -- Contract cases that apply to a subprogram + -- Dependency relations of inputs and output of a subprogram + -- Global annotations classifying data as input or output + -- Initialization sequences for a package declaration + -- Pre- and postconditions that apply to a subprogram -- The node appears in an entry and [generic] subprogram [body] entity. @@ -7170,8 +7175,13 @@ package Sinfo is -- Pre_Post_Conditions contains a collection of pragmas that correspond -- to pre- and postconditions associated with an entry or a subprogram -- [body or stub]. The pragmas can either come from source or be the - -- byproduct of aspect expansion. The ordering in the list is in LIFO - -- fashion. + -- byproduct of aspect expansion. Currently the following pragmas appear + -- in this list: + -- Post + -- Postcondition + -- Pre + -- Precondition + -- The ordering in the list is in LIFO fashion. -- Note that there might be multiple preconditions or postconditions -- in this list, either because they come from separate pragmas in the @@ -7182,10 +7192,17 @@ package Sinfo is -- to aspects/pragmas Contract_Cases and Test_Case. The ordering in the -- list is in LIFO fashion. - -- Classifications contains pragmas that either categorize subprogram - -- inputs and outputs or establish dependencies between them. Currently - -- pragmas Depends, Global, Refined_Depends and Refined_Global are - -- stored in this list. The ordering is in LIFO fashion. + -- Classifications contains pragmas that either declare, categorize or + -- establish dependencies between subprogram or package inputs and + -- outputs. Currently the following pragmas appear in this list: + -- Abstract_States + -- Depends + -- Global + -- Initializes + -- Refined_Depends + -- Refined_Global + -- Refined_States + -- The ordering is in LIFO fashion. ------------------- -- Expanded_Name -- diff --git a/gcc/ada/snames.ads-tmpl b/gcc/ada/snames.ads-tmpl index aacaf8a..0a5d946 100644 --- a/gcc/ada/snames.ads-tmpl +++ b/gcc/ada/snames.ads-tmpl @@ -511,6 +511,7 @@ package Snames is Name_Import_Valued_Procedure : constant Name_Id := N + $; -- GNAT Name_Independent : constant Name_Id := N + $; -- Ada 12 Name_Independent_Components : constant Name_Id := N + $; -- Ada 12 + Name_Initializes : constant Name_Id := N + $; -- GNAT Name_Inline : constant Name_Id := N + $; Name_Inline_Always : constant Name_Id := N + $; -- GNAT Name_Inline_Generic : constant Name_Id := N + $; -- GNAT @@ -587,9 +588,6 @@ package Snames is Name_Refined_Global : constant Name_Id := N + $; -- GNAT Name_Refined_Post : constant Name_Id := N + $; -- GNAT Name_Refined_Pre : constant Name_Id := N + $; -- GNAT - - -- Kirchev - Name_Refined_State : constant Name_Id := N + $; -- GNAT Name_Relative_Deadline : constant Name_Id := N + $; -- Ada 05 Name_Remote_Access_Type : constant Name_Id := N + $; -- GNAT @@ -1831,6 +1829,7 @@ package Snames is Pragma_Import_Valued_Procedure, Pragma_Independent, Pragma_Independent_Components, + Pragma_Initializes, Pragma_Inline, Pragma_Inline_Always, Pragma_Inline_Generic,