[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  <trojanek@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).

From-SVN: r272875

diff --git a/gcc/ada/ChangeLog b/gcc/ada/ChangeLog
index 8ac9f489bb34a6f348ee019865e7d724d9b771f7..65ca1e6cc0abc44419baee826b9a46d303aef4be 100644 (file)
--- a/gcc/ada/ChangeLog
+++ b/gcc/ada/ChangeLog
@@ -1,3 +1,8 @@
+2019-07-01  Piotr Trojanek  <trojanek@adacore.com>
+
+       * 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  <trojanek@adacore.com>
 
        * sysdep.c: Cleanup references to LynuxWorks in docs and

diff --git a/gcc/ada/einfo.adb b/gcc/ada/einfo.adb
index 13f381d77af8fe657fb51e5c7c3ec5781dddac61..b9a9a8d53a7261ed25b82ddb869a2b63e641ff79 100644 (file)
--- 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 c6095ef53d2ae3db53db1806e552d287b42f5a59..2ed2746dd620334c6e0bf77656a6f69965adfe05 100644 (file)
--- 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 200e5dbf84719a38d0add697d869cc919ca84bf2..b6d259f82db3d3bb9d8c391e5642725bea25316d 100644 (file)
--- 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 13a06ccf5abee8eb7d5a9199a9cd4e5071b66fee..50ea52a69f444e44b23316f211a7768dd0784a23 100644 (file)
--- 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);