diff options
| author | Yannick Moy <moy@adacore.com> | 2019-08-21 08:31:03 +0000 |
|---|---|---|
| committer | Pierre-Marie de Rodat <pmderodat@gcc.gnu.org> | 2019-08-21 08:31:03 +0000 |
| commit | e9934e8c79c4eafbb231ed53b3a6e1c6632a1a15 (patch) | |
| tree | 48eed833232b4dc376401823d9bcdbef3b2de50d | |
| parent | 3c488e6c8675f069c94567107f777f693671f7ed (diff) | |
| download | gcc-e9934e8c79c4eafbb231ed53b3a6e1c6632a1a15.zip gcc-e9934e8c79c4eafbb231ed53b3a6e1c6632a1a15.tar.gz gcc-e9934e8c79c4eafbb231ed53b3a6e1c6632a1a15.tar.bz2 | |
[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
| -rw-r--r-- | gcc/ada/ChangeLog | 4 | ||||
| -rw-r--r-- | 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 <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 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; |