ada: Remove SPARK legality checks

SPARK legality checks apply only to code with SPARK_Mode On, and are
performed again in GNATprove for detecting SPARK-compatible declarations
in code with SPARK_Mode Auto. Remove this duplication, to only perform
SPARK legality checking in GNATprove. After this patch, only a few
special SPARK legality checks are performed in the frontend, which could
be moved to GNATprove later.

gcc/ada/

	* contracts.adb (Analyze_Entry_Or_Subprogram_Body_Contract):
	Remove checking on volatility. Remove handling of SPARK_Mode, not
	needed anymore.
	(Analyze_Entry_Or_Subprogram_Contract): Remove checking on
	volatility.
	(Check_Type_Or_Object_External_Properties): Same.
	(Analyze_Object_Contract): Same.
	* freeze.adb (Freeze_Record_Type): Same. Also remove checking on
	synchronized types and ghost types.
	* sem_ch12.adb (Instantiate_Object): Remove checking on
	volatility.
	(Instantiate_Type): Same.
	* sem_ch3.adb (Access_Type_Declaration): Same.
	(Derived_Type_Declaration): Remove checking related to untagged
	partial view.
	(Process_Discriminants): Remove checking on volatility.
	* sem_ch5.adb (Analyze_Loop_Parameter_Specification): Same.
	* sem_ch6.adb (Analyze_Procedure_Call): Fix use of SPARK_Mode
	where GNATprove_Mode was intended.
	* sem_disp.adb (Inherited_Subprograms): Protect against Empty
	node.
	* sem_prag.adb (Analyze_Global_In_Decl_Part): Remove checking on
	volatility.
	(Analyze_Pragma): Same.
	* sem_res.adb (Flag_Effectively_Volatile_Objects): Remove.
	(Resolve_Actuals): Remove checking on volatility.
	(Resolve_Entity_Name): Same.
	* sem_util.adb (Check_Nonvolatile_Function_Profile): Remove.
	(Check_Volatility_Compatibility): Remove.
	* sem_util.ads: Same.

1 files changed, 1 insertions, 18 deletions

diff --git a/gcc/ada/sem_util.ads b/gcc/ada/sem_util.ads
index 2fae35b6bc4..081217a455a 100644
--- a/gcc/ada/sem_util.ads
+++ b/gcc/ada/sem_util.ads
@@ -415,10 +415,6 @@ package Sem_Util is
    --  In the error case, error message is associate with Inheritor;
    --  Inheritor parameter is otherwise unused.
 
-   procedure Check_Nonvolatile_Function_Profile (Func_Id : Entity_Id);
-   --  Verify that the profile of nonvolatile function Func_Id does not contain
-   --  effectively volatile parameters or return type for reading.
-
    function Check_Parents (N : Node_Id; List : Elist_Id) return Boolean;
    --  Return True if all the occurrences of subtree N referencing entities in
    --  the given List have the right value in their Parent field.
@@ -467,19 +463,6 @@ package Sem_Util is
    --  and the context is external to the protected operation, to warn against
    --  a possible unlocked access to data.
 
-   procedure Check_Volatility_Compatibility
-     (Id1, Id2                     : Entity_Id;
-      Description_1, Description_2 : String;
-      Srcpos_Bearer                : Node_Id);
-   --  Id1 and Id2 should each be the entity of a state abstraction, a
-   --  variable, or a type (i.e., something suitable for passing to
-   --  Async_Readers_Enabled and similar functions).
-   --  Does nothing if SPARK_Mode /= On. Otherwise, flags a legality violation
-   --  if one or more of the four volatility-related aspects is False for Id1
-   --  and True for Id2. The two descriptions are included in the error message
-   --  text; the source position for the generated message is determined by
-   --  Srcpos_Bearer.
-
    function Choice_List (N : Node_Id) return List_Id;
    --  Utility to retrieve the choices of a Component_Association or the
    --  Discrete_Choices of an Iterated_Component_Association. For various
@@ -2199,7 +2182,7 @@ package Sem_Util is
       Obj_Ref       : Node_Id;
       Check_Actuals : Boolean) return Boolean;
    --  Determine whether node Context denotes a "non-interfering context" (as
-   --  defined in SPARK RM 7.1.3(10)) where volatile reference Obj_Ref can
+   --  defined in SPARK RM 7.1.3(9)) where volatile reference Obj_Ref can
    --  safely reside. When examining references that might be located within
    --  actual parameters of a subprogram call that has not been resolved yet,
    --  Check_Actuals should be False; such references will be assumed to be