ada: Allow No_Caching on volatile types

ada: Allow No_Caching on volatile types

SPARK RM now allow the property No_Caching on volatile types, to
indicate that they should be considered volatile for compilation, but
not by GNATprove's analysis.

gcc/ada/

	* contracts.adb (Add_Contract_Item): Allow No_Caching on types.
	(Check_Type_Or_Object_External_Properties): Check No_Caching.
	Check that non-effectively volatile types does not contain an
	effectively volatile component (instead of just a volatile
	component).
	(Analyze_Object_Contract): Remove shared checking of No_Caching.
	* sem_prag.adb (Analyze_External_Property_In_Decl_Part): Adapt checking
	of No_Caching for types.
	(Analyze_Pragma): Allow No_Caching on types.
	* sem_util.adb (Has_Effectively_Volatile_Component): New query function.
	(Is_Effectively_Volatile): Type with Volatile and No_Caching is not
	effectively volatile.
	(No_Caching_Enabled): Remove assertion to apply to all entities.
	* sem_util.ads: Same.