ada: Allow No_Caching on volatile types

SPARK RM now allow the property No_Caching on volatile types, to
indicate that they should be considered volatile for compilation, but
not by GNATprove's analysis.

gcc/ada/

	* contracts.adb (Add_Contract_Item): Allow No_Caching on types.
	(Check_Type_Or_Object_External_Properties): Check No_Caching.
	Check that non-effectively volatile types does not contain an
	effectively volatile component (instead of just a volatile
	component).
	(Analyze_Object_Contract): Remove shared checking of No_Caching.
	* sem_prag.adb (Analyze_External_Property_In_Decl_Part): Adapt checking
	of No_Caching for types.
	(Analyze_Pragma): Allow No_Caching on types.
	* sem_util.adb (Has_Effectively_Volatile_Component): New query function.
	(Is_Effectively_Volatile): Type with Volatile and No_Caching is not
	effectively volatile.
	(No_Caching_Enabled): Remove assertion to apply to all entities.
	* sem_util.ads: Same.

1 files changed, 16 insertions, 16 deletions

diff --git a/gcc/ada/contracts.adb b/gcc/ada/contracts.adb
index 6f474eb..59121ca 100644
--- a/gcc/ada/contracts.adb
+++ b/gcc/ada/contracts.adb
@@ -316,6 +316,7 @@ package body Contracts is
                         | Name_Async_Writers
                         | Name_Effective_Reads
                         | Name_Effective_Writes
+                        | Name_No_Caching
               or else (Ekind (Id) = E_Task_Type
                          and Prag_Nam in Name_Part_Of
                                        | Name_Depends
@@ -859,6 +860,7 @@ package body Contracts is
       AW_Val  : Boolean := False;
       ER_Val  : Boolean := False;
       EW_Val  : Boolean := False;
+      NC_Val  : Boolean;
       Seen    : Boolean := False;
       Prag    : Node_Id;
       Obj_Typ : Entity_Id;
@@ -956,18 +958,25 @@ package body Contracts is
       end if;
 
       --  Verify the mutual interaction of the various external properties.
-      --  For variables for which No_Caching is enabled, it has been checked
-      --  already that only False values for other external properties are
-      --  allowed.
+      --  For types and variables for which No_Caching is enabled, it has been
+      --  checked already that only False values for other external properties
+      --  are allowed.
 
       if Seen
-        and then (Ekind (Type_Or_Obj_Id) /= E_Variable
-                   or else not No_Caching_Enabled (Type_Or_Obj_Id))
+        and then not No_Caching_Enabled (Type_Or_Obj_Id)
       then
          Check_External_Properties
            (Type_Or_Obj_Id, AR_Val, AW_Val, ER_Val, EW_Val);
       end if;
 
+      --  Analyze the non-external volatility property No_Caching
+
+      Prag := Get_Pragma (Type_Or_Obj_Id, Pragma_No_Caching);
+
+      if Present (Prag) then
+         Analyze_External_Property_In_Decl_Part (Prag, NC_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, as well as return objects.
@@ -1047,10 +1056,10 @@ package body Contracts is
 
             if Is_Type_Id
               and then not Is_Effectively_Volatile (Type_Or_Obj_Id)
-              and then Has_Volatile_Component (Type_Or_Obj_Id)
+              and then Has_Effectively_Volatile_Component (Type_Or_Obj_Id)
             then
                Error_Msg_N
-                 ("non-volatile type & cannot have volatile"
+                 ("non-volatile type & cannot have effectively volatile"
                     & " components",
                   Type_Or_Obj_Id);
             end if;
@@ -1076,7 +1085,6 @@ package body Contracts is
       Saved_SMP : constant Node_Id         := SPARK_Mode_Pragma;
       --  Save the SPARK_Mode-related data to restore on exit
 
-      NC_Val   : Boolean;
       Items    : Node_Id;
       Prag     : Node_Id;
       Ref_Elmt : Elmt_Id;
@@ -1118,14 +1126,6 @@ package body Contracts is
 
       Check_Type_Or_Object_External_Properties (Type_Or_Obj_Id => Obj_Id);
 
-      --  Analyze the non-external volatility property No_Caching
-
-      Prag := Get_Pragma (Obj_Id, Pragma_No_Caching);
-
-      if Present (Prag) then
-         Analyze_External_Property_In_Decl_Part (Prag, NC_Val);
-      end if;
-
       --  Constant-related checks
 
       if Ekind (Obj_Id) = E_Constant then