SPARK RM 7.1.3(8) has been deleted, but there were actually plenty of
mistakes in references to rules 7.1.3(X). This patch fixes them in both
comments and error messages.
Tested on x86_64-pc-linux-gnu, committed on trunk
2020-06-11 Piotr Trojanek <troja...@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.--- gcc/ada/sem_ch4.adb
+++ 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)
--- gcc/ada/sem_ch6.adb
+++ 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
--- gcc/ada/sem_res.adb
+++ 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
--- gcc/ada/sem_util.ads
+++ 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;
