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