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

10 files changed, 647 insertions, 184 deletions

diff --git a/gcc/ada/contracts.adb b/gcc/ada/contracts.adb
index 79078df..42f36d5 100644
--- a/gcc/ada/contracts.adb
+++ b/gcc/ada/contracts.adb
@@ -61,6 +61,11 @@ package body Contracts is
    --
    --    Part_Of
 
+   procedure Check_Type_Or_Object_External_Properties
+     (Type_Or_Obj_Id : Entity_Id);
+   --  Perform checking of external properties pragmas that is common to both
+   --  type declarations and object declarations.
+
    procedure Expand_Subprogram_Contract (Body_Id : Entity_Id);
    --  Expand the contracts of a subprogram body and its correspoding spec (if
    --  any). This routine processes all [refined] pre- and postconditions as
@@ -244,18 +249,33 @@ package body Contracts is
             raise Program_Error;
          end if;
 
-      --  Protected units, the applicable pragmas are:
-      --    Part_Of
-
-      elsif Ekind (Id) = E_Protected_Type then
-         if Prag_Nam = Name_Part_Of then
-            Add_Classification;
+      --  The four volatility refinement pragmas are ok for all types.
+      --  Part_Of is ok for task types and protected types.
+      --  Depends and Global are ok for task types.
+
+      elsif Is_Type (Id) then
+         declare
+            Is_OK : constant Boolean :=
+              Nam_In (Prag_Nam, Name_Async_Readers,
+                                Name_Async_Writers,
+                                Name_Effective_Reads,
+                                Name_Effective_Writes)
+              or else (Ekind (Id) = E_Task_Type
+                         and Nam_In (Prag_Nam, Name_Part_Of,
+                                               Name_Depends,
+                                               Name_Global))
+              or else (Ekind (Id) = E_Protected_Type
+                         and Prag_Nam = Name_Part_Of);
+         begin
+            if Is_OK then
+               Add_Classification;
+            else
 
-         --  The pragma is not a proper contract item
+               --  The pragma is not a proper contract item
 
-         else
-            raise Program_Error;
-         end if;
+               raise Program_Error;
+            end if;
+         end;
 
       --  Subprogram bodies, the applicable pragmas are:
       --    Postcondition
@@ -299,16 +319,6 @@ package body Contracts is
       --    Global
       --    Part_Of
 
-      elsif Ekind (Id) = E_Task_Type then
-         if Nam_In (Prag_Nam, Name_Depends, Name_Global, Name_Part_Of) then
-            Add_Classification;
-
-         --  The pragma is not a proper contract item
-
-         else
-            raise Program_Error;
-         end if;
-
       --  Variables, the applicable pragmas are:
       --    Async_Readers
       --    Async_Writers
@@ -338,6 +348,9 @@ package body Contracts is
          else
             raise Program_Error;
          end if;
+
+      else
+         raise Program_Error;
       end if;
    end Add_Contract_Item;
 
@@ -430,6 +443,15 @@ package body Contracts is
             end;
          end if;
 
+         if Nkind_In (Decl, N_Full_Type_Declaration,
+                            N_Private_Type_Declaration,
+                            N_Task_Type_Declaration,
+                            N_Protected_Type_Declaration,
+                            N_Formal_Type_Declaration)
+         then
+            Analyze_Type_Contract (Defining_Identifier (Decl));
+         end if;
+
          Next (Decl);
       end loop;
    end Analyze_Contracts;
@@ -720,6 +742,233 @@ package body Contracts is
       end if;
    end Analyze_Entry_Or_Subprogram_Contract;
 
