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.
Tested on x86_64-pc-linux-gnu, committed on trunk
2019-08-21 Yannick Moy <m...@adacore.com>
gcc/ada/
* checks.adb (Install_Null_Excluding_Check): Do not install
check in GNATprove mode.--- gcc/ada/checks.adb
+++ 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,
