einfo.adb: Add node/list usage for Refined_State and Refinement_Constituents.

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

	* einfo.adb: Add node/list usage for Refined_State
	and Refinement_Constituents.
	(Get_Pragma): Update the
	initialization of Is_CDG to include Refined_Global and
	Refined_Depends. Rename constant Delayed to In_Contract and update
	all of its occurrences.
	(Is_Non_Volatile_State): New routine.
	(Is_Volatile_State): Removed.
	(Refined_State): New routine.
	(Refinement_Constituents): New routine.
	(Set_Refined_State): New routine.
	(Set_Refinement_Constituents): New routine.
	(Write_Field8_Name): Add output for Refinement_Constituents.
	(Write_Field10_Name): Add output for Refined_State.
	* einfo.ads: Add new synthesized attribute Is_Non_Volatile_State.
	Remove synthesized attribute Is_Volatile_State.  Add new
	attributes Refined_State and Refinement_Constituents along with
	usage in nodes.
	(Get_Pragma): Update the comment on usage.
	(Is_Non_Volatile_State): New routine.
	(Is_Volatile_State): Removed.
	(Refined_State): New routine and pragma Inline.
	(Refinement_Constituents): New routine and pragma Inline.
	(Set_Refined_State): New routine and pragma Inline.
	(Set_Refinement_Constituents): New routine and pragma Inline.
	* elists.ads, elists.adb (Clone): Removed.
	(New_Copy_Elist): New routine.
	(Remove): New routine.
	* sem_ch3.adb (Analyze_Declarations): Use Defining_Entity
	to get the entity of the subprogram [body].
	(Analyze_Object_Declaration): Add initialization for
	Refined_State.
	* sem_ch6.adb (Analyze_Subprogram_Body_Contract): Add processing
	for Refined_Global and Refined_Depends. Emit an error when
	the body requires Refined_Global, but the aspect/pragma is
	not present.
	* sem_ch6.ads (Analyze_Subprogram_Body_Contract): Change
	procedure signature and add comment on usage.
	* sem_ch13.adb (Analyze_Aspect_Specifications): Add processing
	for aspect Refined_Global.
	* sem_prag.adb (Analyze_Abstract_State): Add initialization
	of attributes Refined_State and Refinement_Constituents.
	(Analyze_Depends_In_Decl_Part, Analyze_Global_In_Decl_Part,
	Analyze_Contract_Cases_In_Decl_Part): Remove local
	constant Arg1.
	(Analyze_Pragma): Add processing for pragma
	Refined_Global. The analysis of Refined_Post and Refined_Pre
	has been merged. Update an error message in the processing of
	pragma Refined_State.
	(Analyze_Refined_Global_In_Decl_Part): Provide implementation.
	(Analyze_Refined_Pragma): New routine.
	(Analyze_Refined_Pre_Post_Condition): Removed.
	(Analyze_Refined_State_In_Decl_Part): Update the call to Clone.
	(Analyze_Refinement_Clause): Make State_Id visible to all
	nested subprogram.
	(Check_Matching_Constituent): Establish
	a relation between a refined state and its constituent.
	(Collect_Hidden_States_In_Decls): Remove ??? comment. Look at
	the entity of the object declaration to establish its kind.
	* sem_util.adb: Alphabetize with and use clauses.
	(Contains_Refined_State): New routine.
	* sem_util.ads (Contains_Refined_State): New routine.

From-SVN: r203504

1 files changed, 39 insertions, 4 deletions

diff --git a/gcc/ada/sem_ch6.adb b/gcc/ada/sem_ch6.adb
index f138aea..aee35fb 100644
--- a/gcc/ada/sem_ch6.adb
+++ b/gcc/ada/sem_ch6.adb
@@ -1975,12 +1975,47 @@ package body Sem_Ch6 is
    -- Analyze_Subprogram_Body_Contract --
    --------------------------------------
 
-   --  ??? To be implemented
+   procedure Analyze_Subprogram_Body_Contract (Body_Id : Entity_Id) is
+      Body_Decl : constant Node_Id   := Parent (Parent (Body_Id));
+      Spec_Id   : constant Entity_Id := Corresponding_Spec (Body_Decl);
+      Prag      : Node_Id;
+
+      Has_Refined_Global : Boolean := False;
 
-   procedure Analyze_Subprogram_Body_Contract (Subp : Entity_Id) is
-      pragma Unreferenced (Subp);
    begin
-      null;
+      --  When a subprogram body declaration is erroneous, its defining entity
+      --  is left unanalyzed. There is nothing left to do in this case because
+      --  the body lacks a contract.
+
+      if not Analyzed (Body_Id) then
+         return;
+      end if;
+
+      Prag := Classifications (Contract (Body_Id));
+      while Present (Prag) loop
+         if Pragma_Name (Prag) = Name_Refined_Depends then
+            Analyze_Refined_Depends_In_Decl_Part (Prag);
+
+         elsif Pragma_Name (Prag) = Name_Refined_Global then
+            Has_Refined_Global := True;
+            Analyze_Refined_Global_In_Decl_Part (Prag);
+         end if;
+
+         Prag := Next_Pragma (Prag);
+      end loop;
+
+      --  When the corresponding Global aspect/pragma references a state with
+      --  visible refinement, the body requires Refined_Global.
+
+      if not Has_Refined_Global and then Present (Spec_Id) then
+         Prag := Get_Pragma (Spec_Id, Pragma_Global);
+
+         if Present (Prag) and then Contains_Refined_State (Prag) then
+            Error_Msg_NE
+              ("body of subprogram & requires global refinement",
+               Body_Decl, Spec_Id);
+         end if;
+      end if;
    end Analyze_Subprogram_Body_Contract;
 
    ------------------------------------