[Ada] Flip the meaning of debug switch -gnatdF

2019-07-11  Yannick Moy  <moy@adacore.com>

gcc/ada/

	* debug.adb: Flip meaning of debug switch -gnatdF.

From-SVN: r273404

diff --git a/gcc/ada/ChangeLog b/gcc/ada/ChangeLog
index 15b90e379cbfb6b42921d18b98c577bcac2d18c7..a5273a8644dd18cf7b2851dd7e221fe317223d12 100644 (file)
--- a/gcc/ada/ChangeLog
+++ b/gcc/ada/ChangeLog
@@ -1,3 +1,7 @@
+2019-07-11  Yannick Moy  <moy@adacore.com>
+
+       * debug.adb: Flip meaning of debug switch -gnatdF.
+
 2019-07-11  Yannick Moy  <moy@adacore.com>
 
        * sem_eval.adb (Is_Same_Value): Add special case for rewritten

diff --git a/gcc/ada/debug.adb b/gcc/ada/debug.adb
index 6df3d6fab9cfc8089fcf620f90b09f96fdff66c8..6a5d0eaebea8e1be57c30dbbaacb55132933710a 100644 (file)
--- a/gcc/ada/debug.adb
+++ b/gcc/ada/debug.adb
@@ -602,10 +602,11 @@ package body Debug is
    --  dE   Apply compile time elaboration checking for with relations between
    --       predefined units. Normally no checks are made.
 
-   --  dF   Perform the new SPARK checking rules for pointer aliasing. This is
-   --       only activated in GNATprove mode and on SPARK code. These rules are
-   --       not yet part of the official SPARK language, but are expected to be
-   --       included in a future version of SPARK.
+   --  dF   Disable the new SPARK checking rules for pointer aliasing. This is
+   --       only activated as part of GNATprove mode and on SPARK code. Now
+   --       that pointer support is part of the official SPARK language, this
+   --       switch allows reverting to the previous version of GNATprove
+   --       rejecting pointers.
 
    --  dG   Generate all warnings. Normally Errout suppresses warnings on
    --       units that are not part of the main extended source, and also