+   ----------------------------------------------
+   -- Check_Type_Or_Object_External_Properties --
+   ----------------------------------------------
+
+   procedure Check_Type_Or_Object_External_Properties
+     (Type_Or_Obj_Id : Entity_Id)
+   is
+      function Decl_Kind (Is_Type     : Boolean;
+                          Object_Kind : String) return String;
+      --  Returns "type" or Object_Kind, depending on Is_Type
+
+      ---------------
+      -- Decl_Kind --
+      ---------------
+
+      function Decl_Kind (Is_Type     : Boolean;
+                          Object_Kind : String) return String is
+      begin
+         if Is_Type then
+            return "type";
+         else
+            return Object_Kind;
+         end if;
+      end Decl_Kind;
+
+      Is_Type_Id : constant Boolean := Is_Type (Type_Or_Obj_Id);
+
+      --  Local variables
+
+      AR_Val       : Boolean := False;
+      AW_Val       : Boolean := False;
+      ER_Val       : Boolean := False;
+      EW_Val       : Boolean := False;
+      Seen         : Boolean := False;
+      Prag         : Node_Id;
+      Obj_Typ      : Entity_Id;
+
+   --  Start of processing for Check_Type_Or_Object_External_Properties
+
+   begin
+      --  Analyze all external properties
+
+      if Is_Type_Id then
+         Obj_Typ := Type_Or_Obj_Id;
+
+         --  If the parent type of a derived type is volatile
+         --  then the derived type inherits volatility-related flags.
+
+         if Is_Derived_Type (Type_Or_Obj_Id) then
+            declare
+               Parent_Type : constant Entity_Id :=
+                 Etype (Base_Type (Type_Or_Obj_Id));
+            begin
+               if Is_Effectively_Volatile (Parent_Type) then
+                  AR_Val := Async_Readers_Enabled (Parent_Type);
+                  AW_Val := Async_Writers_Enabled (Parent_Type);
+                  ER_Val := Effective_Reads_Enabled (Parent_Type);
+                  EW_Val := Effective_Writes_Enabled (Parent_Type);
+               end if;
+            end;
+         end if;
+      else
+         Obj_Typ := Etype (Type_Or_Obj_Id);
+      end if;
+
+      Prag := Get_Pragma (Type_Or_Obj_Id, Pragma_Async_Readers);
+
+      if Present (Prag) then
+         declare
+            Saved_AR_Val : constant Boolean := AR_Val;
+         begin
+            Analyze_External_Property_In_Decl_Part (Prag, AR_Val);
+            Seen := True;
+            if Saved_AR_Val and not AR_Val then
+               Error_Msg_N
+                 ("illegal non-confirming Async_Readers specification",
+                  Prag);
+            end if;
+         end;
+      end if;
+
+      Prag := Get_Pragma (Type_Or_Obj_Id, Pragma_Async_Writers);
+
+      if Present (Prag) then
+         declare
+            Saved_AW_Val : constant Boolean := AW_Val;
+         begin
+            Analyze_External_Property_In_Decl_Part (Prag, AW_Val);
+            Seen := True;
+            if Saved_AW_Val and not AW_Val then
+               Error_Msg_N
+                 ("illegal non-confirming Async_Writers specification",
+                  Prag);
+            end if;
+         end;
+      end if;
+
+      Prag := Get_Pragma (Type_Or_Obj_Id, Pragma_Effective_Reads);
+
+      if Present (Prag) then
+         declare
+            Saved_ER_Val : constant Boolean := ER_Val;
+         begin
+            Analyze_External_Property_In_Decl_Part (Prag, ER_Val);
+            Seen := True;
+            if Saved_ER_Val and not ER_Val then
+               Error_Msg_N
+                 ("illegal non-confirming Effective_Reads specification",
+                  Prag);
+            end if;
+         end;
+      end if;
+
+      Prag := Get_Pragma (Type_Or_Obj_Id, Pragma_Effective_Writes);
+
+      if Present (Prag) then
+         declare
+            Saved_EW_Val : constant Boolean := EW_Val;
+         begin
+            Analyze_External_Property_In_Decl_Part (Prag, EW_Val);
+            Seen := True;
+            if Saved_EW_Val and not EW_Val then
+               Error_Msg_N
+                 ("illegal non-confirming Effective_Writes specification",
+                  Prag);
+            end if;
+         end;
+      end if;
+
+      --  Verify the mutual interaction of the various external properties
+
+      if Seen then
+         Check_External_Properties
+           (Type_Or_Obj_Id, AR_Val, AW_Val, ER_Val, EW_Val);
+      end if;
+
+      --  The following checks are relevant only when SPARK_Mode is on, as
+      --  they are not standard Ada legality rules. Internally generated
+      --  temporaries are ignored.
+
+      if SPARK_Mode = On and then Comes_From_Source (Type_Or_Obj_Id) then
+         if Is_Effectively_Volatile (Type_Or_Obj_Id) then
+
+            --  The declaration of an effectively volatile object or type must
+            --  appear at the library level (SPARK RM 7.1.3(3), C.6(6)).
+
+            if not Is_Library_Level_Entity (Type_Or_Obj_Id) then
+               Error_Msg_N
+                 ("effectively volatile "
+                    & Decl_Kind (Is_Type     => Is_Type_Id,
+                                 Object_Kind => "variable")
+                    & " & must be declared at library level "
+                    & "(SPARK RM 7.1.3(3))", Type_Or_Obj_Id);
+
+            --  An object of a discriminated type cannot be effectively
+            --  volatile except for protected objects (SPARK RM 7.1.3(5)).
+
+            elsif Has_Discriminants (Obj_Typ)
+              and then not Is_Protected_Type (Obj_Typ)
+            then
+               Error_Msg_N
+                ("discriminated "
+                   & Decl_Kind (Is_Type     => Is_Type_Id,
+                                Object_Kind => "object")
+                   & " & cannot be volatile",
+                 Type_Or_Obj_Id);
+            end if;
+
+            --  An object decl shall be compatible with respect to volatility
+            --  with its type (SPARK RM 7.1.3(2)).
+
+            if not Is_Type_Id then
+               if Is_Effectively_Volatile  (Obj_Typ) then
+                  Check_Volatility_Compatibility
+                    (Type_Or_Obj_Id, Obj_Typ,
+                     "volatile object", "its type",
+                     Srcpos_Bearer => Type_Or_Obj_Id);
+               end if;
+
+            --  A component of a composite type (in this case, the composite
+            --  type is an array type) shall be compatible with respect to
+            --  volatility with the composite type (SPARK RM 7.1.3(6)).
+
+            elsif Is_Array_Type (Obj_Typ) then
+               Check_Volatility_Compatibility
+                 (Component_Type (Obj_Typ), Obj_Typ,
+                  "component type", "its enclosing array type",
+                  Srcpos_Bearer => Obj_Typ);
+
+            --  A component of a composite type (in this case, the composite
+            --  type is a record type) shall be compatible with respect to
+            --  volatility with the composite type (SPARK RM 7.1.3(6)).
+
+            elsif Is_Record_Type (Obj_Typ) then
+               declare
+                  Comp : Entity_Id := First_Component (Obj_Typ);
+               begin
+                  while Present (Comp) loop
+                     Check_Volatility_Compatibility
+                       (Etype (Comp), Obj_Typ,
+                        "record component " & Get_Name_String (Chars (Comp)),
+                        "its enclosing record type",
+                        Srcpos_Bearer => Comp);
+                     Next_Component (Comp);
+                  end loop;
+               end;
+            end if;
+
+         --  The type or object is not effectively volatile
+
+         else
+            --  A non-effectively volatile type cannot have effectively
+            --  volatile components (SPARK RM 7.1.3(6)).
+
+            if Is_Type_Id
+              and then not Is_Effectively_Volatile (Type_Or_Obj_Id)
+              and then Has_Volatile_Component (Type_Or_Obj_Id)
+            then
+               Error_Msg_N
+                 ("non-volatile type & cannot have volatile"
+                    & " components",
+                  Type_Or_Obj_Id);
+            end if;
+         end if;
+      end if;
+   end Check_Type_Or_Object_External_Properties;
+
    -----------------------------
    -- Analyze_Object_Contract --
    -----------------------------
