diff mbox

[Ada] Allow constants in SPARK contracts

Message ID 20150521132727.GA23471@adacore.com
State New
Headers show

Commit Message

Arnaud Charlet May 21, 2015, 1:27 p.m. UTC 
This patch permits constants to appear in the following SPARK annotations:

   Depends
   Global
   Initializes
   Part_Of
   Refined_Depends
   Refined_Global
   Refined_State

------------
-- Source --
------------

--  legal_usage.ads

package Legal_Usage
  with SPARK_Mode,
       Abstract_State    => State,
       Initializes       => (C1, C2),
       Initial_Condition => (C1 = 1 and then C2 = 2)
is
   C1 : constant Integer := 1;
   C2 : constant Integer := 2;

   function Func (Formal : Integer) return Integer
     with Global  => (Input => (C1, C2, State)),
          Depends => (Func'Result => (Formal, C1, C2, State));

private
   C3 : constant Integer := 3 with Part_Of => State;
end Legal_Usage;

--  legal_usage.adb

package body Legal_Usage
  with SPARK_Mode,
       Refined_State => (State => (C3, C4))
is
   C4 : constant Integer := 4;

   function Func (Formal : Integer) return Integer
     with Refined_Global  => (Input => (C1, C2, C3, C4)),
          Refined_Depends => (Func'Result => (Formal, C1, C2, C3, C4))
   is
   begin
      return Formal + C1 + C2 + C3 + C4;
   end Func;
end Legal_Usage;

--  illegal_usage.ads

package Illegal_Usage is
   C1 : constant Integer := 1;

   procedure Error_1
     with Global => (In_Out => C1);

   procedure Error_2
     with Global => (Output => C1);

   procedure Error_3 (Formal : Integer)
     with Depends => (C1 => Formal);

   procedure Error_4 (Formal : Integer)
     with Global  => (Input => C1),
          Depends => (C1 => Formal);
end Illegal_Usage;

----------------------------
-- Compilation and output --
----------------------------

$ gcc -c legal_usage.adb
$ gcc -c illegal_usage.adb
illegal_usage.ads:5:32: constant "C1" cannot act as output
illegal_usage.ads:8:32: constant "C1" cannot act as output
illegal_usage.ads:11:23: read-only constant "C1" cannot appear as output in
  dependence relation
illegal_usage.ads:14:32: constant "C1" must appear in at least one input
  dependence list
illegal_usage.ads:15:23: read-only constant "C1" cannot appear as output in
  dependence relation

Tested on x86_64-pc-linux-gnu, committed on trunk

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.
diff mbox

Patch

Index: sem_ch3.adb
===================================================================
--- sem_ch3.adb	(revision 223477)
+++ sem_ch3.adb	(working copy)
@@ -3205,6 +3205,8 @@ 
          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 @@ 
             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 @@ 
          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))
Index: einfo.adb
===================================================================
--- einfo.adb	(revision 223476)
+++ einfo.adb	(working copy)
@@ -1175,7 +1175,8 @@ 
    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 @@ 
    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 @@ 
    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                                    |
Index: einfo.ads
===================================================================
--- einfo.ads	(revision 223476)
+++ einfo.ads	(working copy)
@@ -1096,10 +1096,10 @@ 
 --       '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 @@ 
    --    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)
Index: sem_prag.adb
===================================================================
--- sem_prag.adb	(revision 223476)
+++ sem_prag.adb	(working copy)
@@ -497,7 +497,7 @@ 
       --  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 @@ 
                   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 @@ 
                   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 @@ 
                      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 @@ 
                         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 @@ 
       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 @@ 
       --  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 @@ 
             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 @@ 
                      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 @@ 
 
             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 @@ 
                   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 @@ 
                            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 @@ 
          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 @@ 
          --  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 @@ 
 
       --  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 @@ 
             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 @@ 
                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 @@ 
 
                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 @@ 
 
                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 @@ 
                      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 @@ 
             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 @@ 
                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 @@ 
             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 @@ 
          --    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 @@ 
             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 @@ 
                      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 @@ 
                Item := First (Expressions (List));
                while Present (Item) loop
                   Check_Refined_Global_Item (Item, Global_Mode);
-
                   Next (Item);
                end loop;
 
@@ -23770,7 +23779,7 @@ 
       --  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 @@ 
 
                         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 @@ 
                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 @@ 
                   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 @@ 
          ----------------------------
 
          procedure Collect_Visible_States (Pack_Id : Entity_Id) is
+            Decl    : Node_Id;
             Item_Id : Entity_Id;
 
          begin
@@ -24420,9 +24438,20 @@ 
                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 @@ 
 
          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 @@ 
                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 @@ 
 
       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 @@ 
             Clause := First (Component_Associations (Clauses));
             while Present (Clause) loop
                Analyze_Refinement_Clause (Clause);
-
                Next (Clause);
             end loop;
          end if;
@@ -24587,7 +24619,7 @@ 
 
       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);
Index: sem_util.adb
===================================================================
--- sem_util.adb	(revision 223476)
+++ sem_util.adb	(working copy)
@@ -312,6 +312,19 @@ 
          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 @@ 
       --    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)
Index: sem_util.ads
===================================================================
--- sem_util.ads	(revision 223476)
+++ sem_util.ads	(working copy)
@@ -50,7 +50,7 @@ 
    --  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 @@ 
       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.