[Ada] SPARK property "effectively volatile" and its effects

[Arnaud Charlet <charlet at adacore dot com>]

This patch implements SPARK property "effectively volatile" which states:

   In SPARK 2014, the terms volatile type and volatile object are defined as
   per Ada RM C.6(8/3). An effectively volatile type is a volatile type or an
   array type to which the Volatile_Components aspect has been applied. An
   effectively volatile object is a volatile object or an object of an array
   type to which Volatile_Components has been applied.

------------
-- Source --
------------

--  volatile_comps.ads

package Volatile_Comps with SPARK_Mode is
   type I is range 1 .. 10;

   type VC_Array  is array (I) of Integer with Volatile_Components;
   type NVC_Array is array (I) of Integer;

   Obj_1 : VC_Array  with Async_Readers;
   Obj_2 : VC_Array  with Async_Readers, Effective_Reads;
   Obj_3 : NVC_Array with Volatile, Async_Readers;
   Obj_4 : NVC_Array with Volatile, Async_Readers, Effective_Reads;
end Volatile_Comps;

----------------------------
-- Compilation and output --
----------------------------

$ gcc -c volatile_comps.ads
volatile_comps.ads:8:04: illegal combination of external properties (SPARK RM
  7.1.2(6))
volatile_comps.ads:10:04: illegal combination of external properties (SPARK RM
  7.1.2(6))

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

2014-07-31  Hristian Kirtchev  <kirtchev@adacore.com>

	* freeze.adb (Freeze_Record_Type): Replace all calls to
	Is_SPARK_Volatile with Is_Effectively_Volatile and update
	related comments.
	* sem_ch3.adb (Analyze_Object_Contract, Process_Discriminants):
	Replace all calls to Is_SPARK_Volatile with
	Is_Effectively_Volatile and update related comments.
	* sem_ch5.adb (Analyze_Iterator_Specification,
	Analyze_Loop_Parameter_Specification): Replace all calls to
	Is_SPARK_Volatile with Is_Effectively_Volatile and update
	related comments.
	* sem_ch6.adb (Process_Formals): Replace all calls to
	Is_SPARK_Volatile with Is_Effectively_Volatile and update
	related comments.
	* sem_ch12.adb (Instantiate_Object): Replace the call to
	Is_SPARK_Volatile_Object with Is_Effectively_Volatile_Object
	and update related comment.
	* sem_prag.adb (Analyze_External_Property_In_Decl_Part,
	Analyze_Global_Item): Replace all calls to Is_SPARK_Volatile
	with Is_Effectively_Volatile and update related comments.
	* sem_res.adb (Resolve_Actuals, Resolve_Entity_Name): Replace
	all calls to Is_SPARK_Volatile with Is_Effectively_Volatile and
	update related comments.
	* sem_util.adb (Has_Enabled_Property,
	Variable_Has_Enabled_Property): Replace all calls
	to Is_SPARK_Volatile with Is_Effectively_Volatile and
	update related comments.
	(Is_Effectively_Volatile): New routine.
	(Is_Effectively_Volatile_Object): New routine.
	(Is_SPARK_Volatile): Removed.
	(Is_SPARK_Volatile_Object): Removed.
	* sem_util.ads (Is_Effectively_Volatile): New routine.
	(Is_Effectively_Volatile_Object): New routine.
	(Is_SPARK_Volatile): Removed.
	(Is_SPARK_Volatile_Object): Removed.

Attachment: difs
Description: Text document