[multiple changes]

2013-10-10  Hristian Kirtchev  <kirtchev@adacore.com>

	* aspects.adb: Add an entry in table Canonical_Aspect for
	Refined_State.
	* aspects.ads: Add entries in tables Aspect_Id, Aspect_Argument,
	Aspect_Names and Aspect_Delay for Refined_State.
	* einfo.adb: Add with and use clauses for Elists.
	Remove Refined_State from the list of node usage.
	Add Refined_State_Pragma to the list of node usage.
	(Has_Null_Abstract_State): New routine.
	(Refined_State): Removed.
	(Refined_State_Pragma): New routine.
	(Set_Refined_State): Removed.
	(Set_Refined_State_Pragma): New routine.
	(Write_Field8_Name): Add output for Refined_State_Pragma.
	(Write_Field9_Name): Remove the output for Refined_State.
	* einfo.ads: Add new synthesized attribute Has_Null_Abstract_State
	along with usage in nodes.  Remove attribute Refined_State along
	with usage in nodes.  Add new attribute Refined_State_Pragma along
	with usage in nodes.
	(Has_Null_Abstract_State): New routine.
	(Refined_State): Removed.
	(Refined_State_Pragma): New routine.
	(Set_Refined_State): Removed.
	(Set_Refined_State_Pragma): New routine.
	* elists.adb (Clone): New routine.
	* elists.ads (Clone): New routine.
	* par-prag.adb: Add Refined_State to the pragmas that do not
	require special processing by the parser.
	* sem_ch3.adb: Add with and use clause for Sem_Prag.
	(Analyze_Declarations): Add local variables Body_Id, Context and
	Spec_Id. Add processing for delayed aspect/pragma Refined_State.
	* sem_ch13.adb (Analyze_Aspect_Specifications): Update the
	handling of aspect Abstract_State.  Add processing for aspect
	Refined_State. Remove the bizzare insertion policy for aspect
	Abstract_State.
	(Check_Aspect_At_Freeze_Point): Add an entry for Refined_State.
	* sem_prag.adb: Add an entry to table Sig_Flags
	for pragma Refined_State.
	(Add_Item): Update the
	comment on usage. The inserted items need not be unique.
	(Analyze_Contract_Cases_In_Decl_Part): Rename variable Restore to
	Restore_Scope and update all its occurrences.
	(Analyze_Pragma):
	Update the handling of pragma Abstract_State. Add processing for
	pragma Refined_State.
	(Analyze_Pre_Post_Condition_In_Decl_Part):
	Rename variable Restore to Restore_Scope and update all its
	occurrences.
	(Analyze_Refined_State_In_Decl_Part): New routine.
	* sem_prag.ads (Analyze_Refined_State_In_Decl_Part): New routine.
	* snames.ads-tmpl: Add new predefined name for Refined_State. Add
	new Pragma_Id for Refined_State.

2013-10-10  Ed Schonberg  <schonberg@adacore.com>

	* sem_ch10.adb (Install_Limited_Withed_Unit): handle properly the
	case of a record declaration in a limited view, when the record
	contains a self-referential component of an anonymous access type.

From-SVN: r203371

gcc/ada/ChangeLog

