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

2 files changed, 30 insertions, 25 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;
diff --git a/gcc/ada/sem_prag.adb b/gcc/ada/sem_prag.adb
index 8cc42c6..20c90b1 100644
--- a/gcc/ada/sem_prag.adb
+++ b/gcc/ada/sem_prag.adb
@@ -2139,11 +2139,24 @@ package body Sem_Prag is
       Expr     : Node_Id;
 
    begin
-      --  Do not analyze the pragma multiple times, but set the output
-      --  parameter to the argument specified by the pragma.
+      --  Ensure that the Boolean expression (if present) is static. A missing
+      --  argument defaults the value to True (SPARK RM 7.1.2(5)).
+
+      Expr_Val := True;
+
+      if Present (Arg1) then
+         Expr := Get_Pragma_Arg (Arg1);
+
+         if Is_OK_Static_Expression (Expr) then
+            Expr_Val := Is_True (Expr_Value (Expr));
+         end if;
+      end if;
+
+      --  The output parameter was set to the argument specified by the pragma.
+      --  Do not analyze the pragma multiple times.
 
       if Is_Analyzed_Pragma (N) then
-         goto Leave;
+         return;
       end if;
 
       Error_Msg_Name_1 := Pragma_Name (N);
@@ -2163,9 +2176,11 @@ package body Sem_Prag is
          if Ekind (Obj_Id) = E_Variable
            and then No_Caching_Enabled (Obj_Id)
          then
-            SPARK_Msg_N
-              ("illegal combination of external property % and property "
-               & """No_Caching"" (SPARK RM 7.1.2(6))", N);
+            if Expr_Val then  --  Confirming value of False is allowed
+               SPARK_Msg_N
+                 ("illegal combination of external property % and property "
+                  & """No_Caching"" (SPARK RM 7.1.2(6))", N);
+            end if;
          else
             SPARK_Msg_N
               ("external property % must apply to a volatile type or object",
@@ -2185,22 +2200,6 @@ package body Sem_Prag is
       end if;
 
       Set_Is_Analyzed_Pragma (N);
-
-      <<Leave>>
-
-      --  Ensure that the Boolean expression (if present) is static. A missing
-      --  argument defaults the value to True (SPARK RM 7.1.2(5)).
-
-      Expr_Val := True;
-
-      if Present (Arg1) then
-         Expr := Get_Pragma_Arg (Arg1);
-
-         if Is_OK_Static_Expression (Expr) then
-            Expr_Val := Is_True (Expr_Value (Expr));
-         end if;
-      end if;
-
    end Analyze_External_Property_In_Decl_Part;
 
    ---------------------------------