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.



git-svn-id: svn+ssh://gcc.gnu.org/svn/gcc/trunk@206927 138bc75d-0d04-0410-961f-82ee72b054a4

4 files changed, 37 insertions, 25 deletions

diff --git a/gcc/ada/ChangeLog b/gcc/ada/ChangeLog
index 53e59897456..1cb84d207be 100644
--- 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 76cba3998d0..f3469364c82 100644
--- 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 ba9b0d3b663..d5497d6da6b 100644
--- 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 05cea8aa5a7..f6177eb52ee 100644
--- 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