From 9d8aaa4e00958418c01a4aee5a08261108eaf997 Mon Sep 17 00:00:00 2001 From: Piotr Trojanek Date: Mon, 1 Jul 2019 13:37:06 +0000 Subject: [PATCH] [Ada] Remove a SPARK rule about implicit Global 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. 2019-07-01 Piotr Trojanek 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). From-SVN: r272875 --- gcc/ada/ChangeLog | 5 +++++ gcc/ada/einfo.adb | 4 ++-- gcc/ada/sem_ch7.adb | 2 +- gcc/ada/sem_prag.adb | 2 +- gcc/ada/sem_util.adb | 2 +- 5 files changed, 10 insertions(+), 5 deletions(-) diff --git a/gcc/ada/ChangeLog b/gcc/ada/ChangeLog index 8ac9f489bb3..65ca1e6cc0a 100644 --- a/gcc/ada/ChangeLog +++ b/gcc/ada/ChangeLog @@ -1,3 +1,8 @@ +2019-07-01 Piotr Trojanek + + * 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). + 2019-07-01 Piotr Trojanek * sysdep.c: Cleanup references to LynuxWorks in docs and diff --git a/gcc/ada/einfo.adb b/gcc/ada/einfo.adb index 13f381d77af..b9a9a8d53a7 100644 --- a/gcc/ada/einfo.adb +++ b/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 diff --git a/gcc/ada/sem_ch7.adb b/gcc/ada/sem_ch7.adb index c6095ef53d2..2ed2746dd62 100644 --- a/gcc/ada/sem_ch7.adb +++ b/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 diff --git a/gcc/ada/sem_prag.adb b/gcc/ada/sem_prag.adb index 200e5dbf847..b6d259f82db 100644 --- a/gcc/ada/sem_prag.adb +++ b/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 diff --git a/gcc/ada/sem_util.adb b/gcc/ada/sem_util.adb index 13a06ccf5ab..50ea52a69f4 100644 --- a/gcc/ada/sem_util.adb +++ b/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); -- 2.30.2