Previously, the four aspects Async_Readers, Async_Writers, Effective_Reads, and Effective_Writes could only be specified for volatile variables and for state abstractions. Allow specifying these aspects for volatile types.
Tested on x86_64-pc-linux-gnu, committed on trunk
2020-06-11 Steve Baird <ba...@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.
patch.diff.gz
Description: application/gzip
