einfo.adb (Contract): This attribute now applies to constants.

2015-05-21  Hristian Kirtchev  <kirtchev@adacore.com>

	* 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

gcc/ada/ChangeLog

+2015-05-21  Hristian Kirtchev  <kirtchev@adacore.com>
+
+	* 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  <schonberg@adacore.com>
 
 	* sem_ch5.adb: minor reformatting.

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                                    |

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)

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))

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)

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.