From 5c34f30d16b99d7d0898d19193b3890452efa7cf Mon Sep 17 00:00:00 2001 From: Yannick Moy Date: Wed, 21 Aug 2019 08:29:51 +0000 Subject: [PATCH] [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 gcc/ada/ * checks.adb (Install_Null_Excluding_Check): Do not install check in GNATprove mode. From-SVN: r274780 --- gcc/ada/ChangeLog | 5 +++++ gcc/ada/checks.adb | 6 ++++++ 2 files changed, 11 insertions(+) diff --git a/gcc/ada/ChangeLog b/gcc/ada/ChangeLog index 65e57efea55..e422ee771da 100644 --- a/gcc/ada/ChangeLog +++ b/gcc/ada/ChangeLog @@ -1,3 +1,8 @@ +2019-08-21 Yannick Moy + + * checks.adb (Install_Null_Excluding_Check): Do not install + check in GNATprove mode. + 2019-08-21 Yannick Moy * sem_spark.adb (Process_Path): Do nothing on address of diff --git a/gcc/ada/checks.adb b/gcc/ada/checks.adb index 61cabedacb6..52b29fc9a3b 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,