[Ada] Update references to the SPARK RM

2019-08-21  Yannick Moy  <moy@adacore.com>

gcc/ada/

	* sem_spark.adb: Update references to the SPARK RM.

From-SVN: r274787

diff --git a/gcc/ada/ChangeLog b/gcc/ada/ChangeLog
index a6508ae4ec1bb7ab59fe2709fc1992f9ae1f465d..9133c6c1192abf300d26937e0a255bcc2b02f912 100644 (file)
--- a/gcc/ada/ChangeLog
+++ b/gcc/ada/ChangeLog
@@ -1,3 +1,7 @@
+2019-08-21  Yannick Moy  <moy@adacore.com>
+
+       * sem_spark.adb: Update references to the SPARK RM.
+
 2019-08-21  Eric Botcazou  <ebotcazou@adacore.com>
 
        * repinfo.adb (List_Array_Info): In -gnatR4 mode, set the

diff --git a/gcc/ada/sem_spark.adb b/gcc/ada/sem_spark.adb
index a24648289572b21c05dd5c1840056564a97653d1..aea521432959319bdfdc5941c62eec8000912074 100644 (file)
--- a/gcc/ada/sem_spark.adb
+++ b/gcc/ada/sem_spark.adb
@@ -672,7 +672,7 @@ package body Sem_SPARK is
    --  Main traversal procedure to check safe pointer usage
 
    procedure Check_Old_Loop_Entry (N : Node_Id);
-   --  Check SPARK RM 3.10(14) regarding 'Old and 'Loop_Entry
+   --  Check SPARK RM 3.10(13) regarding 'Old and 'Loop_Entry
 
    procedure Check_Package_Body (Pack : Node_Id);
 
@@ -1085,7 +1085,7 @@ package body Sem_SPARK is
          Borrowed : constant Node_Id := Get_Observed_Or_Borrowed_Expr (Expr);
 
       begin
-         --  SPARK RM 3.10(8): If the type of the target is an anonymous
+         --  SPARK RM 3.10(7): If the type of the target is an anonymous
          --  access-to-variable type (an owning access type), the source shall
          --  be an owning access object [..] whose root object is the target
          --  object itself.
@@ -1100,7 +1100,7 @@ package body Sem_SPARK is
             if Emit_Messages then
                Error_Msg_NE
                  ("source of assignment must have & as root" &
-                    " (SPARK RM 3.10(8)))",
+                    " (SPARK RM 3.10(7)))",
                   Expr, Var);
             end if;
             return;
@@ -1132,7 +1132,7 @@ package body Sem_SPARK is
             if Emit_Messages then
                Error_Msg_NE
                  ("source of assignment must have & as root" &
-                    " (SPARK RM 3.10(8)))",
+                    " (SPARK RM 3.10(7)))",
                   Expr, Var);
             end if;
             return;
@@ -2855,7 +2855,7 @@ package body Sem_SPARK is
                         Error_Msg_Name_1 := Aname;
                         Error_Msg_N
                           ("prefix of % attribute must be a function call "
-                           & "(SPARK RM 3.10(14))", Pref);
+                           & "(SPARK RM 3.10(13))", Pref);
                      end if;
 
                   elsif Is_Traversal_Function_Call (Pref) then
@@ -2863,7 +2863,7 @@ package body Sem_SPARK is
                         Error_Msg_Name_1 := Aname;
                         Error_Msg_N
                           ("prefix of % attribute should not call a traversal "
-                           & "function (SPARK RM 3.10(14))", Pref);
+                           & "function (SPARK RM 3.10(13))", Pref);
                      end if;
                   end if;
                end if;