[Ada] Allow confirming volatile properties on No_Caching variables

Volatile variables marked with the No_Caching aspect can now have
confirming aspects for other volatile properties, with a value of
False.

gcc/ada/

	* contracts.adb (Check_Type_Or_Object_External_Properties): Check
	the validity of combinations only when No_Caching is not used.
	* sem_prag.adb (Analyze_External_Property_In_Decl_Part): Check
	valid combinations with No_Caching.

1 files changed, 9 insertions, 3 deletions

diff --git a/gcc/ada/contracts.adb b/gcc/ada/contracts.adb
index ed97d16..1081b98 100644
--- a/gcc/ada/contracts.adb
+++ b/gcc/ada/contracts.adb
@@ -892,9 +892,15 @@ package body Contracts is
          end;
       end if;
 
-      --  Verify the mutual interaction of the various external properties
-
-      if Seen then
+      --  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.
+
+      if Seen
+        and then (Ekind (Type_Or_Obj_Id) /= E_Variable
+                   or else 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;