Volatile refinement properties (e.g. Async_Writers), which refine the
Volatile aspect in SPARK, are inherited by subtypes from their base
types. In particular, this patch fixes handling of those properties for
subtypes of private types.
gcc/ada/
* sem_util.adb (Type_Or_Variable_Has_Enabled_Property): Given a
subtype recurse into its base type.
then
return False;
- -- For a private type, may need to look at the full view
+ -- For a private type (including subtype of a private types), look at
+ -- the full view.
elsif Is_Private_Type (Item_Id) and then Present (Full_View (Item_Id))
then
return Type_Or_Variable_Has_Enabled_Property
(First_Subtype (Etype (Base_Type (Item_Id))));
+ -- For a subtype, the property will be inherited from its base type.
+
+ elsif Is_Type (Item_Id)
+ and then not Is_Base_Type (Item_Id)
+ then
+ return Type_Or_Variable_Has_Enabled_Property (Etype (Item_Id));
+
-- If not specified explicitly for an object and its type
-- is effectively volatile, then take result from the type.