[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.

1 files changed, 15 insertions, 2 deletions

diff --git a/gcc/ada/contracts.ads b/gcc/ada/contracts.ads
index a41285f..9e7b955 100644
--- a/gcc/ada/contracts.ads
+++ b/gcc/ada/contracts.ads
@@ -33,8 +33,8 @@ package Contracts is
    procedure Add_Contract_Item (Prag : Node_Id; Id : Entity_Id);
    --  Add pragma Prag to the contract of a constant, entry, entry family,
    --  [generic] package, package body, protected unit, [generic] subprogram,
-   --  subprogram body, variable or task unit denoted by Id. The following are
-   --  valid pragmas:
+   --  subprogram body, variable, task unit, or type denoted by Id.
+   --  The following are valid pragmas:
    --
    --    Abstract_State
    --    Async_Readers
@@ -114,6 +114,19 @@ package Contracts is
    --  Freeze_Id is the entity of a [generic] package body or a [generic]
    --  subprogram body which "freezes" the contract of Obj_Id.
 
+   procedure Analyze_Type_Contract (Type_Id : Entity_Id);
+   --  Analyze all delayed pragmas chained on the contract of object Obj_Id as
+   --  if they appeared at the end of the declarative region. The pragmas to be
+   --  considered are:
+   --
+   --    Async_Readers
+   --    Async_Writers
+   --    Effective_Reads
+   --    Effective_Writes
+   --
+   --  In the case of a protected or task type, there will also be
+   --  a call to Analyze_Protected_Contract or Analyze_Task_Contract.
+
    procedure Analyze_Package_Body_Contract
      (Body_Id   : Entity_Id;
       Freeze_Id : Entity_Id := Empty);