+2013-10-10  Hristian Kirtchev  <kirtchev@adacore.com>
+
+	* aspects.adb: Add an entry in table Canonical_Aspect for
+	Refined_State.
+	* aspects.ads: Add entries in tables Aspect_Id, Aspect_Argument,
+	Aspect_Names and Aspect_Delay for Refined_State.
+	* einfo.adb: Add with and use clauses for Elists.
+	Remove Refined_State from the list of node usage.
+	Add Refined_State_Pragma to the list of node usage.
+	(Has_Null_Abstract_State): New routine.
+	(Refined_State): Removed.
+	(Refined_State_Pragma): New routine.
+	(Set_Refined_State): Removed.
+	(Set_Refined_State_Pragma): New routine.
+	(Write_Field8_Name): Add output for Refined_State_Pragma.
+	(Write_Field9_Name): Remove the output for Refined_State.
+	* einfo.ads: Add new synthesized attribute Has_Null_Abstract_State
+	along with usage in nodes.  Remove attribute Refined_State along
+	with usage in nodes.  Add new attribute Refined_State_Pragma along
+	with usage in nodes.
+	(Has_Null_Abstract_State): New routine.
+	(Refined_State): Removed.
+	(Refined_State_Pragma): New routine.
+	(Set_Refined_State): Removed.
+	(Set_Refined_State_Pragma): New routine.
+	* elists.adb (Clone): New routine.
+	* elists.ads (Clone): New routine.
+	* par-prag.adb: Add Refined_State to the pragmas that do not
+	require special processing by the parser.
+	* sem_ch3.adb: Add with and use clause for Sem_Prag.
+	(Analyze_Declarations): Add local variables Body_Id, Context and
+	Spec_Id. Add processing for delayed aspect/pragma Refined_State.
+	* sem_ch13.adb (Analyze_Aspect_Specifications): Update the
+	handling of aspect Abstract_State.  Add processing for aspect
+	Refined_State. Remove the bizzare insertion policy for aspect
+	Abstract_State.
+	(Check_Aspect_At_Freeze_Point): Add an entry for Refined_State.
+	* sem_prag.adb: Add an entry to table Sig_Flags
+	for pragma Refined_State.
+	(Add_Item): Update the
+	comment on usage. The inserted items need not be unique.
+	(Analyze_Contract_Cases_In_Decl_Part): Rename variable Restore to
+	Restore_Scope and update all its occurrences.
+	(Analyze_Pragma):
+	Update the handling of pragma Abstract_State. Add processing for
+	pragma Refined_State.
+	(Analyze_Pre_Post_Condition_In_Decl_Part):
+	Rename variable Restore to Restore_Scope and update all its
+	occurrences.
+	(Analyze_Refined_State_In_Decl_Part): New routine.
+	* sem_prag.ads (Analyze_Refined_State_In_Decl_Part): New routine.
+	* snames.ads-tmpl: Add new predefined name for Refined_State. Add
+	new Pragma_Id for Refined_State.
+
+2013-10-10  Ed Schonberg  <schonberg@adacore.com>
+
+	* sem_ch10.adb (Install_Limited_Withed_Unit): handle properly the
+	case of a record declaration in a limited view, when the record
+	contains a self-referential component of an anonymous access type.
+
 2013-10-10  Thomas Quinot  <quinot@adacore.com>
 
 	* exp_ch4.adb (Process_Transient_Object): For any context other

gcc/ada/aspects.adb

@@ -470,6 +470,7 @@ package body Aspects is
     Aspect_Refined_Global               => Aspect_Refined_Global,
     Aspect_Refined_Post                 => Aspect_Refined_Post,
     Aspect_Refined_Pre                  => Aspect_Refined_Pre,
+    Aspect_Refined_State                => Aspect_Refined_State,
     Aspect_Remote_Access_Type           => Aspect_Remote_Access_Type,
     Aspect_Remote_Call_Interface        => Aspect_Remote_Call_Interface,
     Aspect_Remote_Types                 => Aspect_Remote_Types,

gcc/ada/aspects.ads

@@ -115,6 +115,7 @@ package Aspects is
       Aspect_Refined_Global,                -- GNAT
       Aspect_Refined_Post,                  -- GNAT
       Aspect_Refined_Pre,                   -- GNAT
+      Aspect_Refined_State,                 -- GNAT
       Aspect_Relative_Deadline,
       Aspect_Scalar_Storage_Order,          -- GNAT
       Aspect_Simple_Storage_Pool,           -- GNAT
@@ -327,6 +328,7 @@ package Aspects is
       Aspect_Refined_Global          => Expression,
       Aspect_Refined_Post            => Expression,
       Aspect_Refined_Pre             => Expression,
