[gcc r13-1634] [Ada] Ignore switches for controlling frontend warnings in GNATprove mode

[gcc r13-1634] [Ada] Ignore switches for controlling frontend warnings in GNATprove mode

[Pierre-Marie de Rodat]

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

commit r13-1634-gf40948963b0847f995056fef25c41caec5a969e7
Author: Yannick Moy <moy@adacore.com>
Date:   Wed Jun 8 11:58:43 2022 +0200

    [Ada] Ignore switches for controlling frontend warnings in GNATprove mode
    
    In the special mode for GNATprove, ignore switches controlling frontend
    warnings, like already done for the control of style checks warnings.
    Also remove special handling of warning mode in Errout to make up for
    the previous division of control between -gnatw (GNAT) and --warnings
    (GNATprove).
    
    gcc/ada/
    
            * errout.adb (Record_Compilation_Errors): Remove global
            variable.
            (Compilation_Errors): Simplify.
            (Initialize): Inline Reset_Warnings.
            (Reset_Warnings): Remove.
            * errout.ads (Reset_Warnings): Remove.
            (Compilation_Errors): Update comment.
            * gnat1drv.adb (Adjust_Global_Switches): Ignore all frontend
            warnings in GNATprove mode, except regarding elaboration and
            suspicious contracts.

Diff:
---
 gcc/ada/errout.adb   | 35 +++++------------------------------
 gcc/ada/errout.ads   | 14 ++++----------
 gcc/ada/gnat1drv.adb |  8 ++++++--
 3 files changed, 15 insertions(+), 42 deletions(-)

diff --git a/gcc/ada/errout.adb b/gcc/ada/errout.adb
index 4e095a739da..79e162ab4cb 100644
--- a/gcc/ada/errout.adb
+++ b/gcc/ada/errout.adb
@@ -64,13 +64,6 @@ package body Errout is
    Finalize_Called : Boolean := False;
    --  Set True if the Finalize routine has been called
 
-   Record_Compilation_Errors : Boolean := False;
-   --  Record that a compilation error was witnessed during a given phase of
-   --  analysis for gnat2why. This is needed as Warning_Mode is modified twice
-   --  in gnat2why, hence Erroutc.Compilation_Errors can only return a suitable
-   --  value for each phase of analysis separately. This is updated at each
-   --  call to Compilation_Errors.
-
    Warn_On_Instance : Boolean;
    --  Flag set true for warning message to be posted on instance
 
@@ -252,17 +245,8 @@ package body Errout is
    begin
       if not Finalize_Called then
          raise Program_Error;
-
-      --  Record that a compilation error was witnessed during a given phase of
-      --  analysis for gnat2why. This is needed as Warning_Mode is modified
-      --  twice in gnat2why, hence Erroutc.Compilation_Errors can only return a
-      --  suitable value for each phase of analysis separately.
-
       else
-         Record_Compilation_Errors :=
-           Record_Compilation_Errors or else Erroutc.Compilation_Errors;
-
-         return Record_Compilation_Errors;
+         return Erroutc.Compilation_Errors;
       end if;
    end Compilation_Errors;
 
@@ -1914,7 +1898,10 @@ package body Errout is
 
       --  Reset counts for warnings
 
-      Reset_Warnings;
+      Warnings_Treated_As_Errors := 0;
+      Warnings_Detected := 0;
+      Warning_Info_Messages := 0;
+      Warnings_As_Errors_Count := 0;
 
       --  Initialize warnings tables
 
@@ -3414,18 +3401,6 @@ package body Errout is
       end loop;
    end Remove_Warning_Messages;
 
-   --------------------
-   -- Reset_Warnings --
-   --------------------
-
-   procedure Reset_Warnings is
-   begin
-      Warnings_Treated_As_Errors := 0;
-      Warnings_Detected := 0;
-      Warning_Info_Messages := 0;
-      Warnings_As_Errors_Count := 0;
-   end Reset_Warnings;
-
    ----------------------
    -- Adjust_Name_Case --
    ----------------------
diff --git a/gcc/ada/errout.ads b/gcc/ada/errout.ads
index c115a1ba533..45166f5e835 100644
--- a/gcc/ada/errout.ads
+++ b/gcc/ada/errout.ads
@@ -858,11 +858,6 @@ package Errout is
    --  Remove warnings on all elements of a list (Calls Remove_Warning_Messages
    --  on each element of the list, see above).
 
-   procedure Reset_Warnings;
-   --  Reset the counts related to warnings. This is used both to initialize
-   --  these counts and to reset them after each phase of analysis for a given
-   --  value of Opt.Warning_Mode in gnat2why.
-
    procedure Set_Ignore_Errors (To : Boolean);
    --  Following a call to this procedure with To=True, all error calls are
    --  ignored. A call with To=False restores the default treatment in which
@@ -910,11 +905,10 @@ package Errout is
    --  matching Warnings Off pragma preceding this one.
 
    function Compilation_Errors return Boolean;
-   --  Returns True if errors have been detected, or warnings in -gnatwe (treat
-   --  warnings as errors) mode. Note that it is mandatory to call Finalize
-   --  before calling this routine. To account for changes to Warning_Mode in
-   --  gnat2why between phases, the past or current presence of an error is
-   --  recorded in a global variable at each call.
+   --  Returns True if errors have been detected, or warnings when they are
+   --  treated as errors, which corresponds to switch -gnatwe in the compiler,
+   --  and other switches in other tools. Note that it is mandatory to call
+   --  Finalize before calling this routine.
 
    procedure Error_Msg_CRT (Feature : String; N : Node_Id);
    --  Posts a non-fatal message on node N saying that the feature identified
diff --git a/gcc/ada/gnat1drv.adb b/gcc/ada/gnat1drv.adb
index 5c6fd92a825..3217546d4b9 100644
--- a/gcc/ada/gnat1drv.adb
+++ b/gcc/ada/gnat1drv.adb
@@ -557,10 +557,14 @@ procedure Gnat1drv is
          Validity_Checks_On := False;
          Check_Validity_Of_Parameters := False;
 
-         --  Turn off style check options since we are not interested in any
-         --  front-end warnings when we are getting SPARK output.
+         --  Turn off style checks and compiler warnings in GNATprove except:
+         --    - elaboration warnings, which turn into errors on SPARK code
+         --    - suspicious contracts, which are useful for SPARK code
 
          Reset_Style_Check_Options;
+         Restore_Warnings (W => (Elab_Warnings               => True,
+                                 Warn_On_Suspicious_Contract => True,
+                                 others                      => False));
 
          --  Suppress the generation of name tables for enumerations, which are
          --  not needed for formal verification, and fall outside the SPARK