[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 --git a/gcc/ada/errout.adb b/gcc/ada/errout.adb
index 4e095a739daafc69a994bf848f3b3d75a819416d..79e162ab4cb637c960d848e588c4da8fa2c0c70c 100644 (file)
--- 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 c115a1ba5332548cf722a6f4d66c11c7eb267c18..45166f5e835e5d56e2fc78403b87cab75485f2f7 100644 (file)
--- 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 5c6fd92a825a5b96685c8516f5c45a423db2a690..3217546d4b98c77f1686c955bc822aeb164681fd 100644 (file)
--- 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