+      Aspect_Refined_State           => Expression,
       Aspect_Relative_Deadline       => Expression,
       Aspect_Scalar_Storage_Order    => Expression,
       Aspect_Simple_Storage_Pool     => Name,
@@ -427,6 +429,7 @@ package Aspects is
       Aspect_Refined_Global               => Name_Refined_Global,
       Aspect_Refined_Post                 => Name_Refined_Post,
       Aspect_Refined_Pre                  => Name_Refined_Pre,
+      Aspect_Refined_State                => Name_Refined_State,
       Aspect_Relative_Deadline            => Name_Relative_Deadline,
       Aspect_Remote_Access_Type           => Name_Remote_Access_Type,
       Aspect_Remote_Call_Interface        => Name_Remote_Call_Interface,
@@ -620,6 +623,7 @@ package Aspects is
       Aspect_Read                         => Always_Delay,
       Aspect_Refined_Depends              => Always_Delay,
       Aspect_Refined_Global               => Always_Delay,
+      Aspect_Refined_State                => Always_Delay,
       Aspect_Relative_Deadline            => Always_Delay,
       Aspect_Remote_Access_Type           => Always_Delay,
       Aspect_Remote_Call_Interface        => Always_Delay,

gcc/ada/einfo.adb

@@ -33,6 +33,7 @@ pragma Style_Checks (All_Checks);
 --  Turn off subprogram ordering, not used for this unit
 
 with Atree;   use Atree;
+with Elists;  use Elists;
 with Namet;   use Namet;
 with Nlists;  use Nlists;
 with Output;  use Output;
@@ -79,12 +80,12 @@ package body Einfo is
    --    Mechanism                       Uint8 (but returns Mechanism_Type)
    --    Normalized_First_Bit            Uint8
    --    Postcondition_Proc              Node8
+   --    Refined_State_Pragma            Node8
    --    Return_Applies_To               Node8
    --    First_Exit_Statement            Node8
 
    --    Class_Wide_Type                 Node9
    --    Current_Value                   Node9
-   --    Refined_State                   Node9
    --    Renaming_Map                    Uint9
 
    --    Direct_Primitive_Operations     Elist10
@@ -2647,11 +2648,11 @@ package body Einfo is
       return Flag227 (Id);
    end Referenced_As_Out_Parameter;
 
-   function Refined_State (Id : E) return E is
+   function Refined_State_Pragma (Id : E) return N is
    begin
-      pragma Assert (Ekind (Id) = E_Abstract_State);
-      return Node9 (Id);
-   end Refined_State;
+      pragma Assert (Ekind (Id) = E_Package_Body);
+      return Node8 (Id);
+   end Refined_State_Pragma;
 
    function Register_Exception_Call (Id : E) return N is
    begin
@@ -5307,11 +5308,11 @@ package body Einfo is
       Set_Flag227 (Id, V);
    end Set_Referenced_As_Out_Parameter;
 
-   procedure Set_Refined_State (Id : E; V : E) is
+   procedure Set_Refined_State_Pragma (Id : E; V : N) is
    begin
-      pragma Assert (Ekind (Id) = E_Abstract_State);
-      Set_Node9 (Id, V);
-   end Set_Refined_State;
+      pragma Assert (Ekind (Id) = E_Package_Body);
+      Set_Node8 (Id, V);
+   end Set_Refined_State_Pragma;
 
    procedure Set_Register_Exception_Call (Id : E; V : N) is
    begin
@@ -6427,6 +6428,19 @@ package body Einfo is
       return False;
    end Has_Interrupt_Handler;
 
+   -----------------------------
+   -- Has_Null_Abstract_State --
+   -----------------------------
+
+   function Has_Null_Abstract_State (Id : E) return B is
+   begin
+      pragma Assert (Ekind_In (Id, E_Generic_Package, E_Package));
+
+      return
+        Present (Abstract_States (Id))
+          and then Is_Null_State (Node (First_Elmt (Abstract_States (Id))));
+   end Has_Null_Abstract_State;
+
    --------------------
    -- Has_Unmodified --
    --------------------