@@ -738,15 +987,10 @@ package body Contracts is
       Saved_SMP : constant Node_Id         := SPARK_Mode_Pragma;
       --  Save the SPARK_Mode-related data to restore on exit
 
-      AR_Val   : Boolean := False;
-      AW_Val   : Boolean := False;
-      ER_Val   : Boolean := False;
-      EW_Val   : Boolean := False;
       NC_Val   : Boolean := False;
       Items    : Node_Id;
       Prag     : Node_Id;
       Ref_Elmt : Elmt_Id;
-      Seen     : Boolean := False;
 
    begin
       --  The loop parameter in an element iterator over a formal container
@@ -813,41 +1057,8 @@ package body Contracts is
 
       else pragma Assert (Ekind (Obj_Id) = E_Variable);
 
-         --  Analyze all external properties
-
-         Prag := Get_Pragma (Obj_Id, Pragma_Async_Readers);
-
-         if Present (Prag) then
-            Analyze_External_Property_In_Decl_Part (Prag, AR_Val);
-            Seen := True;
-         end if;
-
-         Prag := Get_Pragma (Obj_Id, Pragma_Async_Writers);
-
-         if Present (Prag) then
-            Analyze_External_Property_In_Decl_Part (Prag, AW_Val);
-            Seen := True;
-         end if;
-
-         Prag := Get_Pragma (Obj_Id, Pragma_Effective_Reads);
-
-         if Present (Prag) then
-            Analyze_External_Property_In_Decl_Part (Prag, ER_Val);
-            Seen := True;
-         end if;
-
-         Prag := Get_Pragma (Obj_Id, Pragma_Effective_Writes);
-
-         if Present (Prag) then
-            Analyze_External_Property_In_Decl_Part (Prag, EW_Val);
-            Seen := True;
-         end if;
-
-         --  Verify the mutual interaction of the various external properties
-
-         if Seen then
-            Check_External_Properties (Obj_Id, AR_Val, AW_Val, ER_Val, EW_Val);
-         end if;
+         Check_Type_Or_Object_External_Properties
+           (Type_Or_Obj_Id => Obj_Id);
 
          --  Analyze the non-external volatility property No_Caching
 
@@ -911,47 +1122,6 @@ package body Contracts is
          else
             Check_Missing_Part_Of (Obj_Id);
          end if;
-
-         --  The following checks are relevant only when SPARK_Mode is on, as
-         --  they are not standard Ada legality rules. Internally generated
-         --  temporaries are ignored.
-
-         if SPARK_Mode = On and then Comes_From_Source (Obj_Id) then
-            if Is_Effectively_Volatile (Obj_Id) then
-
-               --  The declaration of an effectively volatile object must
-               --  appear at the library level (SPARK RM 7.1.3(3), C.6(6)).
-
-               if not Is_Library_Level_Entity (Obj_Id) then
-                  Error_Msg_N
-                    ("volatile variable & must be declared at library level "
-                     & "(SPARK RM 7.1.3(3))", Obj_Id);
-
-               --  An object of a discriminated type cannot be effectively
-               --  volatile except for protected objects (SPARK RM 7.1.3(5)).
-
-               elsif Has_Discriminants (Obj_Typ)
-                 and then not Is_Protected_Type (Obj_Typ)
-               then
-                  Error_Msg_N
-                    ("discriminated object & cannot be volatile", Obj_Id);
-               end if;
-
-            --  The object is not effectively volatile
-
-            else
-               --  A non-effectively volatile object cannot have effectively
-               --  volatile components (SPARK RM 7.1.3(6)).
-
-               if not Is_Effectively_Volatile (Obj_Id)
-                 and then Has_Volatile_Component (Obj_Typ)
-               then
-                  Error_Msg_N
-                    ("non-volatile object & cannot have volatile components",
-                     Obj_Id);
-               end if;
-            end if;
-         end if;
       end if;
 
       --  Common checks
@@ -1304,6 +1474,16 @@ package body Contracts is
       Restore_SPARK_Mode (Saved_SM, Saved_SMP);
    end Analyze_Task_Contract;
 
+   ---------------------------
+   -- Analyze_Type_Contract --
+   ---------------------------
+
+   procedure Analyze_Type_Contract (Type_Id : Entity_Id) is
+   begin
+      Check_Type_Or_Object_External_Properties
+        (Type_Or_Obj_Id => Type_Id);
+   end Analyze_Type_Contract;
+
    -----------------------------
    -- Create_Generic_Contract --
    -----------------------------
@@ -2757,6 +2937,15 @@ package body Contracts is
                Analyze_Task_Contract (Defining_Entity (Decl));
             end if;
 
+            if Nkind_In (Decl, N_Full_Type_Declaration,
+                               N_Private_Type_Declaration,
+                               N_Task_Type_Declaration,
+                               N_Protected_Type_Declaration,
+                               N_Formal_Type_Declaration)
+            then
+               Analyze_Type_Contract (Defining_Identifier (Decl));
+            end if;
+
             Prev (Decl);
          end loop;
       end Freeze_Contracts;
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);
diff --git a/gcc/ada/einfo.adb b/gcc/ada/einfo.adb
index ee1aecb..83beff6 100644
--- a/gcc/ada/einfo.adb
+++ b/gcc/ada/einfo.adb
@@ -1291,6 +1291,8 @@ package body Einfo is
                        E_Package,
                        E_Package_Body)
            or else
