From 9b2451e5b31bcea0398b5cb8574d516c97efa0f9 Mon Sep 17 00:00:00 2001 From: Arnaud Charlet Date: Mon, 14 Oct 2013 15:33:48 +0200 Subject: [PATCH] [multiple changes] 2013-10-14 Hristian Kirtchev * aspects.adb: Add an entry in table Canonical_Aspect for Initial_Condition. * aspects.ads: Add entries in tables Aspect_Id, Aspect_Argument, Aspect_Names and Aspect_Delay for Initial_Condition. * einfo.adb (Get_Pragma): Include pragma Initial_Condition to categorization pragmas. * einfo.ads (Get_Pragma): Update comment on usage. * exp_ch7.adb (Expand_N_Package_Body): Add a runtime check to verify the assertion introduced by pragma Initial_Condition. (Expand_N_Package_Declaration): Add a runtime check to verify the assertion introduced by pragma Initial_Condition. (Expand_Pragma_Initial_Condition): New routine. * par-prag: Include pragma Initial_Condition to the list of pragmas that do not require special processing by the parser. * sem_ch3.adb (Analyze_Declarations): Analyze pragma Initial_Condition at the end of the visible declarations. * sem_ch13.adb (Analyze_Aspect_Specifications): Add processing for aspect Initial_Condition. (Check_Aspect_At_Freeze_Point): Aspect Initial_Condition does not need inspection at freezing. * sem_prag.adb (Analyze_Initial_Condition_In_Decl_Part): New routine. (Analyze_Pragma): Update all calls to Check_Declaration_Order. Add processing for pragma Initial_Condition. Initial_Condition is now a valid assertion kind. Add an entry in table Sig_Flags for Initial_Condition. (Check_Declaration_Order): Reimplemented to handle arbitrary pragmas. (Is_Valid_Assertion_Kind): Add an entry for Initial_Condition. * sem_pag.ads (Analyze_Initial_Condition_In_Decl_Part): New routine. * sem_util.adb (Add_Contract_Item): Pragma Initial_Condition can now be associated with a package spec. * sem_util.ads (Add_Contract_Item): Update comment on usage. * sinfo.ads: Update the documentation of node N_Contract * snames.ads-tmpl: Add new predefined name Initial_Condition. Add new pragma id for Initial_Condition. 2013-10-14 Thomas Quinot * exp_pakd.adb: Minor reformatting. From-SVN: r203551 --- gcc/ada/ChangeLog | 45 +++++ gcc/ada/aspects.adb | 1 + gcc/ada/aspects.ads | 4 + gcc/ada/einfo.adb | 17 +- gcc/ada/einfo.ads | 2 + gcc/ada/exp_ch7.adb | 115 ++++++++++++- gcc/ada/exp_pakd.adb | 4 +- gcc/ada/par-prag.adb | 1 + gcc/ada/sem_ch13.adb | 40 +++++ gcc/ada/sem_ch3.adb | 12 +- gcc/ada/sem_prag.adb | 359 ++++++++++++++++++++++++++++++++++------ gcc/ada/sem_prag.ads | 3 + gcc/ada/sem_util.adb | 6 +- gcc/ada/sem_util.ads | 1 + gcc/ada/sinfo.ads | 1 + gcc/ada/snames.ads-tmpl | 2 + 16 files changed, 545 insertions(+), 68 deletions(-) diff --git a/gcc/ada/ChangeLog b/gcc/ada/ChangeLog index adb5e6d79e2..acb4f5881ab 100644 --- a/gcc/ada/ChangeLog +++ b/gcc/ada/ChangeLog @@ -1,3 +1,48 @@ +2013-10-14 Hristian Kirtchev + + * aspects.adb: Add an entry in table Canonical_Aspect for + Initial_Condition. + * aspects.ads: Add entries in tables Aspect_Id, Aspect_Argument, + Aspect_Names and Aspect_Delay for Initial_Condition. + * einfo.adb (Get_Pragma): Include pragma Initial_Condition to + categorization pragmas. + * einfo.ads (Get_Pragma): Update comment on usage. + * exp_ch7.adb (Expand_N_Package_Body): Add a runtime check to + verify the assertion introduced by pragma Initial_Condition. + (Expand_N_Package_Declaration): Add a runtime check to + verify the assertion introduced by pragma Initial_Condition. + (Expand_Pragma_Initial_Condition): New routine. + * par-prag: Include pragma Initial_Condition to the list of + pragmas that do not require special processing by the parser. + * sem_ch3.adb (Analyze_Declarations): Analyze pragma + Initial_Condition at the end of the visible declarations. + * sem_ch13.adb (Analyze_Aspect_Specifications): Add processing + for aspect Initial_Condition. + (Check_Aspect_At_Freeze_Point): + Aspect Initial_Condition does not need inspection at freezing. + * sem_prag.adb (Analyze_Initial_Condition_In_Decl_Part): + New routine. + (Analyze_Pragma): Update all calls + to Check_Declaration_Order. Add processing for pragma + Initial_Condition. Initial_Condition is now a valid assertion + kind. Add an entry in table Sig_Flags for Initial_Condition. + (Check_Declaration_Order): Reimplemented to handle arbitrary + pragmas. + (Is_Valid_Assertion_Kind): Add an entry for + Initial_Condition. + * sem_pag.ads (Analyze_Initial_Condition_In_Decl_Part): + New routine. + * sem_util.adb (Add_Contract_Item): Pragma Initial_Condition + can now be associated with a package spec. + * sem_util.ads (Add_Contract_Item): Update comment on usage. + * sinfo.ads: Update the documentation of node N_Contract + * snames.ads-tmpl: Add new predefined name Initial_Condition. Add + new pragma id for Initial_Condition. + +2013-10-14 Thomas Quinot + + * exp_pakd.adb: Minor reformatting. + 2013-10-14 Robert Dewar * exp_prag.adb: Minor reformatting. diff --git a/gcc/ada/aspects.adb b/gcc/ada/aspects.adb index b9f1a56af6c..0d9d28c556d 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_Initial_Condition => Aspect_Initial_Condition, Aspect_Initializes => Aspect_Initializes, Aspect_Input => Aspect_Input, Aspect_Interrupt_Handler => Aspect_Interrupt_Handler, diff --git a/gcc/ada/aspects.ads b/gcc/ada/aspects.ads index 2325d970383..877a1af3b79 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_Initial_Condition, -- GNAT Aspect_Initializes, -- GNAT Aspect_Input, Aspect_Interrupt_Priority, @@ -310,6 +311,7 @@ package Aspects is Aspect_External_Tag => Expression, Aspect_Global => Expression, Aspect_Implicit_Dereference => Name, + Aspect_Initial_Condition => Expression, Aspect_Initializes => Expression, Aspect_Input => Name, Aspect_Interrupt_Priority => Expression, @@ -400,6 +402,7 @@ package Aspects is Aspect_Independent_Components => Name_Independent_Components, Aspect_Inline => Name_Inline, Aspect_Inline_Always => Name_Inline_Always, + Aspect_Initial_Condition => Name_Initial_Condition, Aspect_Initializes => Name_Initializes, Aspect_Input => Name_Input, Aspect_Interrupt_Handler => Name_Interrupt_Handler, @@ -600,6 +603,7 @@ package Aspects is Aspect_Independent_Components => Always_Delay, Aspect_Inline => Always_Delay, Aspect_Inline_Always => Always_Delay, + Aspect_Initial_Condition => Always_Delay, Aspect_Initializes => Always_Delay, Aspect_Input => Always_Delay, Aspect_Interrupt_Handler => Always_Delay, diff --git a/gcc/ada/einfo.adb b/gcc/ada/einfo.adb index 176a81fbc5d..8636d8511cd 100644 --- a/gcc/ada/einfo.adb +++ b/gcc/ada/einfo.adb @@ -6300,18 +6300,19 @@ 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 or else + Id = Pragma_Abstract_State or else + Id = Pragma_Depends or else + Id = Pragma_Global or else + Id = Pragma_Initial_Condition or else + Id = Pragma_Initializes or else + Id = Pragma_Refined_Depends or else + Id = Pragma_Refined_Global or else Id = Pragma_Refined_State; Is_CTC : constant Boolean := - Id = Pragma_Contract_Cases or else + Id = Pragma_Contract_Cases or else Id = Pragma_Test_Case; Is_PPC : constant Boolean := - Id = Pragma_Precondition or else + Id = Pragma_Precondition or else Id = Pragma_Postcondition; In_Contract : constant Boolean := Is_CDG or Is_CTC or Is_PPC; diff --git a/gcc/ada/einfo.ads b/gcc/ada/einfo.ads index 8bc4b79007f..0526d4406e8 100644 --- a/gcc/ada/einfo.ads +++ b/gcc/ada/einfo.ads @@ -7442,6 +7442,8 @@ package Einfo is -- Contract_Cases -- Depends -- Global + -- Initial_Condition + -- Initializes -- Precondition -- Postcondition -- Refined_Depends diff --git a/gcc/ada/exp_ch7.adb b/gcc/ada/exp_ch7.adb index fdaf213ff86..1b242cc46e9 100644 --- a/gcc/ada/exp_ch7.adb +++ b/gcc/ada/exp_ch7.adb @@ -368,6 +368,11 @@ package body Exp_Ch7 is -- Given an arbitrary entity, traverse the scope chain looking for the -- first enclosing function. Return Empty if no function was found. + procedure Expand_Pragma_Initial_Condition (N : Node_Id); + -- Subsidiary to the expansion of package specs and bodies. Generate a + -- runtime check needed to verify the assumption introduced by pragma + -- Initial_Condition. N denotes the package spec or body. + function Make_Call (Loc : Source_Ptr; Proc_Id : Entity_Id; @@ -3959,6 +3964,15 @@ package body Exp_Ch7 is end if; Build_Task_Activation_Call (N); + + -- When the package is subject to pragma Initial_Condition, the + -- assertion expression must be verified at the end of the body + -- statements. + + if Present (Get_Pragma (Spec_Ent, Pragma_Initial_Condition)) then + Expand_Pragma_Initial_Condition (N); + end if; + Pop_Scope; end if; @@ -4053,10 +4067,9 @@ package body Exp_Ch7 is if No_Body then Push_Scope (Id); + -- Generate RACW subprogram bodies + if Has_RACW (Id) then - - -- Generate RACW subprogram bodies - Decls := Private_Declarations (Spec); if No (Decls) then @@ -4072,13 +4085,21 @@ package body Exp_Ch7 is Analyze_List (Decls); end if; + -- Generate task activation call as last step of elaboration + if Present (Activation_Chain_Entity (N)) then - - -- Generate task activation call as last step of elaboration - Build_Task_Activation_Call (N); end if; + -- When the package is subject to pragma Initial_Condition and lacks + -- a body, the assertion expression must be verified at the end of + -- the visible declarations. Otherwise the check is performed at the + -- end of the body statements (see Expand_N_Package_Body). + + if Present (Get_Pragma (Id, Pragma_Initial_Condition)) then + Expand_Pragma_Initial_Condition (N); + end if; + Pop_Scope; end if; @@ -4114,6 +4135,88 @@ package body Exp_Ch7 is end if; end Expand_N_Package_Declaration; + ------------------------------------- + -- Expand_Pragma_Initial_Condition -- + ------------------------------------- + + procedure Expand_Pragma_Initial_Condition (N : Node_Id) is + Loc : constant Source_Ptr := Sloc (N); + Check : Node_Id; + Expr : Node_Id; + Init_Cond : Node_Id; + List : List_Id; + Pack_Id : Entity_Id; + + begin + if Nkind (N) = N_Package_Body then + Pack_Id := Corresponding_Spec (N); + + if Present (Handled_Statement_Sequence (N)) then + List := Statements (Handled_Statement_Sequence (N)); + + -- The package body lacks statements, create an empty list + + else + List := New_List; + + Set_Handled_Statement_Sequence (N, + Make_Handled_Sequence_Of_Statements (Loc, Statements => List)); + end if; + + elsif Nkind (N) = N_Package_Declaration then + Pack_Id := Defining_Entity (N); + + if Present (Visible_Declarations (Specification (N))) then + List := Visible_Declarations (Specification (N)); + + -- The package lacks visible declarations, create an empty list + + else + List := New_List; + + Set_Visible_Declarations (Specification (N), List); + end if; + + -- This routine should not be used on anything other than packages + + else + raise Program_Error; + end if; + + Init_Cond := Get_Pragma (Pack_Id, Pragma_Initial_Condition); + + -- The caller should check whether the package is subject to pragma + -- Initial_Condition. + + pragma Assert (Present (Init_Cond)); + + Expr := + Get_Pragma_Arg (First (Pragma_Argument_Associations (Init_Cond))); + + -- The assertion expression was found to be illegal, do not generate the + -- runtime check as it will repeat the illegality. + + if Error_Posted (Init_Cond) or else Error_Posted (Expr) then + return; + end if; + + -- Generate: + -- pragma Check (Initial_Condition, ); + + Check := + Make_Pragma (Loc, + Chars => Name_Check, + Pragma_Argument_Associations => New_List ( + Make_Pragma_Argument_Association (Loc, + Expression => Make_Identifier (Loc, Name_Initial_Condition)), + + Make_Pragma_Argument_Association (Loc, + Expression => New_Copy_Tree (Expr)))); + + Append_To (List, Check); + Analyze (Check); + end Expand_Pragma_Initial_Condition; + ----------------------------- -- Find_Node_To_Be_Wrapped -- ----------------------------- diff --git a/gcc/ada/exp_pakd.adb b/gcc/ada/exp_pakd.adb index a6a1f0dc70b..45aafadefee 100644 --- a/gcc/ada/exp_pakd.adb +++ b/gcc/ada/exp_pakd.adb @@ -1326,8 +1326,8 @@ package body Exp_Pakd is -- The expression for the shift value that is required Shift_Used : Boolean := False; - -- Set True if Shift has been used in the generated code at least - -- once, so that it must be duplicated if used again + -- Set True if Shift has been used in the generated code at least once, + -- so that it must be duplicated if used again. New_Lhs : Node_Id; New_Rhs : Node_Id; diff --git a/gcc/ada/par-prag.adb b/gcc/ada/par-prag.adb index a965e12972c..53f4fe4652d 100644 --- a/gcc/ada/par-prag.adb +++ b/gcc/ada/par-prag.adb @@ -1185,6 +1185,7 @@ begin Pragma_Import_Valued_Procedure | Pragma_Independent | Pragma_Independent_Components | + Pragma_Initial_Condition | Pragma_Initialize_Scalars | Pragma_Initializes | Pragma_Inline | diff --git a/gcc/ada/sem_ch13.adb b/gcc/ada/sem_ch13.adb index aacb84c729e..6744484da38 100644 --- a/gcc/ada/sem_ch13.adb +++ b/gcc/ada/sem_ch13.adb @@ -2053,6 +2053,45 @@ package body Sem_Ch13 is Insert_Delayed_Pragma (Aitem); goto Continue; + -- Initial_Condition + + -- Aspect Initial_Condition covers the visible declarations of + -- a package and all hidden states through functions. As such, + -- it must be evaluated at the end of the said declarations. + + when Aspect_Initial_Condition => Initial_Condition : 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_Initial_Condition); + 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 Initial_Condition; + -- Initializes -- Aspect Initializes coverts the visible declarations of a @@ -7849,6 +7888,7 @@ package body Sem_Ch13 is Aspect_Dimension | Aspect_Dimension_System | Aspect_Implicit_Dereference | + Aspect_Initial_Condition | Aspect_Initializes | Aspect_Post | Aspect_Postcondition | diff --git a/gcc/ada/sem_ch3.adb b/gcc/ada/sem_ch3.adb index e81e61f215a..4440910ab69 100644 --- a/gcc/ada/sem_ch3.adb +++ b/gcc/ada/sem_ch3.adb @@ -2224,9 +2224,9 @@ package body Sem_Ch3 is if Present (L) then Context := Parent (L); - -- Analyze aspect/pragma Initializes of a package at the end of the - -- visible declarations as the aspect/pragma has visibility over the - -- said region. + -- Analyze pragmas Initializes and Initial_Condition of a package at + -- the end of the visible declarations as the pragmas have visibility + -- over the said region. if Nkind (Context) = N_Package_Specification and then L = Visible_Declarations (Context) @@ -2238,6 +2238,12 @@ package body Sem_Ch3 is Analyze_Initializes_In_Decl_Part (Prag); end if; + Prag := Get_Pragma (Spec_Id, Pragma_Initial_Condition); + + if Present (Prag) then + Analyze_Initial_Condition_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 diff --git a/gcc/ada/sem_prag.adb b/gcc/ada/sem_prag.adb index 95ac60088ad..4734581b0e5 100644 --- a/gcc/ada/sem_prag.adb +++ b/gcc/ada/sem_prag.adb @@ -911,9 +911,9 @@ package body Sem_Prag is -- as input. OUT parameters are valid inputs only when their type -- is unconstrained or tagged as their discriminants, array bouns -- or tags can be read. In general, states and variables are - -- considered to have mode IN OUT unless they are moded by pragma - -- [Refined_]Global. In that case, the item must appear in an - -- input global list. + -- considered to have mode IN OUT unless they are classified by + -- pragma [Refined_]Global. In that case, the item must appear in + -- an input global list. if (Ekind (Item_Id) = E_Out_Parameter and then not Is_Unconstrained_Or_Tagged_Item (Item_Id)) @@ -1964,6 +1964,194 @@ package body Sem_Prag is end if; end Analyze_Global_In_Decl_Part; + -------------------------------------------- + -- Analyze_Initial_Condition_In_Decl_Part -- + -------------------------------------------- + + procedure Analyze_Initial_Condition_In_Decl_Part (N : Node_Id) is + Pack_Id : constant Entity_Id := Defining_Entity (Parent (Parent (N))); + Prag_Init : constant Node_Id := + Get_Pragma (Pack_Id, Pragma_Initializes); + -- The related pragma Initializes + + Vars : Elist_Id := No_Elist; + -- A list of all variables declared in pragma Initializes + + procedure Collect_Variables; + -- Inspect the initialization list of pragma Initializes and collect the + -- entities of all variables declared within the related package. + + function Match_Variable (N : Node_Id) return Traverse_Result; + -- Determine whether arbitrary node N denotes a variable declared in the + -- visible declarations of the related package. + + procedure Report_Unused_Variables; + -- Emit errors for all variables found in list Vars + + ----------------------- + -- Collect_Variables -- + ----------------------- + + procedure Collect_Variables is + procedure Collect_Variable (Item : Node_Id); + -- Determine whether Item denotes a variable that appears in the + -- related package and if it does, add it to list Vars. + + ---------------------- + -- Collect_Variable -- + ---------------------- + + procedure Collect_Variable (Item : Node_Id) is + Item_Id : Entity_Id; + + begin + if Is_Entity_Name (Item) and then Present (Entity (Item)) then + Item_Id := Entity (Item); + + -- The item is a variable declared in the related package + + if Ekind (Item_Id) = E_Variable + and then Scope (Item_Id) = Pack_Id + then + Add_Item (Item_Id, Vars); + end if; + end if; + end Collect_Variable; + + -- Local variables + + Inits : constant Node_Id := + Get_Pragma_Arg + (First (Pragma_Argument_Associations (Prag_Init))); + Init : Node_Id; + + -- Start of processing for Collect_Variables + + begin + -- Multiple initialization items appear as an aggregate + + if Nkind (Inits) = N_Aggregate + and then Present (Expressions (Inits)) + then + Init := First (Expressions (Inits)); + while Present (Init) loop + Collect_Variable (Init); + + Next (Init); + end loop; + + -- Single initialization item + + else + Collect_Variable (Inits); + end if; + end Collect_Variables; + + -------------------- + -- Match_Variable -- + -------------------- + + function Match_Variable (N : Node_Id) return Traverse_Result is + Var_Id : Entity_Id; + + begin + -- Find a variable declared within the related package and try to + -- remove it from the list of collected variables found in pragma + -- Initializes. + + if Is_Entity_Name (N) + and then Present (Entity (N)) + then + Var_Id := Entity (N); + + if Ekind (Var_Id) = E_Variable + and then Scope (Var_Id) = Pack_Id + then + Remove (Vars, Var_Id); + end if; + end if; + + return OK; + end Match_Variable; + + procedure Match_Variables is new Traverse_Proc (Match_Variable); + + ----------------------------- + -- Report_Unused_Variables -- + ----------------------------- + + procedure Report_Unused_Variables is + Posted : Boolean := False; + Var_Elmt : Elmt_Id; + Var_Id : Entity_Id; + + begin + if Present (Vars) then + Var_Elmt := First_Elmt (Vars); + while Present (Var_Elmt) loop + Var_Id := Node (Var_Elmt); + + if not Posted then + Posted := True; + Error_Msg_Name_1 := Name_Initial_Condition; + Error_Msg_N + ("expression of % must mention the following variables", + N); + end if; + + Error_Msg_Sloc := Sloc (Var_Id); + Error_Msg_NE ("\ & declared #", N, Var_Id); + + Next_Elmt (Var_Elmt); + end loop; + end if; + end Report_Unused_Variables; + + Expr : constant Node_Id := + Get_Pragma_Arg (First (Pragma_Argument_Associations (N))); + Errors : constant Nat := Serious_Errors_Detected; + + -- Start of processing for Analyze_Initial_Condition_In_Decl_Part + + begin + Set_Analyzed (N); + + -- Pragma Initial_Condition depends on the names enumerated in pragma + -- Initializes. Without those, the analysis cannot take place. + + if No (Prag_Init) then + Error_Msg_Name_1 := Name_Initial_Condition; + Error_Msg_Name_2 := Name_Initializes; + + Error_Msg_N ("% requires the presence of aspect or pragma %", N); + return; + end if; + + -- The expression is preanalyzed because it has not been moved to its + -- final place yet. A direct analysis may generate sife effects and this + -- is not desired at this point. + + Preanalyze_And_Resolve (Expr, Standard_Boolean); + + -- Perform variable matching only when the expression is legal + + if Serious_Errors_Detected = Errors then + Collect_Variables; + + -- Verify that all variables mentioned in pragma Initializes are used + -- in the expression of pragma Initial_Condition. + + Match_Variables (Expr); + end if; + + -- Emit errors for all variables that should participate in the + -- expression of pragma Initial_Condition. + + if Serious_Errors_Detected = Errors then + Report_Unused_Variables; + end if; + end Analyze_Initial_Condition_In_Decl_Part; + -------------------------------------- -- Analyze_Initializes_In_Decl_Part -- -------------------------------------- @@ -2451,10 +2639,10 @@ 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_Declaration_Order (States : Node_Id; Inits : Node_Id); - -- Subsidiary routine to the analysis of pragmas Abstract_State and - -- Initializes. Determine whether pragma Abstract_State denoted by - -- States is defined earlier than pragma Initializes denoted by Inits. + procedure Check_Declaration_Order (First : Node_Id; Second : Node_Id); + -- Subsidiary routine to the analysis of pragmas Abstract_State, + -- Initial_Condition and Initializes. Determine whether pragma First + -- appears before pragma Second. If this is not the case, emit an error. procedure Check_Duplicate_Pragma (E : Entity_Id); -- Check if a rep item of the same name as the current pragma is already @@ -3433,7 +3621,7 @@ package body Sem_Prag is -- Check_Declaration_Order -- ----------------------------- - procedure Check_Declaration_Order (States : Node_Id; Inits : Node_Id) is + procedure Check_Declaration_Order (First : Node_Id; Second : Node_Id) is procedure Check_Aspect_Specification_Order; -- Inspect the aspect specifications of the context to determine the -- proper order. @@ -3443,33 +3631,34 @@ package body Sem_Prag is -------------------------------------- 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; + Asp_First : constant Node_Id := Corresponding_Aspect (First); + Asp_Second : constant Node_Id := Corresponding_Aspect (Second); + Asp : Node_Id; begin -- Both aspects must be part of the same aspect specification list - pragma Assert (List_Containing (Asp_I) = List_Containing (Asp_S)); + pragma Assert + (List_Containing (Asp_First) = List_Containing (Asp_Second)); - Asp := First (List_Containing (Asp_I)); + -- Try to reach Second starting from First in a left to right + -- traversal of the aspect specifications. + + Asp := Next (Asp_First); 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; + -- The order is ok, First is followed by Second - exit; + if Asp = Asp_Second then + return; end if; Next (Asp); end loop; + + -- If we get here, then the aspects are out of order + + Error_Msg_N ("aspect % cannot come after aspect %", First); end Check_Aspect_Specification_Order; -- Local variables @@ -3481,44 +3670,41 @@ package body Sem_Prag is begin -- Cannot check the order if one of the pragmas is missing - if No (States) or else No (Inits) then + if No (First) or else No (Second) 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; + Error_Msg_Name_1 := Pragma_Name (First); + Error_Msg_Name_2 := Pragma_Name (Second); - if From_Aspect_Specification (States) then + if From_Aspect_Specification (First) 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. + -- First is an aspect and Second a source pragma. - if From_Aspect_Specification (Inits) then + if From_Aspect_Specification (Second) 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); + if From_Aspect_Specification (Second) then + Error_Msg_N ("pragma % cannot come after aspect %", First); - -- Both pragmas are source constructs. Try to reach States from - -- Inits by traversing the declarations backwards. + -- Both pragmas are source constructs. Try to reach First from + -- Second by traversing the declarations backwards. else - Stmt := Prev (Inits); + Stmt := Prev (Second); while Present (Stmt) loop - -- The order is ok, Abstract_States is first followed by - -- Initializes. + -- The order is ok, First is followed by Second - if Nkind (Stmt) = N_Pragma - and then Pragma_Name (Stmt) = Name_Abstract_State - then + if Stmt = First then return; end if; @@ -3527,7 +3713,7 @@ package body Sem_Prag is -- If we get here, then the pragmas are out of order - Error_Msg_N ("pragma % cannot come after pragma %", States); + Error_Msg_N ("pragma % cannot come after pragma %", First); end if; end if; end Check_Declaration_Order; @@ -9318,8 +9504,8 @@ package body Sem_Prag is -- Initializes. Check_Declaration_Order - (States => N, - Inits => Get_Pragma (Pack_Id, Pragma_Initializes)); + (First => N, + Second => Get_Pragma (Pack_Id, Pragma_Initializes)); State := Expression (Arg1); @@ -9732,6 +9918,7 @@ package body Sem_Prag is -- Assume | -- Contract_Cases | -- Debug | + -- Initial_Condition | -- Loop_Invariant | -- Loop_Variant | -- Postcondition | @@ -13380,6 +13567,80 @@ package body Sem_Prag is end if; end Independent_Components; + ----------------------- + -- Initial_Condition -- + ----------------------- + + -- pragma Initial_Condition (boolean_EXPRESSION); + + when Pragma_Initial_Condition => Initial_Condition : 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. Initial_Condition + -- 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_Initial_Condition_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 pragma Initial_Condition with + -- respect to pragmas Abstract_State and Initializes. + + Check_Declaration_Order + (First => Get_Pragma (Pack_Id, Pragma_Abstract_State), + Second => N); + + Check_Declaration_Order + (First => Get_Pragma (Pack_Id, Pragma_Initializes), + Second => N); + end Initial_Condition; + ------------------------ -- Initialize_Scalars -- ------------------------ @@ -13461,8 +13722,8 @@ package body Sem_Prag is elsif not Comes_From_Source (Stmt) then null; - -- The pragma does not apply to a legal construct, issue an - -- error and stop the analysis. + -- The pragma does not apply to a legal construct, issue an + -- error and stop the analysis. else Pragma_Misplaced; @@ -13484,8 +13745,8 @@ package body Sem_Prag is -- Initializes. Check_Declaration_Order - (States => Get_Pragma (Pack_Id, Pragma_Abstract_State), - Inits => N); + (First => Get_Pragma (Pack_Id, Pragma_Abstract_State), + Second => N); end Initializes; ------------ @@ -16979,8 +17240,8 @@ package body Sem_Prag is elsif not Comes_From_Source (Stmt) then null; - -- The pragma does not apply to a legal construct, issue an - -- error and stop the analysis. + -- The pragma does not apply to a legal construct, issue an + -- error and stop the analysis. else Pragma_Misplaced; @@ -22429,6 +22690,7 @@ package body Sem_Prag is Pragma_Import_Valued_Procedure => 0, Pragma_Independent => 0, Pragma_Independent_Components => 0, + Pragma_Initial_Condition => -1, Pragma_Initialize_Scalars => -1, Pragma_Initializes => -1, Pragma_Inline => 0, @@ -22822,6 +23084,7 @@ package body Sem_Prag is Name_Assume | Name_Contract_Cases | Name_Debug | + Name_Initial_Condition | Name_Invariant | Name_uInvariant | Name_Loop_Invariant | diff --git a/gcc/ada/sem_prag.ads b/gcc/ada/sem_prag.ads index 3f7b3066059..9f88638e921 100644 --- a/gcc/ada/sem_prag.ads +++ b/gcc/ada/sem_prag.ads @@ -64,6 +64,9 @@ package Sem_Prag is -- Perform full analysis of delayed pragma Global. This routine is also -- capable of performing basic analysis of pragma Refind_Global. + procedure Analyze_Initial_Condition_In_Decl_Part (N : Node_Id); + -- Perform full analysis of delayed pragma Initial_Condition + procedure Analyze_Initializes_In_Decl_Part (N : Node_Id); -- Perform full analysis of delayed pragma Initializes diff --git a/gcc/ada/sem_util.adb b/gcc/ada/sem_util.adb index 83decce62f0..add58bf5aeb 100644 --- a/gcc/ada/sem_util.adb +++ b/gcc/ada/sem_util.adb @@ -229,10 +229,14 @@ package body Sem_Util is -- Contract items related to [generic] packages. The applicable pragmas -- are: -- Abstract_States + -- Initial_Condition -- Initializes if Ekind_In (Id, E_Generic_Package, E_Package) then - if Nam_In (Nam, Name_Abstract_State, Name_Initializes) then + if Nam_In (Nam, Name_Abstract_State, + Name_Initial_Condition, + Name_Initializes) + then Set_Next_Pragma (Prag, Classifications (Items)); Set_Classifications (Items, Prag); diff --git a/gcc/ada/sem_util.ads b/gcc/ada/sem_util.ads index 8eaa58014c8..bf9987cb7b8 100644 --- a/gcc/ada/sem_util.ads +++ b/gcc/ada/sem_util.ads @@ -50,6 +50,7 @@ package Sem_Util is -- Contract_Cases -- Depends -- Global + -- Initial_Condition -- Initializes -- Postcondition -- Precondition diff --git a/gcc/ada/sinfo.ads b/gcc/ada/sinfo.ads index ebe51f29d66..eecc2d49960 100644 --- a/gcc/ada/sinfo.ads +++ b/gcc/ada/sinfo.ads @@ -7198,6 +7198,7 @@ package Sinfo is -- Abstract_States -- Depends -- Global + -- Initial_Condition -- Initializes -- Refined_Depends -- Refined_Global diff --git a/gcc/ada/snames.ads-tmpl b/gcc/ada/snames.ads-tmpl index 74702f819e9..577e9ecadf0 100644 --- a/gcc/ada/snames.ads-tmpl +++ b/gcc/ada/snames.ads-tmpl @@ -509,6 +509,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_Initial_Condition : constant Name_Id := N + $; -- GNAT Name_Initializes : constant Name_Id := N + $; -- GNAT Name_Inline : constant Name_Id := N + $; Name_Inline_Always : constant Name_Id := N + $; -- GNAT @@ -1829,6 +1830,7 @@ package Snames is Pragma_Import_Valued_Procedure, Pragma_Independent, Pragma_Independent_Components, + Pragma_Initial_Condition, Pragma_Initializes, Pragma_Inline, Pragma_Inline_Always,