@@ -8292,6 +8306,9 @@ package body Einfo is
          when E_Procedure                                  =>
             Write_Str ("Postcondition_Proc");
 
+         when E_Package_Body                               =>
+            Write_Str ("Refined_State_Pragma");
+
          when E_Return_Statement                           =>
             Write_Str ("Return_Applies_To");
 
@@ -8313,9 +8330,6 @@ package body Einfo is
          when Object_Kind                                  =>
             Write_Str ("Current_Value");
 
-         when E_Abstract_State                             =>
-            Write_Str ("Refined_State");
-
          when E_Function                                   |
               E_Generic_Function                           |
               E_Generic_Package                            |

gcc/ada/einfo.ads

@@ -1645,6 +1645,10 @@ package Einfo is
 --       are not considered to be significant since they do not affect
 --       stored bit patterns.
 
+--    Has_Null_Abstract_State (synth)
+--       Defined in package entities. True if the package is subject to a null
+--       Abstract_State aspect/pragma.
+
 --    Has_Object_Size_Clause (Flag172)
 --       Defined in entities for types and subtypes. Set if an Object_Size
 --       clause has been processed for the type Used to prevent multiple
@@ -3533,9 +3537,9 @@ package Einfo is
 --       we have a separate warning for variables that are only assigned and
 --       never read, and out parameters are a special case.
 
---    Refined_State (Node9)
---       Defined in E_Abstract_State entities. Contains the entity of the
---       abstract state completion which is usually foung in package bodies.
+--    Refined_State_Pragma (Node8)
+--       Defined in [generic] package bodies. Contains the pragma that refines
+--       all abstract states defined in the corresponding package declaration.
 
 --    Register_Exception_Call (Node20)
 --       Defined in exception entities. When an exception is declared,
@@ -5092,7 +5096,6 @@ package Einfo is
    ------------------------------------------
 
    --  E_Abstract_State
-   --    Refined_State                       (Node9)
    --    Is_External_State                   (synth)
    --    Is_Input_Only_State                 (synth)
    --    Is_Null_State                       (synth)
@@ -5636,10 +5639,12 @@ package Einfo is
    --    Is_Visible_Lib_Unit                 (Flag116)
    --    Renamed_In_Spec                     (Flag231)  (non-generic case only)
    --    Static_Elaboration_Desired          (Flag77)   (non-generic case only)
+   --    Has_Null_Abstract_State             (synth)
    --    Is_Wrapper_Package                  (synth)    (non-generic case only)
    --    Scope_Depth                         (synth)
 
    --  E_Package_Body
+   --    Refined_State_Pragma                (Node8)
    --    Handler_Records                     (List10)   (non-generic case only)
    --    Related_Instance                    (Node15)   (non-generic case only)
    --    First_Entity                        (Node17)
@@ -6535,7 +6540,7 @@ package Einfo is
    function Referenced                          (Id : E) return B;
    function Referenced_As_LHS                   (Id : E) return B;
    function Referenced_As_Out_Parameter         (Id : E) return B;
-   function Refined_State                       (Id : E) return E;
+   function Refined_State_Pragma                (Id : E) return E;
    function Register_Exception_Call             (Id : E) return N;
    function Related_Array_Object                (Id : E) return E;
    function Related_Expression                  (Id : E) return N;
@@ -6674,6 +6679,7 @@ package Einfo is
    function Has_Attach_Handler                  (Id : E) return B;
    function Has_Entries                         (Id : E) return B;
    function Has_Foreign_Convention              (Id : E) return B;
+   function Has_Null_Abstract_State             (Id : E) return B;
    function Implementation_Base_Type            (Id : E) return E;
    function Is_Base_Type                        (Id : E) return B;
    function Is_Boolean_Type                     (Id : E) return B;