+         Is_Type (Id)                         --  types
+           or else
          Ekind (Id) = E_Void);                --  special purpose
       return Node34 (Id);
    end Contract;
@@ -4146,6 +4148,10 @@ package body Einfo is
          Ekind_In (Id, E_Generic_Package,     --  packages
                        E_Package,
                        E_Package_Body)
+
+           or else
+         Is_Type (Id)                         -- types
+
            or else
          Ekind (Id) = E_Void);                --  special purpose
       Set_Node34 (Id, V);
@@ -11271,11 +11277,10 @@ package body Einfo is
             | E_Package
             | E_Package_Body
             | E_Procedure
-            | E_Protected_Type
             | E_Subprogram_Body
             | E_Task_Body
-            | E_Task_Type
             | E_Variable
+            | Type_Kind
             | E_Void
          =>
             Write_Str ("Contract");
diff --git a/gcc/ada/einfo.ads b/gcc/ada/einfo.ads
index e28fcd0..75474cd 100644
--- a/gcc/ada/einfo.ads
+++ b/gcc/ada/einfo.ads
@@ -744,9 +744,9 @@ package Einfo is
 
 --    Contract (Node34)
 --       Defined in constant, entry, entry family, operator, [generic] package,
---       package body, protected type, [generic] subprogram, subprogram body,
---       variable and task type entities. Points to the contract of the entity,
---       holding various assertion items and data classifiers.
+--       package body, protected unit, [generic] subprogram, subprogram body,
+--       variable, task unit, and type entities. Points to the contract of the
+--       entity, holding various assertion items and data classifiers.
 
 --    Contract_Wrapper (Node25)
 --       Defined in entry and entry family entities. Set only when the entry
diff --git a/gcc/ada/sem_ch12.adb b/gcc/ada/sem_ch12.adb
index 93a3ca5..e366531 100644
--- a/gcc/ada/sem_ch12.adb
+++ b/gcc/ada/sem_ch12.adb
@@ -11315,6 +11315,44 @@ package body Sem_Ch12 is
                Actual);
          end if;
 
+         --  Check actual/formal compatibility with respect to the four
+         --  volatility refinement aspects.
+
+         declare
+            Actual_Obj : Entity_Id;
+            N          : Node_Id := Actual;
+         begin
+            --  Similar to Sem_Util.Get_Enclosing_Object, but treat
+            --  pointer dereference like component selection.
+            loop
+               if Is_Entity_Name (N) then
+                  Actual_Obj := Entity (N);
+                  exit;
+               end if;
+
+               case Nkind (N) is
+                  when N_Indexed_Component
+                     | N_Selected_Component
+                     | N_Slice
+                     | N_Explicit_Dereference
+                  =>
+                     N := Prefix (N);
+
+                  when N_Type_Conversion =>
+                     N := Expression (N);
+
+                  when others =>
+                     Actual_Obj := Etype (N);
+                     exit;
+               end case;
+            end loop;
+
+            Check_Volatility_Compatibility
+              (Actual_Obj, A_Gen_Obj, "actual object",
+               "its corresponding formal object of mode in out",
+               Srcpos_Bearer => Actual);
+         end;
+
       --  Formal in-parameter
 
       else
@@ -11510,6 +11548,7 @@ package body Sem_Ch12 is
         and then Present (Actual)
         and then Is_Object_Reference (Actual)
         and then Is_Effectively_Volatile_Object (Actual)
