* [Ada] Avoid spurious error in GNATprove mode on non-null access types
@ 2019-08-21 8:31 Pierre-Marie de Rodat
0 siblings, 0 replies; only message in thread
From: Pierre-Marie de Rodat @ 2019-08-21 8:31 UTC (permalink / raw)
To: gcc-patches; +Cc: Yannick Moy
[-- Attachment #1: Type: text/plain, Size: 405 bytes --]
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 <moy@adacore.com>
gcc/ada/
* checks.adb (Install_Null_Excluding_Check): Do not install
check in GNATprove mode.
[-- Attachment #2: patch.diff --]
[-- Type: text/x-diff, Size: 320 bytes --]
--- 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,
^ permalink raw reply [flat|nested] only message in thread
only message in thread, other threads:[~2019-08-21 8:31 UTC | newest]
Thread overview: (only message) (download: mbox.gz / follow: Atom feed)
-- links below jump to the message on this page --
2019-08-21 8:31 [Ada] Avoid spurious error in GNATprove mode on non-null access types Pierre-Marie de Rodat
This is a public inbox, see mirroring instructions
for how to clone and mirror all data and code used for this inbox;
as well as URLs for read-only IMAP folder(s) and NNTP newsgroup(s).