@@ -7152,7 +7158,7 @@ package Einfo is
    procedure Set_Referenced                      (Id : E; V : B := True);
    procedure Set_Referenced_As_LHS               (Id : E; V : B := True);
    procedure Set_Referenced_As_Out_Parameter     (Id : E; V : B := True);
-   procedure Set_Refined_State                   (Id : E; V : E);
+   procedure Set_Refined_State_Pragma            (Id : E; V : N);
    procedure Set_Register_Exception_Call         (Id : E; V : N);
    procedure Set_Related_Array_Object            (Id : E; V : E);
    procedure Set_Related_Expression              (Id : E; V : N);
@@ -7902,7 +7908,7 @@ package Einfo is
    pragma Inline (Referenced);
    pragma Inline (Referenced_As_LHS);
    pragma Inline (Referenced_As_Out_Parameter);
-   pragma Inline (Refined_State);
+   pragma Inline (Refined_State_Pragma);
    pragma Inline (Register_Exception_Call);
    pragma Inline (Related_Array_Object);
    pragma Inline (Related_Expression);
@@ -8318,7 +8324,7 @@ package Einfo is
    pragma Inline (Set_Referenced);
    pragma Inline (Set_Referenced_As_LHS);
    pragma Inline (Set_Referenced_As_Out_Parameter);
-   pragma Inline (Set_Refined_State);
+   pragma Inline (Set_Refined_State_Pragma);
    pragma Inline (Set_Register_Exception_Call);
    pragma Inline (Set_Related_Array_Object);
    pragma Inline (Set_Related_Expression);

gcc/ada/elists.adb

@@ -158,6 +158,34 @@ package body Elists is
       end loop;
    end Append_Unique_Elmt;
 
+   -----------
+   -- Clone --
+   ------------
+
+   function Clone (List : Elist_Id) return Elist_Id is
+      Result : Elist_Id;
+      Elmt   : Elmt_Id;
+
+   begin
+      if List = No_Elist then
+         return No_Elist;
+
+      --  Replicate the contents of the input list while preserving the
+      --  original order.
+
+      else
+         Result := New_Elmt_List;
+
+         Elmt := First_Elmt (List);
+         while Present (Elmt) loop
+            Append_Elmt (Node (Elmt), Result);
+            Next_Elmt (Elmt);
+         end loop;
+
+         return Result;
+      end if;
+   end Clone;
+
    --------------
    -- Contains --
    --------------

gcc/ada/elists.ads

@@ -153,6 +153,10 @@ package Elists is
    --  affected, but the space used by the list element may be (but is not
    --  required to be) freed for reuse in a subsequent Append_Elmt call.
 
+   function Clone (List : Elist_Id) return Elist_Id;
+   --  Create a copy of the input list. Internal list nodes are not shared and
+   --  order of elements is preserved.
+
    function Contains (List : Elist_Id; N : Node_Or_Entity_Id) return Boolean;
    --  Perform a sequential search to determine whether the given list contains
    --  a node or an entity.

gcc/ada/par-prag.adb

@@ -1254,6 +1254,7 @@ begin
            Pragma_Refined_Global                 |
            Pragma_Refined_Post                   |
            Pragma_Refined_Pre                    |
+           Pragma_Refined_State                  |
            Pragma_Relative_Deadline              |
            Pragma_Remote_Access_Type             |
            Pragma_Remote_Call_Interface          |

gcc/ada/sem_ch13.adb

@@ -1883,12 +1883,45 @@ package body Sem_Ch13 is
 
                --  Abstract_State
 
