diff mbox series

[Ada] Ignore switches for controlling frontend warnings in GNATprove mode

Message ID 20220712122526.GA3404840@adacore.com
State New
Headers show
Series [Ada] Ignore switches for controlling frontend warnings in GNATprove mode | expand

Commit Message

Pierre-Marie de Rodat July 12, 2022, 12:25 p.m. UTC 
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).

Tested on x86_64-pc-linux-gnu, committed on trunk

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 mbox series

Patch

diff --git a/gcc/ada/errout.adb b/gcc/ada/errout.adb
--- 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
--- 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
--- 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