https://gcc.gnu.org/g:e65b5c49b93afd69407b0133ac3ef7920125b69f

commit r16-1852-ge65b5c49b93afd69407b0133ac3ef7920125b69f
Author: Martin Clochard <cloch...@adacore.com>
Date:   Tue May 6 15:59:16 2025 +0200

    ada: Remove spurious warnings about No_Exception_Propagation in GNATprove 
mode
    
    gcc/ada/ChangeLog:
    
            * frontend.adb (Frontend): do not override GNATprove's setting for
            Warn_On_Non_Local_Exception

Diff:
---
 gcc/ada/frontend.adb | 3 ++-
 1 file changed, 2 insertions(+), 1 deletion(-)

diff --git a/gcc/ada/frontend.adb b/gcc/ada/frontend.adb
index d5376788ce42..564f153c9826 100644
--- a/gcc/ada/frontend.adb
+++ b/gcc/ada/frontend.adb
@@ -368,11 +368,12 @@ begin
       --  If we have restriction No_Exception_Propagation, and we did not have
       --  an explicit switch turning off Warn_On_Non_Local_Exception, then turn
       --  on this warning by default if we have encountered an exception
-      --  handler.
+      --  handler. We do not override the setting of GNATprove.
 
       if Restriction_Check_Required (No_Exception_Propagation)
         and then not No_Warn_On_Non_Local_Exception
         and then Exception_Handler_Encountered
+        and then not GNATprove_Mode
       then
          Warn_On_Non_Local_Exception := True;
       end if;

Reply via email to