-               when Aspect_Abstract_State =>
-                  Make_Aitem_Pragma
-                    (Pragma_Argument_Associations => New_List (
-                       Make_Pragma_Argument_Association (Loc,
-                         Expression => Relocate_Node (Expr))),
-                     Pragma_Name                  => Name_Abstract_State);
+               when Aspect_Abstract_State => Abstract_State : declare
+                  Decls : List_Id;
+                  Spec  : Node_Id;
+
+               begin
+                  --  Aspect Abstract_State introduces implicit declarations
+                  --  for all state abstraction entities it defines. To emulate
+                  --  this behavior, insert the pragma at the beginning of the
+                  --  visible declarations of the related package so that it is
+                  --  analyzed immediately.
+
+                  if Nkind_In (N, N_Generic_Package_Declaration,
+                                  N_Package_Declaration)
+                  then
+                     Spec  := Specification (N);
+                     Decls := Visible_Declarations (Spec);
+
+                     Make_Aitem_Pragma
+                       (Pragma_Argument_Associations => New_List (
+                          Make_Pragma_Argument_Association (Loc,
+                            Expression => Relocate_Node (Expr))),
+                        Pragma_Name                  => Name_Abstract_State);
+                     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 Abstract_State;
 
                --  Depends
 
@@ -1967,6 +2000,42 @@ package body Sem_Ch13 is
                          Expression => Relocate_Node (Expr))),
                      Pragma_Name                  => Name_Refined_Pre);
 
+               --  Refined_State
+
+               when Aspect_Refined_State => Refined_State : declare
+                  Decls : List_Id;
+
+               begin
+                  --  The corresponding pragma for Refined_State is inserted in
+                  --  the declarations of the related package body. This action
+                  --  synchronizes both the source and from-aspect versions of
+                  --  the pragma.
+
+                  if Nkind (N) = N_Package_Body then
+                     Decls := Declarations (N);
+
+                     Make_Aitem_Pragma
+                       (Pragma_Argument_Associations => New_List (
+                          Make_Pragma_Argument_Association (Loc,
+                            Expression => Relocate_Node (Expr))),
+                        Pragma_Name                  => Name_Refined_State);
+                     Decorate_Delayed_Aspect_And_Pragma (Aspect, Aitem);
+
+                     if No (Decls) then
+                        Decls := New_List;
+                        Set_Declarations (N, Decls);
+                     end if;
+
+                     Prepend_To (Decls, Aitem);
+
+                  else
+                     Error_Msg_NE
+                       ("aspect & must apply to a package body", Aspect, Id);
+                  end if;
+
+                  goto Continue;
+               end Refined_State;
+
                --  Relative_Deadline
 
                when Aspect_Relative_Deadline =>
@@ -2411,21 +2480,6 @@ package body Sem_Ch13 is
                Set_From_Aspect_Specification (Aitem, True);
             end if;
 
-            --  Aspect Abstract_State introduces implicit declarations for all
-            --  state abstraction entities it defines. To emulate this behavior
-            --  insert the pragma at the start of the visible declarations of
-            --  the related package.
-
-            if Nam = Name_Abstract_State
-              and then Nkind (N) = N_Package_Declaration
-            then
-               if No (Visible_Declarations (Specification (N))) then
-                  Set_Visible_Declarations (Specification (N), New_List);
-               end if;
-
-               Prepend (Aitem, Visible_Declarations (Specification (N)));
-               goto Continue;
-
             --  In the context of a compilation unit, we directly put the
             --  pragma in the Pragmas_After list of the N_Compilation_Unit_Aux
             --  node (no delay is required here) except for aspects on a
@@ -2434,7 +2488,7 @@ package body Sem_Ch13 is
             --  copy (see sem_ch12), and for package instantiations, where
             --  the library unit pragmas are better handled early.
 
-            elsif Nkind (Parent (N)) = N_Compilation_Unit
+            if Nkind (Parent (N)) = N_Compilation_Unit
               and then (Present (Aitem) or else Is_Boolean_Aspect (Aspect))
             then
                declare
@@ -7651,6 +7705,7 @@ package body Sem_Ch13 is
               Aspect_Refined_Global       |
               Aspect_Refined_Post         |
               Aspect_Refined_Pre          |
+              Aspect_Refined_State        |
               Aspect_SPARK_Mode           |
               Aspect_Test_Case            =>
             raise Program_Error;

