errout.adb (Initialize): Remove trick to add dummy entry in Warnings table.

2014-01-22  Yannick Moy  <moy@adacore.com>

	* errout.adb (Initialize): Remove trick to add dummy entry
	in Warnings table.
	* erroutc.adb (Set_Warnings_Mode_Off,
	Set_Warnings_Mode_On): Do nothing if warnings are suppressed by
	command line switch.
	* opt.ads (Warning_Mode): Document behavior
	wrt pragma Warnings, in normal mode and in GNATprove_Mode.

From-SVN: r206927

diff --git a/gcc/ada/ChangeLog b/gcc/ada/ChangeLog
index 53e598974569a3934224ef7fddc8d6dc67df3d52..1cb84d207be6d8b5a424824936ff36a5193f72e4 100644 (file)
--- a/gcc/ada/ChangeLog
+++ b/gcc/ada/ChangeLog
@@ -1,3 +1,13 @@
+2014-01-22  Yannick Moy  <moy@adacore.com>
+
+       * errout.adb (Initialize): Remove trick to add dummy entry
+       in Warnings table.
+       * erroutc.adb (Set_Warnings_Mode_Off,
+       Set_Warnings_Mode_On): Do nothing if warnings are suppressed by
+       command line switch.
+       * opt.ads (Warning_Mode): Document behavior
+       wrt pragma Warnings, in normal mode and in GNATprove_Mode.
+
 2014-01-22  Robert Dewar  <dewar@adacore.com>
 
        * sem_ch3.adb, errout.adb, erroutc.adb: Minor reformatting.

diff --git a/gcc/ada/errout.adb b/gcc/ada/errout.adb
index 76cba3998d09ce08c5fc761b4ae33ef389cbe2a2..f3469364c82546b4bd6c0adb7b713915d2f85ef2 100644 (file)
--- a/gcc/ada/errout.adb
+++ b/gcc/ada/errout.adb
@@ -1503,18 +1503,6 @@ package body Errout is
 
       Warnings.Init;
       Specific_Warnings.Init;
-
-      --  As an optimization, if all warnings are suppressed, we supply an
-      --  initial dummy entry covering all possible source locations, which
-      --  avoids taking into account pragma Warnings in the source. In
-      --  GNATprove_Mode, this optimization is disabled, as we rely on
-      --  the Warnings table to be correctly filled for use of the warning
-      --  mechanism for gnatprove itself.
-
-      if not GNATprove_Mode and then Warning_Mode = Suppress then
-         Warnings.Append
-           ((Start => Source_Ptr'First, Stop => Source_Ptr'Last));
-      end if;
    end Initialize;
 
    -----------------

diff --git a/gcc/ada/erroutc.adb b/gcc/ada/erroutc.adb
index ba9b0d3b663654d7040c33649f67ff1e64e99977..d5497d6da6b885cc87600597473e991bf2a5a306 100644 (file)
--- a/gcc/ada/erroutc.adb
+++ b/gcc/ada/erroutc.adb
@@ -1172,11 +1172,19 @@ package body Erroutc is
          return;
       end if;
 
+      --  If all warnings are suppressed by command line switch, this can
+      --  be ignored, unless we are in GNATprove_Mode which requires pragma
+      --  Warnings to be stored for the formal verification backend.
+
+      if Warning_Mode = Suppress
+        and then not GNATprove_Mode
+      then
+         return;
+
       --  If last entry in table already covers us, this is a redundant pragma
-      --  Warnings (Off) and can be ignored. This also handles the case where
-      --  all warnings are suppressed by command line switch.
+      --  Warnings (Off) and can be ignored.
 
-      if Warnings.Last >= Warnings.First
+      elsif Warnings.Last >= Warnings.First
         and then Warnings.Table (Warnings.Last).Start <= Loc
         and then Loc <= Warnings.Table (Warnings.Last).Stop
       then
@@ -1207,20 +1215,23 @@ package body Erroutc is
          return;
       end if;
 
+      --  If all warnings are suppressed by command line switch, this can
+      --  be ignored, unless we are in GNATprove_Mode which requires pragma
+      --  Warnings to be stored for the formal verification backend.
+
+      if Warning_Mode = Suppress
+        and then not GNATprove_Mode
+      then
+         return;
+
       --  If the last entry in the warnings table covers this pragma, then
       --  we adjust the end point appropriately.
 
-      if Warnings.Last >= Warnings.First
+      elsif Warnings.Last >= Warnings.First
         and then Warnings.Table (Warnings.Last).Start <= Loc
         and then Loc <= Warnings.Table (Warnings.Last).Stop
       then
-         --  We can normally skip this adjustment if we are suppressing all
-         --  warnings, but we do want to do it in gnatprove mode even then,
-         --  since we use the warning mechanism in gnatprove itself.
-
-         if Warning_Mode /= Suppress or else GNATprove_Mode then
-            Warnings.Table (Warnings.Last).Stop := Loc;
-         end if;
+         Warnings.Table (Warnings.Last).Stop := Loc;
       end if;
    end Set_Warnings_Mode_On;
 

diff --git a/gcc/ada/opt.ads b/gcc/ada/opt.ads
index 05cea8aa5a7c58529ca68a80a6f2420bcd375ad1..f6177eb52ee0a4aa0250f323a6bb9cd6599a9cf0 100644 (file)
--- a/gcc/ada/opt.ads
+++ b/gcc/ada/opt.ads
@@ -1737,8 +1737,11 @@ package Opt is
    --  GNAT, GNATBIND
    --  Controls treatment of warning messages. If set to Suppress, warning
    --  messages are not generated at all. In Normal mode, they are generated
-   --  but do not count as errors. In Treat_As_Error mode, warning messages
-   --  are generated and are treated as errors.
+   --  but do not count as errors. In Treat_As_Error mode, warning messages are
+   --  generated and are treated as errors. Note that Warning_Mode = Suppress
+   --  causes pragma Warnings to be ignored (except for legality checks),
+   --  unless we are in GNATprove_Mode, which requires pragma Warnings to
+   --  be stored for the formal verification backend.
 
    Wide_Character_Encoding_Method : WC_Encoding_Method := WCEM_Brackets;
    --  GNAT, GNATBIND