From: Hristian Kirtchev Date: Thu, 21 May 2015 13:26:51 +0000 (+0000) Subject: einfo.adb (Contract): This attribute now applies to constants. X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=eb7d283dc33d007ef49e76ba16680644869877c4;p=gcc.git einfo.adb (Contract): This attribute now applies to constants. 2015-05-21 Hristian Kirtchev * einfo.adb (Contract): This attribute now applies to constants. (Set_Contract): This attribute now applies to constants. (Write_Field34_Name): Add output for constants. * einfo.ads Attribute Contract now applies to constants. * sem_ch3.adb (Analyze_Object_Contract): Constants now have their Part_Of indicator verified. * sem_prag.adb (Analyze_Constituent): A constant is now a valid constituent. (Analyze_Global_Item): A constant cannot act as an output. (Analyze_Initialization_Item): Constants are now a valid initialization item. (Analyze_Initializes_In_Decl_Part): Rename global variable States_And_Vars to States_And_Objs and update all its occurrences. (Analyze_Input_Item): Constants are now a valid initialization item. Remove SPARM RM references from error messages. (Analyze_Pragma): Indicator Part_Of can now apply to a constant. (Collect_Body_States): Collect both source constants and variables. (Collect_States_And_Objects): Collect both source constants and variables. (Collect_States_And_Variables): Rename to Collect_States_And_Objects and update all its occurrences. (Collect_Visible_States): Do not collect constants and variables used to map generic formals to actuals. (Find_Role): The role of a constant is that of an input. Separate the role of a variable from that of a constant. (Report_Unused_Constituents): Add specialized wording for constants. (Report_Unused_States): Add specialized wording for constants. * sem_util.adb (Add_Contract_Item): Add processing for constants. * sem_util.ads (Add_Contract_Item): Update the comment on usage. (Find_Placement_In_State_Space): Update the comment on usage. From-SVN: r223484 --- diff --git a/gcc/ada/ChangeLog b/gcc/ada/ChangeLog index 464e9a580c5..27492bde478 100644 --- a/gcc/ada/ChangeLog +++ b/gcc/ada/ChangeLog @@ -1,3 +1,39 @@ +2015-05-21 Hristian Kirtchev + + * einfo.adb (Contract): This attribute now applies to constants. + (Set_Contract): This attribute now applies to constants. + (Write_Field34_Name): Add output for constants. + * einfo.ads Attribute Contract now applies to constants. + * sem_ch3.adb (Analyze_Object_Contract): Constants now have + their Part_Of indicator verified. + * sem_prag.adb (Analyze_Constituent): A constant is now a valid + constituent. + (Analyze_Global_Item): A constant cannot act as an output. + (Analyze_Initialization_Item): Constants are now a valid + initialization item. + (Analyze_Initializes_In_Decl_Part): Rename + global variable States_And_Vars to States_And_Objs and update + all its occurrences. + (Analyze_Input_Item): Constants are now a + valid initialization item. Remove SPARM RM references from error + messages. + (Analyze_Pragma): Indicator Part_Of can now apply to a constant. + (Collect_Body_States): Collect both source constants + and variables. + (Collect_States_And_Objects): Collect both source constants and + variables. + (Collect_States_And_Variables): Rename + to Collect_States_And_Objects and update all its occurrences. + (Collect_Visible_States): Do not collect constants and variables + used to map generic formals to actuals. + (Find_Role): The role of a constant is that of an input. Separate the + role of a variable from that of a constant. + (Report_Unused_Constituents): Add specialized wording for constants. + (Report_Unused_States): Add specialized wording for constants. + * sem_util.adb (Add_Contract_Item): Add processing for constants. + * sem_util.ads (Add_Contract_Item): Update the comment on usage. + (Find_Placement_In_State_Space): Update the comment on usage. + 2015-05-21 Ed Schonberg * sem_ch5.adb: minor reformatting. diff --git a/gcc/ada/einfo.adb b/gcc/ada/einfo.adb index af85c2b1063..78ad3dcf5f0 100644 --- a/gcc/ada/einfo.adb +++ b/gcc/ada/einfo.adb @@ -1175,7 +1175,8 @@ package body Einfo is function Contract (Id : E) return N is begin pragma Assert - (Ekind_In (Id, E_Entry, + (Ekind_In (Id, E_Constant, + E_Entry, E_Entry_Family, E_Generic_Package, E_Package, @@ -3748,7 +3749,8 @@ package body Einfo is procedure Set_Contract (Id : E; V : N) is begin pragma Assert - (Ekind_In (Id, E_Entry, + (Ekind_In (Id, E_Constant, + E_Entry, E_Entry_Family, E_Generic_Package, E_Package, @@ -10066,7 +10068,8 @@ package body Einfo is procedure Write_Field34_Name (Id : Entity_Id) is begin case Ekind (Id) is - when E_Entry | + when E_Constant | + E_Entry | E_Entry_Family | E_Generic_Package | E_Package | diff --git a/gcc/ada/einfo.ads b/gcc/ada/einfo.ads index bf21f76015f..f687d3d64b5 100644 --- a/gcc/ada/einfo.ads +++ b/gcc/ada/einfo.ads @@ -1096,10 +1096,10 @@ package Einfo is -- 'COUNT when it applies to a family member. -- Contract (Node34) --- Defined in entry, entry family, [generic] package, package body, --- [generic] subprogram, subprogram body and variable entities. Points --- to the contract of the entity, holding various assertion items and --- data classifiers. +-- Defined in constant, entry, entry family, [generic] package, package +-- body, [generic] subprogram, subprogram body, and variable entities. +-- 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 @@ -5633,6 +5633,7 @@ package Einfo is -- Activation_Record_Component (Node31) -- Encapsulating_State (Node32) (constants only) -- Linker_Section_Pragma (Node33) + -- Contract (Node34) (constants only) -- Has_Alignment_Clause (Flag46) -- Has_Atomic_Components (Flag86) -- Has_Biased_Representation (Flag139) diff --git a/gcc/ada/sem_ch3.adb b/gcc/ada/sem_ch3.adb index 565efe01dbb..47f6e701b17 100644 --- a/gcc/ada/sem_ch3.adb +++ b/gcc/ada/sem_ch3.adb @@ -3205,6 +3205,8 @@ package body Sem_Ch3 is return; end if; + -- Constant related checks + if Ekind (Obj_Id) = E_Constant then -- A constant cannot be effectively volatile. This check is only @@ -3224,6 +3226,8 @@ package body Sem_Ch3 is Error_Msg_N ("constant cannot be volatile", Obj_Id); end if; + -- Variable related checks + else pragma Assert (Ekind (Obj_Id) = E_Variable); -- The following checks are only relevant when SPARK_Mode is on as @@ -3323,15 +3327,15 @@ package body Sem_Ch3 is if Seen then Check_External_Properties (Obj_Id, AR_Val, AW_Val, ER_Val, EW_Val); end if; + end if; - -- Check whether the lack of indicator Part_Of agrees with the - -- placement of the variable with respect to the state space. + -- Check whether the lack of indicator Part_Of agrees with the placement + -- of the object with respect to the state space. - Prag := Get_Pragma (Obj_Id, Pragma_Part_Of); + Prag := Get_Pragma (Obj_Id, Pragma_Part_Of); - if No (Prag) then - Check_Missing_Part_Of (Obj_Id); - end if; + if No (Prag) then + Check_Missing_Part_Of (Obj_Id); end if; -- A ghost object cannot be imported or exported (SPARK RM 6.9(8)) diff --git a/gcc/ada/sem_prag.adb b/gcc/ada/sem_prag.adb index a4e7db52dad..7fb33b49cb0 100644 --- a/gcc/ada/sem_prag.adb +++ b/gcc/ada/sem_prag.adb @@ -497,7 +497,7 @@ package body Sem_Prag is -- A flag used to track the legality of a null output Result_Seen : Boolean := False; - -- A flag set when Subp_Id'Result is processed + -- A flag set when Spec_Id'Result is processed States_Seen : Elist_Id := No_Elist; -- A list containing the entities of all states processed so far. It @@ -1048,6 +1048,11 @@ package body Sem_Prag is Item_Is_Output := True; end if; + -- Constant case + + elsif Ekind (Item_Id) = E_Constant then + Item_Is_Input := True; + -- Generic parameter cases elsif Ekind (Item_Id) = E_Generic_In_Parameter then @@ -1087,16 +1092,16 @@ package body Sem_Prag is Item_Is_Output := True; end if; - -- Object cases + -- Variable case - else pragma Assert (Ekind_In (Item_Id, E_Constant, E_Variable)); + else pragma Assert (Ekind (Item_Id) = E_Variable); - -- When pragma Global is present, the mode of the object may + -- When pragma Global is present, the mode of the variable may -- be further constrained by setting a more restrictive mode. if Global_Seen then - -- An object has mode IN when its type is unconstrained or + -- A variable has mode IN when its type is unconstrained or -- tagged because array bounds, discriminants or tags can be -- read. @@ -1110,7 +1115,7 @@ package body Sem_Prag is Item_Is_Output := True; end if; - -- Otherwise the object has a default IN OUT mode + -- Otherwise the variable has a default IN OUT mode else Item_Is_Input := True; @@ -1920,6 +1925,19 @@ package body Sem_Prag is Ref => Item); end if; + -- Constant related checks + + elsif Ekind (Item_Id) = E_Constant then + + -- A constant is read-only item, therefore it cannot act as + -- an output. + + if Nam_In (Global_Mode, Name_In_Out, Name_Output) then + SPARK_Msg_NE + ("constant & cannot act as output", Item, Item_Id); + return; + end if; + -- Variable related checks. These are only relevant when -- SPARK_Mode is on as they are not standard Ada legality -- rules. @@ -2275,8 +2293,8 @@ package body Sem_Prag is 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 + States_And_Objs : Elist_Id := No_Elist; + -- A list of all abstract states and objects declared in the visible -- declarations of the related package. This list is used to detect the -- legality of initialization items. @@ -2292,9 +2310,9 @@ package body Sem_Prag is -- Verify the legality of a single initialization item followed by a -- list of input items. - procedure Collect_States_And_Variables; + procedure Collect_States_And_Objects; -- Inspect the visible declarations of the related package and gather - -- the entities of all abstract states and variables in States_And_Vars. + -- the entities of all abstract states and objects in States_And_Objs. --------------------------------- -- Analyze_Initialization_Item -- @@ -2333,12 +2351,14 @@ package body Sem_Prag is if Is_Entity_Name (Item) then Item_Id := Entity_Of (Item); - if Ekind_In (Item_Id, E_Abstract_State, E_Variable) then - + if Ekind_In (Item_Id, E_Abstract_State, + E_Constant, + E_Variable) + then -- The state or variable must be declared in the visible -- declarations of the package (SPARK RM 7.1.5(7)). - if not Contains (States_And_Vars, Item_Id) then + if not Contains (States_And_Objs, Item_Id) then Error_Msg_Name_1 := Chars (Pack_Id); SPARK_Msg_NE ("initialization item & must appear in the visible " @@ -2365,13 +2385,12 @@ package body Sem_Prag is end if; end if; - -- The item references something that is not a state or a - -- variable (SPARK RM 7.1.5(3)). + -- The item references something that is not a state or object + -- (SPARK RM 7.1.5(3)). else SPARK_Msg_N - ("initialization item must denote variable or state", - Item); + ("initialization item must denote object or state", Item); end if; -- Some form of illegal construct masquerading as a name @@ -2379,7 +2398,7 @@ package body Sem_Prag is else Error_Msg_N - ("initialization item must denote variable or state", Item); + ("initialization item must denote object or state", Item); end if; end if; end Analyze_Initialization_Item; @@ -2439,20 +2458,20 @@ package body Sem_Prag is Input_Id := Entity_Of (Input); if Ekind_In (Input_Id, E_Abstract_State, + E_Constant, E_In_Parameter, E_In_Out_Parameter, E_Out_Parameter, E_Variable) then - -- The input cannot denote states or variables declared - -- within the related package. + -- The input cannot denote states or objects declared + -- within the related package (SPARK RM 7.1.5(4)). if Within_Scope (Input_Id, Current_Scope) then Error_Msg_Name_1 := Chars (Pack_Id); SPARK_Msg_NE - ("input item & cannot denote a visible variable or " - & "state of package % (SPARK RM 7.1.5(4))", - Input, Input_Id); + ("input item & cannot denote a visible object or " + & "state of package %", Input, Input_Id); -- Detect a duplicate use of the same input item -- (SPARK RM 7.1.5(5)). @@ -2469,27 +2488,29 @@ package body Sem_Prag is Add_Item (Input_Id, States_Seen); end if; - if Ekind_In (Input_Id, E_Abstract_State, E_Variable) + if Ekind_In (Input_Id, E_Abstract_State, + E_Constant, + E_Variable) and then Present (Encapsulating_State (Input_Id)) then Add_Item (Input_Id, Constits_Seen); end if; end if; - -- The input references something that is not a state or a - -- variable (SPARK RM 7.1.5(3)). + -- The input references something that is not a state or an + -- object (SPARK RM 7.1.5(3)). else SPARK_Msg_N - ("input item must denote variable or state", Input); + ("input item must denote object or state", Input); end if; -- Some form of illegal construct masquerading as a name - -- (SPARK RM 7.1.5(3)). + -- (SPARK RM 7.1.5(3)). This is a syntax error, always report. else - SPARK_Msg_N - ("input item must denote variable or state", Input); + Error_Msg_N + ("input item must denote object or state", Input); end if; end if; end Analyze_Input_Item; @@ -2543,11 +2564,11 @@ package body Sem_Prag is end if; end Analyze_Initialization_Item_With_Inputs; - ---------------------------------- - -- Collect_States_And_Variables -- - ---------------------------------- + -------------------------------- + -- Collect_States_And_Objects -- + -------------------------------- - procedure Collect_States_And_Variables is + procedure Collect_States_And_Objects is Pack_Spec : constant Node_Id := Specification (Pack_Decl); Decl : Node_Id; @@ -2555,26 +2576,25 @@ package body Sem_Prag is -- 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)); + States_And_Objs := New_Copy_Elist (Abstract_States (Pack_Id)); end if; - -- Collect all variables the appear in the visible declarations of - -- the related package. + -- Collect all objects 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) + if Comes_From_Source (Decl) + and then Nkind (Decl) = N_Object_Declaration then - Add_Item (Defining_Entity (Decl), States_And_Vars); + Add_Item (Defining_Entity (Decl), States_And_Objs); end if; Next (Decl); end loop; end if; - end Collect_States_And_Variables; + end Collect_States_And_Objects; -- Local variables @@ -2600,7 +2620,7 @@ package body Sem_Prag is -- Initialize the various lists used during analysis - Collect_States_And_Variables; + Collect_States_And_Objects; if Present (Expressions (Inits)) then Init := First (Expressions (Inits)); @@ -3360,7 +3380,7 @@ package body Sem_Prag is return; end if; - -- Determine where the state, variable or the package instantiation + -- Determine where the state, object or the package instantiation -- lives with respect to the enclosing packages or package bodies (if -- any). This placement dictates the legality of the encapsulating -- state. @@ -17380,7 +17400,7 @@ package body Sem_Prag is State_Id : Entity_Id; Instance : Node_Id); -- Propagate the Part_Of indicator to all abstract states and - -- variables declared in the visible state space of a package + -- objects declared in the visible state space of a package -- denoted by Pack_Id. State_Id is the encapsulating state. -- Instance is the package instantiation node. @@ -17399,7 +17419,7 @@ package body Sem_Prag is procedure Propagate_Part_Of (Pack_Id : Entity_Id); -- Propagate the Part_Of indicator to all abstract states and - -- variables declared in the visible state space of a package + -- objects declared in the visible state space of a package -- denoted by Pack_Id. ----------------------- @@ -17411,8 +17431,8 @@ package body Sem_Prag is begin -- Traverse the entity chain of the package and set relevant - -- attributes of abstract states and variables declared in - -- the visible state space of the package. + -- attributes of abstract states and objects declared in the + -- visible state space of the package. Item_Id := First_Entity (Pack_Id); while Present (Item_Id) @@ -17423,11 +17443,11 @@ package body Sem_Prag is if not Comes_From_Source (Item_Id) then null; - -- The Part_Of indicator turns an abstract state or a - -- variable into a constituent of the encapsulating - -- state. + -- The Part_Of indicator turns an abstract state or an + -- object into a constituent of the encapsulating state. elsif Ekind_In (Item_Id, E_Abstract_State, + E_Constant, E_Variable) then Has_Item := True; @@ -17476,7 +17496,7 @@ package body Sem_Prag is Check_Arg_Count (1); -- Ensure the proper placement of the pragma. Part_Of must appear - -- on a variable declaration or a package instantiation. + -- on an object declaration or a package instantiation. Stmt := Prev (N); while Present (Stmt) loop @@ -17515,16 +17535,6 @@ package body Sem_Prag is Stmt := Prev (Stmt); end loop; - -- When the context is an object declaration, ensure that it is a - -- variable. - - if Nkind (Stmt) = N_Object_Declaration - and then Ekind (Defining_Entity (Stmt)) /= E_Variable - then - SPARK_Msg_N ("indicator Part_Of must apply to a variable", N); - return; - end if; - -- Extract the entity of the related object declaration or package -- instantiation. In the case of the instantiation, use the entity -- of the instance spec. @@ -17549,10 +17559,10 @@ package body Sem_Prag is if Legal then State_Id := Entity (State); - -- The Part_Of indicator turns a variable into a constituent - -- of the encapsulating state. + -- The Part_Of indicator turns an object into a constituent of + -- the encapsulating state. - if Ekind (Item_Id) = E_Variable then + if Ekind_In (Item_Id, E_Constant, E_Variable) then Append_Elmt (Item_Id, Part_Of_Constituents (State_Id)); Set_Encapsulating_State (Item_Id, State_Id); @@ -21983,7 +21993,7 @@ package body Sem_Prag is -- 2) Dep_Item denotes null and Ref_Item is Empty (special case) -- 3) Both items denote attribute 'Result -- 4) Both items denote the same formal parameter - -- 5) Both items denote the same variable + -- 5) Both items denote the same object -- 6) Dep_Item is an abstract state with visible null refinement -- and Ref_Item denotes null. -- 7) Dep_Item is an abstract state with visible null refinement @@ -22079,7 +22089,7 @@ package body Sem_Prag is then Matched := True; - -- Abstract states, formal parameters and variables + -- Abstract states, formal parameters and objects elsif Is_Entity_Name (Dep_Item) then @@ -22127,7 +22137,7 @@ package body Sem_Prag is Matched := True; end if; - -- A formal parameter or a variable matches itself + -- A formal parameter or an object matches itself elsif Is_Entity_Name (Ref_Item) and then Entity_Of (Ref_Item) = Dep_Item_Id @@ -23392,7 +23402,6 @@ package body Sem_Prag is Item := First (Expressions (List)); while Present (Item) loop Check_Refined_Global_Item (Item, Global_Mode); - Next (Item); end loop; @@ -23770,7 +23779,7 @@ package body Sem_Prag is -- Perform full analysis of a single refinement clause function Collect_Body_States (Pack_Id : Entity_Id) return Elist_Id; - -- Gather the entities of all abstract states and variables declared in + -- Gather the entities of all abstract states and objects declared in -- the body state space of package Pack_Id. procedure Report_Unrefined_States (States : Elist_Id); @@ -23953,7 +23962,6 @@ package body Sem_Prag is if Node (State_Elmt) = Constit_Id then Check_Ghost_Constituent (Constit_Id); - Remove_Elmt (Body_States, State_Elmt); Collect_Constituent; return; @@ -24079,7 +24087,10 @@ package body Sem_Prag is if Is_Entity_Name (Constit) then Constit_Id := Entity_Of (Constit); - if Ekind_In (Constit_Id, E_Abstract_State, E_Variable) then + if Ekind_In (Constit_Id, E_Abstract_State, + E_Constant, + E_Variable) + then Check_Matching_Constituent (Constit_Id); else @@ -24210,7 +24221,13 @@ package body Sem_Prag is if Ekind (Constit_Id) = E_Abstract_State then SPARK_Msg_NE ("\abstract state & defined #", State, Constit_Id); + + elsif Ekind (Constit_Id) = E_Constant then + SPARK_Msg_NE + ("\constant & defined #", State, Constit_Id); + else + pragma Assert (Ekind (Constit_Id) = E_Variable); SPARK_Msg_NE ("\variable & defined #", State, Constit_Id); end if; @@ -24405,6 +24422,7 @@ package body Sem_Prag is ---------------------------- procedure Collect_Visible_States (Pack_Id : Entity_Id) is + Decl : Node_Id; Item_Id : Entity_Id; begin @@ -24420,9 +24438,20 @@ package body Sem_Prag is if not Comes_From_Source (Item_Id) then null; - elsif Ekind_In (Item_Id, E_Abstract_State, E_Variable) then + elsif Ekind (Item_Id) = E_Abstract_State then Add_Item (Item_Id, Result); + elsif Ekind_In (Item_Id, E_Constant, E_Variable) then + Decl := Declaration_Node (Item_Id); + + -- Do not consider constants or variables that map generic + -- formals to their actuals as the formals cannot be named + -- from the outside and participate in refinement. + + if No (Corresponding_Generic_Association (Decl)) then + Add_Item (Item_Id, Result); + end if; + -- Recursively gather the visible states of a nested package elsif Ekind (Item_Id) = E_Package then @@ -24448,24 +24477,23 @@ package body Sem_Prag is Decl := First (Declarations (Pack_Body)); while Present (Decl) loop + + -- Capture source objects as internally generated temporaries + -- cannot be named and participate in refinement. + if Nkind (Decl) = N_Object_Declaration then Item_Id := Defining_Entity (Decl); - -- Capture source variables as internally generated temporaries - -- cannot be named and participate in refinement. - - if Ekind (Item_Id) = E_Variable - and then Comes_From_Source (Item_Id) - then + if Comes_From_Source (Item_Id) then Add_Item (Item_Id, Result); end if; + -- Capture the visible abstract states and objects of a source + -- package [instantiation]. + elsif Nkind (Decl) = N_Package_Declaration then Item_Id := Defining_Entity (Decl); - -- Capture the visible abstract states and objects of a - -- source package [instantiation]. - if Comes_From_Source (Item_Id) then Collect_Visible_States (Item_Id); end if; @@ -24529,7 +24557,12 @@ package body Sem_Prag is if Ekind (State_Id) = E_Abstract_State then SPARK_Msg_NE ("\abstract state & defined #", Body_Id, State_Id); + + elsif Ekind (State_Id) = E_Constant then + SPARK_Msg_NE ("\constant & defined #", Body_Id, State_Id); + else + pragma Assert (Ekind (State_Id) = E_Variable); SPARK_Msg_NE ("\variable & defined #", Body_Id, State_Id); end if; @@ -24553,7 +24586,7 @@ package body Sem_Prag is Available_States := New_Copy_Elist (Abstract_States (Spec_Id)); - -- Gather all abstract states and variables declared in the visible + -- Gather all abstract states and objects declared in the visible -- state space of the package body. These items must be utilized as -- constituents in a state refinement. @@ -24571,7 +24604,6 @@ package body Sem_Prag is Clause := First (Component_Associations (Clauses)); while Present (Clause) loop Analyze_Refinement_Clause (Clause); - Next (Clause); end loop; end if; @@ -24587,7 +24619,7 @@ package body Sem_Prag is Report_Unrefined_States (Available_States); - -- Ensure that all abstract states and variables declared in the body + -- Ensure that all abstract states and objects declared in the body -- state space of the related package are utilized as constituents. Report_Unused_States (Body_States); diff --git a/gcc/ada/sem_util.adb b/gcc/ada/sem_util.adb index 01dc53163d9..716c2d84c3e 100644 --- a/gcc/ada/sem_util.adb +++ b/gcc/ada/sem_util.adb @@ -312,6 +312,19 @@ package body Sem_Util is Set_Contract (Id, Items); end if; + -- Contract items related to constants. Applicable pragmas are: + -- Part_Of + + if Ekind (Id) = E_Constant then + if Prag_Nam = Name_Part_Of then + Add_Classification; + + -- The pragma is not a proper contract item + + else + raise Program_Error; + end if; + -- Contract items related to [generic] packages or instantiations. The -- applicable pragmas are: -- Abstract_States @@ -319,7 +332,7 @@ package body Sem_Util is -- Initializes -- Part_Of (instantiation only) - if Ekind_In (Id, E_Generic_Package, E_Package) then + elsif Ekind_In (Id, E_Generic_Package, E_Package) then if Nam_In (Prag_Nam, Name_Abstract_State, Name_Initial_Condition, Name_Initializes) diff --git a/gcc/ada/sem_util.ads b/gcc/ada/sem_util.ads index 84d04903c72..910b282d4d4 100644 --- a/gcc/ada/sem_util.ads +++ b/gcc/ada/sem_util.ads @@ -50,7 +50,7 @@ package Sem_Util is -- block already has an identifier, Id returns the entity of its label. procedure Add_Contract_Item (Prag : Node_Id; Id : Entity_Id); - -- Add pragma Prag to the contract of an entry, a package [body], a + -- Add pragma Prag to the contract of a constant, entry, package [body], -- subprogram [body] or variable denoted by Id. The following are valid -- pragmas: -- Abstract_State @@ -733,10 +733,10 @@ package Sem_Util is Placement : out State_Space_Kind; Pack_Id : out Entity_Id); -- Determine the state space placement of an item. Item_Id denotes the - -- entity of an abstract state, variable or package instantiation. - -- Placement captures the precise placement of the item in the enclosing - -- state space. If the state space is that of a package, Pack_Id denotes - -- its entity, otherwise Pack_Id is Empty. + -- entity of an abstract state, object or package instantiation. Placement + -- captures the precise placement of the item in the enclosing state space. + -- If the state space is that of a package, Pack_Id denotes its entity, + -- otherwise Pack_Id is Empty. function Find_Static_Alternative (N : Node_Id) return Node_Id; -- N is a case statement whose expression is a compile-time value.