[Ada] Handle correctly current instance of PO in local subprogram Global

Pierre-Marie de Rodat derodat@adacore.com
Tue Nov 24 10:17:01 GMT 2020

SPARK defines the current instance of a protected object as non-volatile
for internal calls, which allows to use it in the Global contract of a
local non-volatile function. This was not handled correctly, now fixed.

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


	* sem_prag.adb (Analyze_Global_Item): Handle specially the
	current instance of a PO.
	* sem_util.ads (Is_Effectively_Volatile,
	Is_Effectively_Volatile_For_Reading): Add parameter
	* sem_util.adb (Is_Effectively_Volatile,
	Is_Effectively_Volatile_For_Reading): Add parameter
	Ignore_Protected to compute the query results ignoring protected
	Is_Effectively_Volatile_Object_For_Reading): Adapt to new
-------------- next part --------------
A non-text attachment was scrubbed...
Name: patch.diff
Type: text/x-diff
Size: 7400 bytes
Desc: not available
URL: <https://gcc.gnu.org/pipermail/gcc-patches/attachments/20201124/4736bf98/attachment-0001.bin>

More information about the Gcc-patches mailing list