ada: Remove SPARK legality checks

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.