diff options
| author | Piotr Trojanek <trojanek@adacore.com> | 2019-07-01 13:37:06 +0000 |
|---|---|---|
| committer | Pierre-Marie de Rodat <pmderodat@gcc.gnu.org> | 2019-07-01 13:37:06 +0000 |
| commit | 9d8aaa4e00958418c01a4aee5a08261108eaf997 (patch) | |
| tree | 8f0b9daed4376b3da593b9c85bb8cdf7c9ea3340 /gcc/ada/einfo.adb | |
| parent | 397348b919d12c643071ebf0ef79b2c663682523 (diff) | |
| download | gcc-9d8aaa4e00958418c01a4aee5a08261108eaf997.zip gcc-9d8aaa4e00958418c01a4aee5a08261108eaf997.tar.gz gcc-9d8aaa4e00958418c01a4aee5a08261108eaf997.tar.bz2 | |
[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
Diffstat (limited to 'gcc/ada/einfo.adb')
| -rw-r--r-- | gcc/ada/einfo.adb | 4 |
1 files changed, 2 insertions, 2 deletions
diff --git a/gcc/ada/einfo.adb b/gcc/ada/einfo.adb index 13f381d..b9a9a8d 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 |