sem_ch6.adb (Analyze_Subprogram_Body_Contract): Do not enforce global and…

sem_ch6.adb (Analyze_Subprogram_Body_Contract): Do not enforce global and dependence refinement when SPARK_Mode is off.

2014-02-24  Hristian Kirtchev  <kirtchev@adacore.com>

	* sem_ch6.adb (Analyze_Subprogram_Body_Contract): Do not enforce
	global and dependence refinement when SPARK_Mode is off.
	* sem_ch7.adb (Analyze_Package_Body_Contract): Do not enforce
	state refinement when SPARK_Mode is off.
	* sem_ch13.adb (Analyze_Aspect_Specifications): Add local
	variable Decl. Insert the generated pragma for Refined_State
	after a potential pragma SPARK_Mode.
	* sem_prag.adb (Analyze_Depends_In_Decl_Part): Add local
	constant Deps. Remove local variable Expr. Check the syntax
	of pragma Depends when SPARK_Mode is off. Factor out the
	processing for extra parenthesis around individual clauses.
	(Analyze_Global_In_Decl_List): Items is now a constant. Check
	the syntax of pragma Global when SPARK_Mode is off.
	(Analyze_Initializes_In_Decl_Part): Check the syntax of pragma
	Initializes when SPARK_Mode is off.
	(Analyze_Part_Of): Check
	the syntax of the encapsulating state when SPARK_Mode is off.
	(Analyze_Pragma): Check the syntax of pragma Abstract_State when
	SPARK_Mode is off. Move the declaration order check with respect
	to pragma Initializes to the end of the processing. Do not verify
	the declaration order for pragma Initial_Condition when SPARK_Mode
	is off. Do not complain about a useless package refinement when
	SPARK_Mode is off.
	(Analyze_Refined_Depends_In_Decl_Part): Refs
	is now a constant. Check the syntax of pragma Refined_Depends
	when SPARK_Mode is off.
	(Analyze_Refined_Global_In_Decl_Part):
	Check the syntax of pragma Refined_Global when SPARK_Mode is off.
	(Analyze_Refined_State_In_Decl_Part): Check the syntax of pragma
	Refined_State when SPARK_Mode is off.
	(Check_Dependence_List_Syntax): New routine.
	(Check_Global_List_Syntax): New routine.
	(Check_Initialization_List_Syntax): New routine.
	(Check_Item_Syntax): New routine.
	(Check_State_Declaration_Syntax): New routine.
	(Check_Refinement_List_Syntax): New routine.
	(Has_Extra_Parentheses): Moved to the top level of Sem_Prag.

From-SVN: r208087

gcc/ada/ChangeLog

+2014-02-24  Hristian Kirtchev  <kirtchev@adacore.com>
+
+	* sem_ch6.adb (Analyze_Subprogram_Body_Contract): Do not enforce
+	global and dependence refinement when SPARK_Mode is off.
+	* sem_ch7.adb (Analyze_Package_Body_Contract): Do not enforce
+	state refinement when SPARK_Mode is off.
+	* sem_ch13.adb (Analyze_Aspect_Specifications): Add local
+	variable Decl. Insert the generated pragma for Refined_State
+	after a potential pragma SPARK_Mode.
+	* sem_prag.adb (Analyze_Depends_In_Decl_Part): Add local
+	constant Deps. Remove local variable Expr. Check the syntax
+	of pragma Depends when SPARK_Mode is off. Factor out the
+	processing for extra parenthesis around individual clauses.
+	(Analyze_Global_In_Decl_List): Items is now a constant. Check
+	the syntax of pragma Global when SPARK_Mode is off.
+	(Analyze_Initializes_In_Decl_Part): Check the syntax of pragma
+	Initializes when SPARK_Mode is off.
+	(Analyze_Part_Of): Check
+	the syntax of the encapsulating state when SPARK_Mode is off.
+	(Analyze_Pragma): Check the syntax of pragma Abstract_State when
+	SPARK_Mode is off. Move the declaration order check with respect
+	to pragma Initializes to the end of the processing. Do not verify
+	the declaration order for pragma Initial_Condition when SPARK_Mode
+	is off. Do not complain about a useless package refinement when
+	SPARK_Mode is off.
+	(Analyze_Refined_Depends_In_Decl_Part): Refs
+	is now a constant. Check the syntax of pragma Refined_Depends
+	when SPARK_Mode is off.
+	(Analyze_Refined_Global_In_Decl_Part):
+	Check the syntax of pragma Refined_Global when SPARK_Mode is off.
+	(Analyze_Refined_State_In_Decl_Part): Check the syntax of pragma
+	Refined_State when SPARK_Mode is off.
+	(Check_Dependence_List_Syntax): New routine.
+	(Check_Global_List_Syntax): New routine.
+	(Check_Initialization_List_Syntax): New routine.
+	(Check_Item_Syntax): New routine.
+	(Check_State_Declaration_Syntax): New routine.
+	(Check_Refinement_List_Syntax): New routine.
+	(Has_Extra_Parentheses): Moved to the top level of Sem_Prag.
+
 2014-02-24  Robert Dewar  <dewar@adacore.com>
 
 	* a-tags.adb, s-os_lib.adb: Minor reformatting.

