[Ada] SPARK: update for effectively volatile types and objects

[Ada] SPARK: update for effectively volatile types and objects

gcc/ada/

	* sem_prag.adb (Analyze_Global_In_Decl_Part): Update check to
	reject volatile object for reading.
	* sem_res.adb (Resolve_Actuals, Resolve_Entity_Name): Update
	check to reject volatile object for reading.
	* sem_util.adb, sem_util.ads
	(Check_Nonvolatile_Function_Profile,
	Has_Effectively_Volatile_Profile): Detect use of volatile object
	for reading.
	(Has_Enabled_Property): Accept constants as well.
	(Is_Effectively_Volatile_For_Reading): New function based on
	existing Is_Effectively_Volatile.
	(Is_Effectively_Volatile_Object_For_Reading): Adapted from the
	existing Is_Effectively_Volatile_Object, using a shared
	implementation in Is_Effectively_Volatile_Object_Shared.