[Ada] Allow specifying volatility refinement aspects for types

[Ada] Allow specifying volatility refinement aspects for types

2020-06-11  Steve Baird  <baird@adacore.com>

gcc/ada/

	* contracts.adb (Add_Contract_Item): Support specifying
	volatility refinement aspects for types.
	(Analyze_Contracts): Add call to Analyze_Type_Contract in the
	case of a contract for a type.
	(Freeze_Contracts): Add call to Analyze_Type_Contract in the
	case of a contract for a type.
	(Check_Type_Or_Object_External_Properties): A new procedure
	which performs the work that needs to be done for both object
	declarations and types.
	(Analyze_Object_Contract): Add a call to
	Check_Type_Or_Object_External_Properties and remove the code in
	this procedure which did much of the work that is now performed
	by that call.
	(Analyze_Type_Contract): Implement this new routine as nothing
	more than a call to Check_Type_Or_Object_External_Properties.
	* contracts.ads: Update comment for Add_Contract_To_Item because
	types can have contracts.  Follow (questionable) precedent and
	declare new routine Analyze_Type_Contract as visible (following
	example of Analyze_Object_Contract), despite the fact that it is
	never called from outside of the package where it is declared.
	* einfo.adb (Contract, Set_Contract): Id argument can be a type;
	support this case.
	(Write_Field34_Name): Field name is "contract" for a type.
	* einfo.ads: Update comment describing Contract attribute.
	* sem_ch3.adb (Build_Derived_Numeric_Type): Is_Volatile should
	return same answer for all subtypes of a given type. Thus, when
	building the base type for something like type Volatile_1_To_10
	is range 1 .. 10 with Volatile; that basetype should be marked
	as being volatile.
	(Access_Type_Declaration): Add SPARK-specific legality check
	that the designated type of an access type shall be compatible
	with respect to volatility with the access type.
	* sem_ch12.adb (Check_Shared_Variable_Control_Aspects): Add
	SPARK-specific legality check that an actual type parameter in
	an instantiation shall be compatible with respect to volatility
	with the corresponding formal type.
	* sem_ch13.adb (Analyze_Aspect_Specifications): Perform checks
	for aspect specs for the 4 volatility refinement aspects that
	were already being performed for all language-defined aspects.
	* sem_prag.adb (Analyze_External_Property_In_Decl_Part,
	Analyze_Pragma): External properties (other than No_Caching) may
	be specified for a type, including a generic formal type.
	* sem_util.ads: Declare new subprograms - Async_Readers_Enabled,
	Async_Writers_Enabled, Effective_Reads, Effective_Writes, and
	Check_Volatility_Compatibility.
	* sem_util.adb (Async_Readers_Enabled, Async_Writers_Enabled,
	Effective_Reads, Effective_Writes): Initial implementation of
	new functions for querying aspect values.
	(Check_Volatility_Compatibility): New procedure intended for use
	in checking all SPARK legality rules of the form "<> shall be
	compatible with respect to volatility with <>".
	(Has_Enabled_Property): Update comment because Item_Id can be a
	type.  Change name of nested Variable_Has_Enabled_Property
	function to Type_Or_Variable_Has_Enabled_Property; add a
	parameter to that function because recursion may be needed,
	e.g., in the case of a derived typ).  Cope with the case where
	the argument to Has_Enabled_Property is a type.