[Ada] Adapt SPARK RM rule on non-effectively volatile abstract state

[Pierre-Marie de Rodat]

SPARK RM 7.1.3(8) has been updated to reflect the fact that abstract
states which do have Async_Writers or Effective_Reads cannot have as
constituents objects which are effectively volatile for reading,
hence need not require that a function reading such an abstract state
be marked as a volatile function.

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

gcc/ada/

	* sem_prag.adb (Analyze_Global_Item): Adapt to update SPARK RM
	rule.
-------------- next part --------------
A non-text attachment was scrubbed...
Name: patch.diff
Type: text/x-diff
Size: 990 bytes
Desc: not available
URL: <https://gcc.gnu.org/pipermail/gcc-patches/attachments/20210705/edff5d42/attachment-0001.bin>