diff options
Diffstat (limited to 'gcc/ada')
| -rw-r--r-- | gcc/ada/ChangeLog | 76 | ||||
| -rw-r--r-- | gcc/ada/aspects.adb | 1 | ||||
| -rw-r--r-- | gcc/ada/aspects.ads | 4 | ||||
| -rw-r--r-- | gcc/ada/atree.adb | 34 | ||||
| -rw-r--r-- | gcc/ada/atree.ads | 20 | ||||
| -rw-r--r-- | gcc/ada/einfo.adb | 78 | ||||
| -rw-r--r-- | gcc/ada/einfo.ads | 24 | ||||
| -rw-r--r-- | gcc/ada/par-prag.adb | 1 | ||||
| -rw-r--r-- | gcc/ada/sem_ch12.adb | 20 | ||||
| -rw-r--r-- | gcc/ada/sem_ch13.adb | 55 | ||||
| -rw-r--r-- | gcc/ada/sem_ch3.adb | 33 | ||||
| -rw-r--r-- | gcc/ada/sem_ch6.adb | 63 | ||||
| -rw-r--r-- | gcc/ada/sem_ch7.adb | 43 | ||||
| -rw-r--r-- | gcc/ada/sem_prag.adb | 617 | ||||
| -rw-r--r-- | gcc/ada/sem_prag.ads | 3 | ||||
| -rw-r--r-- | gcc/ada/sem_util.adb | 67 | ||||
| -rw-r--r-- | gcc/ada/sem_util.ads | 9 | ||||
| -rw-r--r-- | gcc/ada/sinfo.ads | 35 | ||||
| -rw-r--r-- | gcc/ada/snames.ads-tmpl | 5 |
19 files changed, 1013 insertions, 175 deletions
diff --git a/gcc/ada/ChangeLog b/gcc/ada/ChangeLog index 2ec3be47c05..f9c6ace636c 100644 --- a/gcc/ada/ChangeLog +++ b/gcc/ada/ChangeLog @@ -1,3 +1,79 @@ +2013-10-14 Hristian Kirtchev <kirtchev@adacore.com> + + * 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 <roche@adacore.com> Eric Botcazou <ebotcazou@adacore.com> diff --git a/gcc/ada/aspects.adb b/gcc/ada/aspects.adb index 2aea7b3ee8b..b9f1a56af6c 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 15c6e4cec43..2325d970383 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 a6105e2c427..a44a247b896 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 123beb3907e..54655545dbd 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 fa0daa98ce6..2c1a094a4bb 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 4843b9e01e8..489576310e9 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 aed45f96982..22e79d78921 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 df80232311a..d5c5ce7c595 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 71cc77e60c1..29fc1c79382 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 85872e10803..b2e2a9263cb 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 acf1aeb812b..34d0a8853b1 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 516683004b1..d15add3bf53 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 0bfcf0de491..070d7cbb48b 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 a50757b3ef4..cef28caf803 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 80ba002a711..a5a6f7b35fa 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 13ee3b3dbe3..d19ba57710c 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 2670c6ab4c7..5abe9224387 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 aacaf8a505f..0a5d9460e36 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, |