[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.

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.

From-SVN: r262781

diff --git a/gcc/ada/ChangeLog b/gcc/ada/ChangeLog
index 9b9bdca64893af60458ab050a27284f4f727578c..0dbbe8c11eaa48fb1c9d94db6fd4228f5b487949 100644 (file)
--- a/gcc/ada/ChangeLog
+++ b/gcc/ada/ChangeLog
@@ -1,3 +1,8 @@
+2018-07-17  Yannick Moy  <moy@adacore.com>
+
+       * gnat1drv.adb (Gnat1drv): Do not issue warning about exception not
+       being propagated in GNATprove mode.
+
 2018-07-17  Dmitriy Anisimkov  <anisimko@adacore.com>
 
        * libgnat/g-socket.adb, libgnat/g-socket.ads: Reorganize and make

diff --git a/gcc/ada/gnat1drv.adb b/gcc/ada/gnat1drv.adb
index 95780624a86743ddde3a3447fa42d09464e70898..4b8db7d5979c0e7c5b586781ac775242e65a8bdf 100644 (file)
--- a/gcc/ada/gnat1drv.adb
+++ b/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.