This is the mail archive of the
gcc-patches@gcc.gnu.org
mailing list for the GCC project.
[Ada] Avoid confusing warning on exception propagation in GNATprove mode
- From: Pierre-Marie de Rodat <derodat at adacore dot com>
- To: gcc-patches at gcc dot gnu dot org
- Cc: Yannick Moy <moy at adacore dot com>
- Date: Tue, 17 Jul 2018 04:23:36 -0400
- Subject: [Ada] Avoid confusing warning on exception propagation in GNATprove mode
When compiling with the restriction No_Exception_Propagation, GNAT compiler
may issue a warning about exceptions not being propagated. This warning is
useless and confusing to users for GNATprove analysis, as GNATprove
precisely detects possible exceptions, so disable the warning in that mode.
Tested on x86_64-pc-linux-gnu, committed on trunk
2018-07-17 Yannick Moy <moy@adacore.com>
gcc/ada/
* gnat1drv.adb (Gnat1drv): Do not issue warning about exception not
being propagated in GNATprove mode.
--- gcc/ada/gnat1drv.adb
+++ gcc/ada/gnat1drv.adb
@@ -467,6 +467,12 @@ procedure Gnat1drv is
Ineffective_Inline_Warnings := True;
+ -- Do not issue warnings for possible propagation of exception.
+ -- GNATprove already issues messages about possible exceptions.
+
+ No_Warn_On_Non_Local_Exception := True;
+ Warn_On_Non_Local_Exception := False;
+
-- Disable front-end optimizations, to keep the tree as close to the
-- source code as possible, and also to avoid inconsistencies between
-- trees when using different optimization switches.