[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

1 files changed, 35 insertions, 0 deletions

diff --git a/gcc/ada/sem_ch3.adb b/gcc/ada/sem_ch3.adb
index 1e6abf2..5e40656 100644
--- a/gcc/ada/sem_ch3.adb
+++ b/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.