From e9934e8c79c4eafbb231ed53b3a6e1c6632a1a15 Mon Sep 17 00:00:00 2001 From: Yannick Moy Date: Wed, 21 Aug 2019 08:31:03 +0000 Subject: [Ada] Update references to the SPARK RM 2019-08-21 Yannick Moy gcc/ada/ * sem_spark.adb: Update references to the SPARK RM. From-SVN: r274787 --- gcc/ada/ChangeLog | 4 ++++ gcc/ada/sem_spark.adb | 12 ++++++------ 2 files changed, 10 insertions(+), 6 deletions(-) diff --git a/gcc/ada/ChangeLog b/gcc/ada/ChangeLog index a6508ae..9133c6c 100644 --- a/gcc/ada/ChangeLog +++ b/gcc/ada/ChangeLog @@ -1,3 +1,7 @@ +2019-08-21 Yannick Moy + + * sem_spark.adb: Update references to the SPARK RM. + 2019-08-21 Eric Botcazou * 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 a246482..aea5214 100644 --- 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; -- cgit v1.1