A rule about implicit Global contract for functions whose names overload
an abstract state was never implemented (and no user complained about
this). It is now removed, so references to other rules need to be
renumbered.
Tested on x86_64-pc-linux-gnu, committed on trunk
2019-07-01 Piotr Trojanek <troja...@adacore.com>
gcc/ada/
* einfo.adb, sem_ch7.adb, sem_prag.adb, sem_util.adb: Update
references to the SPARK RM after the removal of Rule 7.1.4(5).--- gcc/ada/einfo.adb
+++ gcc/ada/einfo.adb
@@ -8141,7 +8141,7 @@ package body Einfo is
function Is_External_State (Id : E) return B is
begin
-- To qualify, the abstract state must appear with option "external" or
- -- "synchronous" (SPARK RM 7.1.4(8) and (10)).
+ -- "synchronous" (SPARK RM 7.1.4(7) and (9)).
return
Ekind (Id) = E_Abstract_State
@@ -8319,7 +8319,7 @@ package body Einfo is
function Is_Synchronized_State (Id : E) return B is
begin
-- To qualify, the abstract state must appear with simple option
- -- "synchronous" (SPARK RM 7.1.4(10)).
+ -- "synchronous" (SPARK RM 7.1.4(9)).
return
Ekind (Id) = E_Abstract_State
--- gcc/ada/sem_ch7.adb
+++ gcc/ada/sem_ch7.adb
@@ -3253,7 +3253,7 @@ package body Sem_Ch7 is
-- A [generic] package that defines at least one non-null abstract state
-- requires a completion only when at least one other construct requires
- -- a completion in a body (SPARK RM 7.1.4(4) and (6)). This check is not
+ -- a completion in a body (SPARK RM 7.1.4(4) and (5)). This check is not
-- performed if the caller requests this behavior.
if Do_Abstract_States
--- gcc/ada/sem_prag.adb
+++ gcc/ada/sem_prag.adb
@@ -12219,7 +12219,7 @@ package body Sem_Prag is
Check_Ghost_Synchronous;
-- Option Part_Of without an encapsulating state is
- -- illegal (SPARK RM 7.1.4(9)).
+ -- illegal (SPARK RM 7.1.4(8)).
elsif Chars (Opt) = Name_Part_Of then
SPARK_Msg_N
--- gcc/ada/sem_util.adb
+++ gcc/ada/sem_util.adb
@@ -10737,7 +10737,7 @@ package body Sem_Util is
-- Asynch_Writers Effective_Writes
--
-- Note that both forms of External have higher precedence than
- -- Synchronous (SPARK RM 7.1.4(10)).
+ -- Synchronous (SPARK RM 7.1.4(9)).
elsif Has_Synchronous then
return Nam_In (Property, Name_Async_Readers, Name_Async_Writers);
