From 014eddc6d9cec9d0fd526b1e2d3d9cb4f0674f63 Mon Sep 17 00:00:00 2001 From: Yannick Moy Date: Tue, 17 Jul 2018 08:07:31 +0000 Subject: [PATCH] [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 gcc/ada/ * gnat1drv.adb (Gnat1drv): Do not issue warning about exception not being propagated in GNATprove mode. From-SVN: r262781 --- gcc/ada/ChangeLog | 5 +++++ gcc/ada/gnat1drv.adb | 6 ++++++ 2 files changed, 11 insertions(+) diff --git a/gcc/ada/ChangeLog b/gcc/ada/ChangeLog index 9b9bdca6489..0dbbe8c11ea 100644 --- a/gcc/ada/ChangeLog +++ b/gcc/ada/ChangeLog @@ -1,3 +1,8 @@ +2018-07-17 Yannick Moy + + * gnat1drv.adb (Gnat1drv): Do not issue warning about exception not + being propagated in GNATprove mode. + 2018-07-17 Dmitriy Anisimkov * libgnat/g-socket.adb, libgnat/g-socket.ads: Reorganize and make diff --git a/gcc/ada/gnat1drv.adb b/gcc/ada/gnat1drv.adb index 95780624a86..4b8db7d5979 100644 --- 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. -- 2.30.2