+        and then not Is_Effectively_Volatile (A_Gen_Obj)
       then
          Error_Msg_N
            ("volatile object cannot act as actual in generic instantiation",
@@ -12480,6 +12519,14 @@ package body Sem_Ch12 is
                  ("actual for& must have Independent_Components specified",
                      Actual, A_Gen_T);
             end if;
+
+            --  Check actual/formal compatibility with respect to the four
+            --  volatility refinement aspects.
+
+            Check_Volatility_Compatibility
+              (Act_T, A_Gen_T,
+               "actual type", "its corresponding formal type",
+               Srcpos_Bearer => Act_T);
          end if;
       end Check_Shared_Variable_Control_Aspects;
 
diff --git a/gcc/ada/sem_ch13.adb b/gcc/ada/sem_ch13.adb
index f73b55a..4b042d8 100644
--- a/gcc/ada/sem_ch13.adb
+++ b/gcc/ada/sem_ch13.adb
@@ -2180,7 +2180,12 @@ package body Sem_Ch13 is
 
             --  Check some general restrictions on language defined aspects
 
-            if not Implementation_Defined_Aspect (A_Id) then
+            if not Implementation_Defined_Aspect (A_Id)
+              or else A_Id = Aspect_Async_Readers
+              or else A_Id = Aspect_Async_Writers
+              or else A_Id = Aspect_Effective_Reads
+              or else A_Id = Aspect_Effective_Reads
+            then
                Error_Msg_Name_1 := Nam;
 
                --  Not allowed for renaming declarations. Examine the original
@@ -2209,6 +2214,10 @@ package body Sem_Ch13 is
                      and then A_Id /= Aspect_Atomic_Components
                      and then A_Id /= Aspect_Independent_Components
                      and then A_Id /= Aspect_Volatile_Components
+                     and then A_Id /= Aspect_Async_Readers
+                     and then A_Id /= Aspect_Async_Writers
+                     and then A_Id /= Aspect_Effective_Reads
+                     and then A_Id /= Aspect_Effective_Reads
                   then
                      Error_Msg_N
                        ("aspect % not allowed for formal type declaration",
diff --git a/gcc/ada/sem_ch3.adb b/gcc/ada/sem_ch3.adb
index ccb0ea9..f38d6e7 100644
--- a/gcc/ada/sem_ch3.adb
+++ b/gcc/ada/sem_ch3.adb
@@ -1398,6 +1398,26 @@ package body Sem_Ch3 is
          Set_Is_Tagged_Type (T, False);
       end if;
 
+      --  For SPARK, check that the designated type is compatible with
+      --  respect to volatility with the access type.
+
+      if SPARK_Mode /= Off
+         and then Comes_From_Source (T)
+      then
+         --  ??? UNIMPLEMENTED
+         --  In the case where the designated type is incomplete at this point,
+         --  performing this check here is harmless but the check will need to
+         --  be repeated when the designated type is complete.
+
+         --  The preceding call to Comes_From_Source is needed because the
+         --  FE sometimes introduces implicitly declared access types. See,
+         --  for example, the expansion of nested_po.ads in OA28-015.
+
+         Check_Volatility_Compatibility
+           (Full_Desig, T, "designated type", "access type",
+            Srcpos_Bearer => T);
+      end if;
+
       Set_Etype (T, T);
 
       --  If the type has appeared already in a with_type clause, it is frozen
@@ -7265,6 +7285,7 @@ package body Sem_Ch3 is
       Set_First_Rep_Item (Implicit_Base, First_Rep_Item (Parent_Base));
       Set_Parent         (Implicit_Base, Parent (Derived_Type));
       Set_Is_Known_Valid (Implicit_Base, Is_Known_Valid (Parent_Base));
+      Set_Is_Volatile    (Implicit_Base, Is_Volatile    (Parent_Base));
 
       --  Set RM Size for discrete type or decimal fixed-point type
       --  Ordinary fixed-point is excluded, why???
diff --git a/gcc/ada/sem_prag.adb b/gcc/ada/sem_prag.adb
index d05b8fe..05171d4 100644
--- a/gcc/ada/sem_prag.adb
+++ b/gcc/ada/sem_prag.adb
@@ -2123,7 +2123,8 @@ package body Sem_Prag is
                & """No_Caching"" (SPARK RM 7.1.2(6))", N);
          else
             SPARK_Msg_N
-              ("external property % must apply to a volatile object", N);
+              ("external property % must apply to a volatile type or object",
+               N);
          end if;
 
       --  Pragma No_Caching should only apply to volatile variables of
@@ -7847,6 +7848,7 @@ package body Sem_Prag is
            and then Prag_Id = Pragma_Volatile
            and then not Nkind_In (Original_Node (Decl),
                                   N_Full_Type_Declaration,
+                                  N_Formal_Type_Declaration,
                                   N_Object_Declaration,
                                   N_Single_Protected_Declaration,
                                   N_Single_Task_Declaration)
@@ -13476,41 +13478,65 @@ package body Sem_Prag is
             | Pragma_No_Caching
          =>
          Async_Effective : declare
-            Obj_Decl : Node_Id;
-            Obj_Id   : Entity_Id;
-
+            Obj_Or_Type_Decl : Node_Id;
+            Obj_Or_Type_Id   : Entity_Id;
          begin
             GNAT_Pragma;
             Check_No_Identifiers;
             Check_At_Most_N_Arguments  (1);
 
-            Obj_Decl := Find_Related_Context (N, Do_Checks => True);
-
-            --  Object declaration
-
-            if Nkind (Obj_Decl) /= N_Object_Declaration then
-               Pragma_Misplaced;
-               return;
+            Obj_Or_Type_Decl := Find_Related_Context (N, Do_Checks => True);
+
+            --  Pragma must apply to a object declaration or to a type
+            --  declaration (only the former in the No_Caching case).
+            --  Original_Node is necessary to account for untagged derived
+            --  types that are rewritten as subtypes of their
+            --  respective root types.
+
+            if Nkind (Obj_Or_Type_Decl) /= N_Object_Declaration then
+               if (Prag_Id = Pragma_No_Caching)
+                  or not Nkind_In (Original_Node (Obj_Or_Type_Decl),
+                                   N_Full_Type_Declaration,
+                                   N_Private_Type_Declaration,
+                                   N_Formal_Type_Declaration,
+                                   N_Task_Type_Declaration,
+                                   N_Protected_Type_Declaration)
+               then
+                  Pragma_Misplaced;
+                  return;
+               end if;
             end if;
 
-            Obj_Id := Defining_Entity (Obj_Decl);
+            Obj_Or_Type_Id := Defining_Entity (Obj_Or_Type_Decl);
 
             --  Perform minimal verification to ensure that the argument is at
-            --  least a variable. Subsequent finer grained checks will be done
-            --  at the end of the declarative region the contains the pragma.
+            --  least a variable or a type. Subsequent finer grained checks
+            --  will be done at the end of the declarative region that
+            --  contains the pragma.
 
-            if Ekind (Obj_Id) = E_Variable then
+            if Ekind (Obj_Or_Type_Id) = E_Variable or Is_Type (Obj_Or_Type_Id)
+            then
+
+               --  In the case of a type, pragma is a type-related
+               --  representation item and so requires checks common to
+               --  all type-related representation items.
+
+               if Is_Type (Obj_Or_Type_Id)
+                 and then Rep_Item_Too_Late (Obj_Or_Type_Id, N)
+               then
+                  return;
+               end if;
 
                --  A pragma that applies to a Ghost entity becomes Ghost for
                --  the purposes of legality checks and removal of ignored Ghost
                --  code.
 
-               Mark_Ghost_Pragma (N, Obj_Id);
+               Mark_Ghost_Pragma (N, Obj_Or_Type_Id);
 
                --  Chain the pragma on the contract for further processing by
                --  Analyze_External_Property_In_Decl_Part.
 
-               Add_Contract_Item (N, Obj_Id);
+               Add_Contract_Item (N, Obj_Or_Type_Id);
 
                --  Analyze the Boolean expression (if any)
 
@@ -13521,7 +13547,8 @@ package body Sem_Prag is
             --  Otherwise the external property applies to a constant
 
             else
-               Error_Pragma ("pragma % must apply to a volatile object");
+               Error_Pragma
+                 ("pragma % must apply to a volatile type or object");
             end if;
          end Async_Effective;
 
@@ -30170,7 +30197,9 @@ package body Sem_Prag is
 
          --  Skip internally generated code
 
-         elsif not Comes_From_Source (Stmt) then
+         elsif not Comes_From_Source (Stmt)
+           and then not Comes_From_Source (Original_Node (Stmt))
+         then
 
             --  The anonymous object created for a single concurrent type is a
             --  suitable context.
diff --git a/gcc/ada/sem_util.adb b/gcc/ada/sem_util.adb
index d1c63ab..76eb665 100644
--- a/gcc/ada/sem_util.adb
+++ b/gcc/ada/sem_util.adb
@@ -116,8 +116,8 @@ package body Sem_Util is
      (Item_Id  : Entity_Id;
       Property : Name_Id) return Boolean;
    --  Subsidiary to routines Async_xxx_Enabled and Effective_xxx_Enabled.
-   --  Determine whether an abstract state or a variable denoted by entity
-   --  Item_Id has enabled property Property.
+   --  Determine whether the state abstraction, variable, or type denoted by
+   --  entity Item_Id has enabled property Property.
 
    function Has_Null_Extension (T : Entity_Id) return Boolean;
    --  T is a derived tagged type. Check whether the type extension is null.
@@ -4911,6 +4911,96 @@ package body Sem_Util is
       end if;
    end Check_Unused_Body_States;
 
+   ------------------------------------
+   -- Check_Volatility_Compatibility --
+   ------------------------------------
+
+   procedure Check_Volatility_Compatibility
+     (Id1, Id2                     : Entity_Id;
+      Description_1, Description_2 : String;
+      Srcpos_Bearer                : Node_Id) is
+
+   begin
+      if SPARK_Mode /= On then
+         return;
+      end if;
+
+      declare
+         AR1 : constant Boolean := Async_Readers_Enabled (Id1);
+         AW1 : constant Boolean := Async_Writers_Enabled (Id1);
+         ER1 : constant Boolean := Effective_Reads_Enabled (Id1);
+         EW1 : constant Boolean := Effective_Writes_Enabled (Id1);
+         AR2 : constant Boolean := Async_Readers_Enabled (Id2);
+         AW2 : constant Boolean := Async_Writers_Enabled (Id2);
+         ER2 : constant Boolean := Effective_Reads_Enabled (Id2);
+         EW2 : constant Boolean := Effective_Writes_Enabled (Id2);
+
+         AR_Check_Failed : constant Boolean := AR1 and not AR2;
+         AW_Check_Failed : constant Boolean := AW1 and not AW2;
+         ER_Check_Failed : constant Boolean := ER1 and not ER2;
+         EW_Check_Failed : constant Boolean := EW1 and not EW2;
+
+         package Failure_Description is
+            procedure Note_If_Failure
+              (Failed : Boolean; Aspect_Name : String);
+            --  If Failed is False, do nothing.
+            --  If Failed is True, add Aspect_Name to the failure description.
+
+            function Failure_Text return String;
+            --  returns accumulated list of failing aspects
+         end Failure_Description;
+
+         package body Failure_Description is
+            Description_Buffer : Bounded_String;
+
+            ---------------------
+            -- Note_If_Failure --
+            ---------------------
+
+            procedure Note_If_Failure
+              (Failed : Boolean; Aspect_Name : String) is
+            begin
+               if Failed then
+                  if Description_Buffer.Length /= 0 then
+                     Append (Description_Buffer, ", ");
+                  end if;
+                  Append (Description_Buffer, Aspect_Name);
+               end if;
+            end Note_If_Failure;
+
+            ------------------
+            -- Failure_Text --
+            ------------------
+
+            function Failure_Text return String is
+            begin
+               return +Description_Buffer;
+            end Failure_Text;
+         end Failure_Description;
+
+         use Failure_Description;
+      begin
+         if AR_Check_Failed
+           or AW_Check_Failed
+           or ER_Check_Failed
+           or EW_Check_Failed
+         then
+            Note_If_Failure (AR_Check_Failed, "Async_Readers");
+            Note_If_Failure (AW_Check_Failed, "Async_Writers");
+            Note_If_Failure (ER_Check_Failed, "Effective_Reads");
+            Note_If_Failure (EW_Check_Failed, "Effective_Writes");
+
+            Error_Msg_N
+              (Description_1
+                 & " and "
+                 & Description_2
+                 & " are not compatible with respect to volatility due to "
+                 & Failure_Text,
+               Srcpos_Bearer);
+         end if;
+      end;
+   end Check_Volatility_Compatibility;
+
    -----------------
    -- Choice_List --
    -----------------
@@ -11036,28 +11126,26 @@ package body Sem_Util is
      (Item_Id  : Entity_Id;
       Property : Name_Id) return Boolean
    is
-      function Protected_Object_Has_Enabled_Property return Boolean;
-      --  Determine whether a protected object denoted by Item_Id has the
-      --  property enabled.
+      function Protected_Type_Or_Variable_Has_Enabled_Property return Boolean;
+      --  Determine whether a protected type or variable denoted by Item_Id
+      --  has the property enabled.
 
       function State_Has_Enabled_Property return Boolean;
       --  Determine whether a state denoted by Item_Id has the property enabled
 
-      function Variable_Has_Enabled_Property return Boolean;
-      --  Determine whether a variable denoted by Item_Id has the property
-      --  enabled.
-
-      -------------------------------------------
-      -- Protected_Object_Has_Enabled_Property --
-      -------------------------------------------
+      function Type_Or_Variable_Has_Enabled_Property
+        (Item_Id : Entity_Id) return Boolean;
+      --  Determine whether type or variable denoted by Item_Id has the
+      --  property enabled.
 
-      function Protected_Object_Has_Enabled_Property return Boolean is
-         Constits     : constant Elist_Id := Part_Of_Constituents (Item_Id);
-         Constit_Elmt : Elmt_Id;
-         Constit_Id   : Entity_Id;
+      -----------------------------------------------------
+      -- Protected_Type_Or_Variable_Has_Enabled_Property --
+      -----------------------------------------------------
 
+      function Protected_Type_Or_Variable_Has_Enabled_Property return Boolean
+      is
       begin
-         --  Protected objects always have the properties Async_Readers and
+         --  Protected entities always have the properties Async_Readers and
          --  Async_Writers (SPARK RM 7.1.2(16)).
 
          if Property = Name_Async_Readers
@@ -11069,21 +11157,30 @@ package body Sem_Util is
          --  properties Effective_Reads and Effective_Writes
          --  (SPARK RM 7.1.2(16)).
 
-         elsif Present (Constits) then
-            Constit_Elmt := First_Elmt (Constits);
-            while Present (Constit_Elmt) loop
-               Constit_Id := Node (Constit_Elmt);
+         elsif Is_Single_Protected_Object (Item_Id) then
+            declare
+               Constit_Elmt : Elmt_Id;
+               Constit_Id   : Entity_Id;
+               Constits     : constant Elist_Id
+                 := Part_Of_Constituents (Item_Id);
+            begin
+               if Present (Constits) then
+                  Constit_Elmt := First_Elmt (Constits);
+                  while Present (Constit_Elmt) loop
+                     Constit_Id := Node (Constit_Elmt);
+
+                     if Has_Enabled_Property (Constit_Id, Property) then
+                        return True;
+                     end if;
 
-               if Has_Enabled_Property (Constit_Id, Property) then
-                  return True;
+                     Next_Elmt (Constit_Elmt);
+                  end loop;
                end if;
-
-               Next_Elmt (Constit_Elmt);
-            end loop;
+            end;
          end if;
 
          return False;
-      end Protected_Object_Has_Enabled_Property;
+      end Protected_Type_Or_Variable_Has_Enabled_Property;
 
       --------------------------------
       -- State_Has_Enabled_Property --
@@ -11245,11 +11342,13 @@ package body Sem_Util is
          return False;
       end State_Has_Enabled_Property;
 
-      -----------------------------------
-      -- Variable_Has_Enabled_Property --
-      -----------------------------------
+      -------------------------------------------
+      -- Type_Or_Variable_Has_Enabled_Property --
+      -------------------------------------------
 
-      function Variable_Has_Enabled_Property return Boolean is
+      function Type_Or_Variable_Has_Enabled_Property
+        (Item_Id : Entity_Id) return Boolean
+      is
          function Is_Enabled (Prag : Node_Id) return Boolean;
          --  Determine whether property pragma Prag (if present) denotes an
          --  enabled property.
@@ -11297,7 +11396,11 @@ package body Sem_Util is
          EW : constant Node_Id :=
                 Get_Pragma (Item_Id, Pragma_Effective_Writes);
 
-      --  Start of processing for Variable_Has_Enabled_Property
+         Is_Derived_Type_With_Volatile_Parent_Type : constant Boolean :=
+           Is_Derived_Type (Item_Id)
+           and then Is_Effectively_Volatile (Etype (Base_Type (Item_Id)));
+
+      --  Start of processing for Type_Or_Variable_Has_Enabled_Property
 
       begin
          --  A non-effectively volatile object can never possess external
@@ -11312,23 +11415,57 @@ package body Sem_Util is
          --  property is enabled when the flag evaluates to True or the flag is
          --  missing altogether.
 
-         elsif Property = Name_Async_Readers    and then Is_Enabled (AR) then
-            return True;
+         elsif Property = Name_Async_Readers    and then Present (AR) then
+            return Is_Enabled (AR);
 
-         elsif Property = Name_Async_Writers    and then Is_Enabled (AW) then
-            return True;
+         elsif Property = Name_Async_Writers    and then Present (AW) then
+            return Is_Enabled (AW);
 
-         elsif Property = Name_Effective_Reads  and then Is_Enabled (ER) then
-            return True;
+         elsif Property = Name_Effective_Reads  and then Present (ER) then
+            return Is_Enabled (ER);
 
-         elsif Property = Name_Effective_Writes and then Is_Enabled (EW) then
-            return True;
+         elsif Property = Name_Effective_Writes and then Present (EW) then
+            return Is_Enabled (EW);
+
+         --  If other properties are set explicitly, then this one is set
+         --  implicitly to False, except in the case of a derived type
+         --  whose parent type is volatile (in that case, we will inherit
+         --  from the parent type, below).
+
+         elsif (Present (AR)
+           or else Present (AW)
+           or else Present (ER)
+           or else Present (EW))
+           and then not Is_Derived_Type_With_Volatile_Parent_Type
+         then
+            return False;
+
+         --  For a private type, may need to 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 (Full_View (Item_Id));
+
+         --  For a derived type whose parent type is volatile, the
+         --  property may be inherited (but ignore a non-volatile parent).
+
+         elsif Is_Derived_Type_With_Volatile_Parent_Type then
+            return Type_Or_Variable_Has_Enabled_Property
+              (First_Subtype (Etype (Base_Type (Item_Id))));
+
+         --  If not specified explicitly for an object and the type
+         --  is effectively volatile, then take result from the type.
+
+         elsif not Is_Type (Item_Id)
+           and then Is_Effectively_Volatile (Etype (Item_Id))
+         then
+            return Has_Enabled_Property (Etype (Item_Id), Property);
 
          --  The implicit case lacks all property pragmas
 
          elsif No (AR) and then No (AW) and then No (ER) and then No (EW) then
             if Is_Protected_Type (Etype (Item_Id)) then
-               return Protected_Object_Has_Enabled_Property;
+               return Protected_Type_Or_Variable_Has_Enabled_Property;
             else
                return True;
             end if;
@@ -11336,7 +11473,7 @@ package body Sem_Util is
          else
             return False;
          end if;
-      end Variable_Has_Enabled_Property;
+      end Type_Or_Variable_Has_Enabled_Property;
 
    --  Start of processing for Has_Enabled_Property
 
@@ -11348,7 +11485,11 @@ package body Sem_Util is
          return State_Has_Enabled_Property;
 
       elsif Ekind (Item_Id) = E_Variable then
-         return Variable_Has_Enabled_Property;
+         return Type_Or_Variable_Has_Enabled_Property (Item_Id);
+
+      elsif Is_Type (Item_Id) then
+         return Type_Or_Variable_Has_Enabled_Property
+           (Item_Id => First_Subtype (Item_Id));
 
       --  By default, protected objects only have the properties Async_Readers
       --  and Async_Writers. If they have Part_Of components, they also inherit
@@ -11356,7 +11497,7 @@ package body Sem_Util is
       --  (SPARK RM 7.1.2(16)).
 
       elsif Ekind (Item_Id) = E_Protected_Object then
-         return Protected_Object_Has_Enabled_Property;
+         return Protected_Type_Or_Variable_Has_Enabled_Property;
 
       --  Otherwise a property is enabled when the related item is effectively
       --  volatile.
diff --git a/gcc/ada/sem_util.ads b/gcc/ada/sem_util.ads
index 07619fc..74fa2a6 100644
--- a/gcc/ada/sem_util.ads
+++ b/gcc/ada/sem_util.ads
@@ -157,14 +157,12 @@ package Sem_Util is
    --  force an error).
 
    function Async_Readers_Enabled (Id : Entity_Id) return Boolean;
-   --  Given the entity of an abstract state or a variable, determine whether
-   --  Id is subject to external property Async_Readers and if it is, the
-   --  related expression evaluates to True.
+   --  Id should be the entity of a state abstraction, a variable, or a type.
+   --  Returns True iff Id is subject to external property Async_Readers.
 
    function Async_Writers_Enabled (Id : Entity_Id) return Boolean;
-   --  Given the entity of an abstract state or a variable, determine whether
-   --  Id is subject to external property Async_Writers and if it is, the
-   --  related expression evaluates to True.
+   --  Id should be the entity of a state abstraction, a variable, or a type.
+   --  Returns True iff Id is subject to external property Async_Writers.
 
    function Available_Full_View_Of_Component (T : Entity_Id) return Boolean;
    --  If at the point of declaration an array type has a private or limited
@@ -456,6 +454,19 @@ package Sem_Util is
    --  and the context is external to the protected operation, to warn against
    --  a possible unlocked access to data.
 
+   procedure Check_Volatility_Compatibility
+     (Id1, Id2                     : Entity_Id;
+      Description_1, Description_2 : String;
+      Srcpos_Bearer                : Node_Id);
+   --  Id1 and Id2 should each be the entity of a state abstraction, a
+   --  variable, or a type (i.e., something suitable for passing to
+   --  Async_Readers_Enabled and similar functions).
+   --  Does nothing if SPARK_Mode /= On. Otherwise, flags a legality violation
+   --  if one or more of the four volatility-related aspects is False for Id1
+   --  and True for Id2. The two descriptions are included in the error message
+   --  text; the source position for the generated message is determined by
+   --  Srcpos_Bearer.
+
    function Choice_List (N : Node_Id) return List_Id;
    --  Utility to retrieve the choices of a Component_Association or the
    --  Discrete_Choices of an Iterated_Component_Association. For various
@@ -664,14 +675,12 @@ package Sem_Util is
    --  are looked through.
 
    function Effective_Reads_Enabled (Id : Entity_Id) return Boolean;
-   --  Given the entity of an abstract state or a variable, determine whether
-   --  Id is subject to external property Effective_Reads and if it is, the
-   --  related expression evaluates to True.
+   --  Id should be the entity of a state abstraction, a variable, or a type.
+   --  Returns True iff Id is subject to external property Effective_Reads.
 
    function Effective_Writes_Enabled (Id : Entity_Id) return Boolean;
-   --  Given the entity of an abstract state or a variable, determine whether
-   --  Id is subject to external property Effective_Writes and if it is, the
-   --  related expression evaluates to True.
+   --  Id should be the entity of a state abstraction, a variable, or a type.
+   --  Returns True iff Id is subject to external property Effective_Writes.
 
    function Enclosing_Comp_Unit_Node (N : Node_Id) return Node_Id;
    --  Returns the enclosing N_Compilation_Unit node that is the root of a