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

[Pierre-Marie de Rodat]

SPARK Reference Manual has been updated to allow the use of volatile
types and objects without Async_Writers or Effective_Reads in more
places, as these references are not considered as external effects.

Tested on x86_64-pc-linux-gnu, committed on trunk

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.
-------------- next part --------------
A non-text attachment was scrubbed...
Name: patch.diff
Type: text/x-diff
Size: 15982 bytes
Desc: not available
URL: <https://gcc.gnu.org/pipermail/gcc-patches/attachments/20201016/75211c29/attachment-0001.bin>