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

gcc/ada/ChangeLog

+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.

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;
 
    -----------------

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,21 +1215,24 @@ 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;
-      end if;
    end Set_Warnings_Mode_On;
 
    ------------------------------------

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