[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 15b90e3..a5273a8 100644 (file)
--- a/gcc/ada/ChangeLog
+++ b/gcc/ada/ChangeLog
@@ -1,5 +1,9 @@
 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
        Loop_Entry attribute.
 

diff --git a/gcc/ada/debug.adb b/gcc/ada/debug.adb
index 6df3d6f..6a5d0ea 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