[Ada] Update SPARK RM rule numbers after removing a redundant rule

2020-06-11  Piotr Trojanek  <trojanek@adacore.com>

gcc/ada/

	* sem_ch4.adb, sem_ch6.adb, sem_res.adb, sem_util.ads: Fix
	references to SPARK RM 7.1.3 rule numbers.

diff --git a/gcc/ada/sem_ch4.adb b/gcc/ada/sem_ch4.adb
index a710ba2..bb0017e 100644 (file)
--- a/gcc/ada/sem_ch4.adb
+++ b/gcc/ada/sem_ch4.adb
@@ -665,7 +665,7 @@ package body Sem_Ch4 is
                --  that outside of spec expressions, otherwise the declaration
                --  cannot be inserted and analyzed. In such a case, GNATprove
                --  later rejects the allocator as it is not used here in
-               --  a non-interfering context (SPARK 4.8(2) and 7.1.3(12)).
+               --  a non-interfering context (SPARK 4.8(2) and 7.1.3(10)).
 
                if Expander_Active
                  or else (GNATprove_Mode and then not In_Spec_Expression)

diff --git a/gcc/ada/sem_ch6.adb b/gcc/ada/sem_ch6.adb
index 787ca9b..e437445 100644 (file)
--- a/gcc/ada/sem_ch6.adb
+++ b/gcc/ada/sem_ch6.adb
@@ -11889,7 +11889,7 @@ package body Sem_Ch6 is
 
             --  A procedure cannot have an effectively volatile formal
             --  parameter of mode IN because it behaves as a constant
-            --  (SPARK RM 7.1.3(6)). -- ??? maybe 7.1.3(4)
+            --  (SPARK RM 7.1.3(4)).
 
             elsif Ekind (Scope (Formal)) = E_Procedure
               and then Ekind (Formal) = E_In_Parameter

diff --git a/gcc/ada/sem_res.adb b/gcc/ada/sem_res.adb
index 6c244db..acc9978 100644 (file)
--- a/gcc/ada/sem_res.adb
+++ b/gcc/ada/sem_res.adb
@@ -3328,7 +3328,7 @@ package body Sem_Res is
 
       procedure Flag_Effectively_Volatile_Objects (Expr : Node_Id);
       --  Emit an error concerning the illegal usage of an effectively volatile
-      --  object in interfering context (SPARK RM 7.1.3(12)).
+      --  object in interfering context (SPARK RM 7.1.3(10)).
 
       procedure Insert_Default;
       --  If the actual is missing in a call, insert in the actuals list
@@ -3613,7 +3613,7 @@ package body Sem_Res is
                then
                   Error_Msg_N
                     ("volatile object cannot appear in this context (SPARK "
-                     & "RM 7.1.3(11))", N);
+                     & "RM 7.1.3(10))", N);
                   return Skip;
                end if;
             end if;
@@ -4739,7 +4739,7 @@ package body Sem_Res is
 
                --  An effectively volatile object may act as an actual when the
                --  corresponding formal is of a non-scalar effectively volatile
-               --  type (SPARK RM 7.1.3(11)).
+               --  type (SPARK RM 7.1.3(10)).
 
                if not Is_Scalar_Type (Etype (F))
                  and then Is_Effectively_Volatile (Etype (F))
@@ -4748,7 +4748,7 @@ package body Sem_Res is
 
                --  An effectively volatile object may act as an actual in a
                --  call to an instance of Unchecked_Conversion.
-               --  (SPARK RM 7.1.3(11)).
+               --  (SPARK RM 7.1.3(10)).
 
                elsif Is_Unchecked_Conversion_Instance (Nam) then
                   null;
@@ -4758,7 +4758,7 @@ package body Sem_Res is
                elsif Is_Effectively_Volatile_Object (A) then
                   Error_Msg_N
                     ("volatile object cannot act as actual in a call (SPARK "
-                     & "RM 7.1.3(11))", A);
+                     & "RM 7.1.3(10))", A);
 
                --  Otherwise the actual denotes an expression. Inspect the
                --  expression and flag each effectively volatile object with
@@ -7544,7 +7544,7 @@ package body Sem_Res is
 
             --  An effectively volatile object subject to enabled properties
             --  Async_Writers or Effective_Reads must appear in non-interfering
-            --  context (SPARK RM 7.1.3(12)).
+            --  context (SPARK RM 7.1.3(10)).
 
             if Is_Object (E)
               and then Is_Effectively_Volatile (E)
@@ -7554,7 +7554,7 @@ package body Sem_Res is
             then
                SPARK_Msg_N
                  ("volatile object cannot appear in this context "
-                  & "(SPARK RM 7.1.3(12))", N);
+                  & "(SPARK RM 7.1.3(10))", N);
             end if;
 
             --  Check for possible elaboration issues with respect to reads of

diff --git a/gcc/ada/sem_util.ads b/gcc/ada/sem_util.ads
index 74fa2a6..34379f9 100644 (file)
--- a/gcc/ada/sem_util.ads
+++ b/gcc/ada/sem_util.ads
@@ -1919,7 +1919,7 @@ package Sem_Util is
      (Context : Node_Id;
       Obj_Ref : Node_Id) return Boolean;
    --  Determine whether node Context denotes a "non-interfering context" (as
-   --  defined in SPARK RM 7.1.3(12)) where volatile reference Obj_Ref can
+   --  defined in SPARK RM 7.1.3(10)) where volatile reference Obj_Ref can
    --  safely reside.
 
    function Is_Package_Contract_Annotation (Item : Node_Id) return Boolean;