diff options
| author | Yannick Moy <moy@adacore.com> | 2019-08-21 08:29:51 +0000 |
|---|---|---|
| committer | Pierre-Marie de Rodat <pmderodat@gcc.gnu.org> | 2019-08-21 08:29:51 +0000 |
| commit | 5c34f30d16b99d7d0898d19193b3890452efa7cf (patch) | |
| tree | 9df666d8b23e81743fbf6ff3da07962180b0f1f0 | |
| parent | 570d0072bdcdd0e9e7d6acb33f594c22efa24ac7 (diff) | |
| download | gcc-5c34f30d16b99d7d0898d19193b3890452efa7cf.zip gcc-5c34f30d16b99d7d0898d19193b3890452efa7cf.tar.gz gcc-5c34f30d16b99d7d0898d19193b3890452efa7cf.tar.bz2 | |
[Ada] Avoid spurious error in GNATprove mode on non-null access types
GNATprove directly handles non-null access checks, and requires that the
frontend does not insert explicit checks in the form of conditional
exceptions being raised. Now fixed.
There is no impact on compilation.
2019-08-21 Yannick Moy <moy@adacore.com>
gcc/ada/
* checks.adb (Install_Null_Excluding_Check): Do not install
check in GNATprove mode.
From-SVN: r274780
| -rw-r--r-- | gcc/ada/ChangeLog | 5 | ||||
| -rw-r--r-- | gcc/ada/checks.adb | 6 |
2 files changed, 11 insertions, 0 deletions
diff --git a/gcc/ada/ChangeLog b/gcc/ada/ChangeLog index 65e57ef..e422ee7 100644 --- a/gcc/ada/ChangeLog +++ b/gcc/ada/ChangeLog @@ -1,5 +1,10 @@ 2019-08-21 Yannick Moy <moy@adacore.com> + * checks.adb (Install_Null_Excluding_Check): Do not install + check in GNATprove mode. + +2019-08-21 Yannick Moy <moy@adacore.com> + * sem_spark.adb (Process_Path): Do nothing on address of subprogram. diff --git a/gcc/ada/checks.adb b/gcc/ada/checks.adb index 61cabed..52b29fc 100644 --- a/gcc/ada/checks.adb +++ b/gcc/ada/checks.adb @@ -7964,6 +7964,12 @@ package body Checks is return; end if; + -- In GNATprove mode, we do not apply the check + + if GNATprove_Mode then + return; + end if; + -- Otherwise install access check Insert_Action (N, |