gcc/ada/sem_ch13.adb

@@ -2343,6 +2343,7 @@ package body Sem_Ch13 is
                --  Refined_State
 
                when Aspect_Refined_State => Refined_State : declare
+                  Decl  : Node_Id;
                   Decls : List_Id;
 
                begin
@@ -2352,8 +2353,6 @@ package body Sem_Ch13 is
                   --  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,
@@ -2361,12 +2360,31 @@ package body Sem_Ch13 is
                         Pragma_Name                  => Name_Refined_State);
                      Decorate_Aspect_And_Pragma (Aspect, Aitem);
 
-                     if No (Decls) then
-                        Decls := New_List;
-                        Set_Declarations (N, Decls);
-                     end if;
+                     Decls := Declarations (N);
 
-                     Prepend_To (Decls, Aitem);
+                     --  When the package body is subject to pragma SPARK_Mode,
+                     --  insert pragma Refined_State after SPARK_Mode.
+
+                     if Present (Decls) then
+                        Decl := First (Decls);
+
+                        if Nkind (Decl) = N_Pragma
+                          and then Pragma_Name (Decl) = Name_SPARK_Mode
+                        then
+                           Insert_After (Decl, Aitem);
+
+                        --  The related package body lacks SPARK_Mode, the
+                        --  corresponding pragma must be the first declaration.
+
+                        else
+                           Prepend_To (Decls, Aitem);
+                        end if;
+
+                     --  Otherwise the pragma forms a new declarative list
+
+                     else
+                        Set_Declarations (N, New_List (Aitem));
+                     end if;
 
                   else
                      Error_Msg_NE

gcc/ada/sem_ch6.adb

@@ -2062,12 +2062,16 @@ package body Sem_Ch6 is
          Analyze_Refined_Global_In_Decl_Part (Ref_Global);
 
       --  When the corresponding Global aspect/pragma references a state with
-      --  visible refinement, the body requires Refined_Global.
+      --  visible refinement, the body requires Refined_Global. Refinement is
+      --  not required when SPARK checks are suppressed.
 
       elsif Present (Spec_Id) then
          Prag := Get_Pragma (Spec_Id, Pragma_Global);
 
-         if Present (Prag) and then Contains_Refined_State (Prag) then
+         if SPARK_Mode /= Off
+           and then Present (Prag)
+           and then Contains_Refined_State (Prag)
+         then
             Error_Msg_NE
               ("body of subprogram & requires global refinement",
                Body_Decl, Spec_Id);
@@ -2081,12 +2085,16 @@ package body Sem_Ch6 is
          Analyze_Refined_Depends_In_Decl_Part (Ref_Depends);
 
       --  When the corresponding Depends aspect/pragma references a state with
-      --  visible refinement, the body requires Refined_Depends.
+      --  visible refinement, the body requires Refined_Depends. Refinement is
+      --  not required when SPARK checks are suppressed.
 
       elsif Present (Spec_Id) then
          Prag := Get_Pragma (Spec_Id, Pragma_Depends);
 
-         if Present (Prag) and then Contains_Refined_State (Prag) then
+         if SPARK_Mode /= Off
+           and then Present (Prag)
+           and then Contains_Refined_State (Prag)
+         then
             Error_Msg_NE
               ("body of subprogram & requires dependance refinement",
                Body_Decl, Spec_Id);

gcc/ada/sem_ch7.adb

@@ -191,10 +191,13 @@ package body Sem_Ch7 is
       if Present (Prag) then
          Analyze_Refined_State_In_Decl_Part (Prag);
 
-      --  State refinement is required when the package declaration has
-      --  abstract states. Null states are not considered.
+      --  State refinement is required when the package declaration defines at
+      --  least one abstract state. Null states are not considered. Refinement
+      --  is not envorced when SPARK checks are turned off.
 
-      elsif Requires_State_Refinement (Spec_Id, Body_Id) then
+      elsif SPARK_Mode /= Off
+        and then Requires_State_Refinement (Spec_Id, Body_Id)
+      then
          Error_Msg_N ("package & requires state refinement", Spec_Id);
       end if;
    end Analyze_Package_Body_Contract;