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.
Tested on x86_64-pc-linux-gnu, committed on trunk
gcc/ada/
* sem_util.adb (Type_Or_Variable_Has_Enabled_Property): Given a
subtype recurse into its base type.diff --git a/gcc/ada/sem_util.adb b/gcc/ada/sem_util.adb
--- a/gcc/ada/sem_util.adb
+++ b/gcc/ada/sem_util.adb
@@ -12683,7 +12683,8 @@ package body Sem_Util is
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
@@ -12696,6 +12697,13 @@ package body Sem_Util is
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.
