From 4127ebece723b172aeecacbba9b523af98cc646b Mon Sep 17 00:00:00 2001 From: Steve Baird Date: Fri, 31 Jan 2020 11:36:51 -0800 Subject: [Ada] Allow specifying volatility refinement aspects for types 2020-06-11 Steve Baird 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. --- gcc/ada/contracts.ads | 17 +++++++++++++++-- 1 file changed, 15 insertions(+), 2 deletions(-) (limited to 'gcc/ada/contracts.ads') 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); -- cgit v1.1