gcc/ada/sem_ch3.adb

@@ -64,6 +64,7 @@ with Sem_Dist; use Sem_Dist;
 with Sem_Elim; use Sem_Elim;
 with Sem_Eval; use Sem_Eval;
 with Sem_Mech; use Sem_Mech;
+with Sem_Prag; use Sem_Prag;
 with Sem_Res;  use Sem_Res;
 with Sem_Smem; use Sem_Smem;
 with Sem_Type; use Sem_Type;
@@ -2079,8 +2080,11 @@ package body Sem_Ch3 is
 
       --  Local variables
 
+      Body_Id     : Entity_Id;
+      Context     : Node_Id;
       Freeze_From : Entity_Id := Empty;
       Next_Decl   : Node_Id;
+      Spec_Id     : Entity_Id;
 
    --  Start of processing for Analyze_Declarations
 
@@ -2190,6 +2194,37 @@ package body Sem_Ch3 is
          Decl := Next_Decl;
       end loop;
 
+      --  Analyze the state refinements within a package body now, after all
+      --  hidden states have been encountered and freely visible. Refinements
+      --  must be processed before pragmas Refined_Depends and Refined_Global
+      --  because the last two may mention constituents.
+
+      if Present (L) then
+         Context := Parent (L);
+
+         if Nkind (Context) = N_Package_Body then
+            Body_Id := Defining_Entity (Context);
+            Spec_Id := Corresponding_Spec (Context);
+
+            --  The analysis of pragma Refined_State detects whether the spec
+            --  has abstract states available for refinement.
+
+            if Present (Refined_State_Pragma (Body_Id)) then
+               Analyze_Refined_State_In_Decl_Part
+                 (Refined_State_Pragma (Body_Id));
+
+            --  State refinement is required when the package declaration has
+            --  abstract states. Null states are not considered.
+
+            elsif Present (Abstract_States (Spec_Id))
+              and then not Has_Null_Abstract_State (Spec_Id)
+            then
+               Error_Msg_NE
+                 ("package & requires state refinement", Context, Spec_Id);
+            end if;
+         end if;
+      end if;
+
       --  Analyze the contracts of a subprogram declaration or a body now due
       --  to delayed visibility requirements of aspects.
 

gcc/ada/sem_prag.ads

@@ -77,6 +77,9 @@ package Sem_Prag is
    procedure Analyze_Refined_Global_In_Decl_Part (N : Node_Id);
    --  Perform full analysis of delayed pragma Refined_Global
 
+   procedure Analyze_Refined_State_In_Decl_Part (N : Node_Id);
+   --  Perform full analysis of delayed pragma Refined_State
+
    procedure Analyze_Test_Case_In_Decl_Part (N : Node_Id; S : Entity_Id);
    --  Perform preanalysis of pragma Test_Case that applies to a subprogram
    --  declaration. Parameter N denotes the pragma, S is the entity of the

gcc/ada/snames.ads-tmpl

@@ -584,6 +584,10 @@ package Snames is
    Name_Refined_Global                 : constant Name_Id := N + $; -- GNAT
    Name_Refined_Post                   : constant Name_Id := N + $; -- GNAT
    Name_Refined_Pre                    : constant Name_Id := N + $; -- GNAT
+
+   --  Kirchev
+
+   Name_Refined_State                  : constant Name_Id := N + $; -- GNAT
    Name_Relative_Deadline              : constant Name_Id := N + $; -- Ada 05
    Name_Remote_Access_Type             : constant Name_Id := N + $; -- GNAT
    Name_Remote_Call_Interface          : constant Name_Id := N + $;
@@ -1871,6 +1875,7 @@ package Snames is
       Pragma_Refined_Global,
       Pragma_Refined_Post,
       Pragma_Refined_Pre,
+      Pragma_Refined_State,
       Pragma_Relative_Deadline,
       Pragma_Remote_Access_Type,
       Pragma_Remote_Call_Interface,