[Ada] Remove use of debug flag -gnatdF for GNATprove
authorYannick Moy <moy@adacore.com>
Tue, 26 May 2020 08:15:18 +0000 (10:15 +0200)
committerPierre-Marie de Rodat <derodat@adacore.com>
Fri, 10 Jul 2020 09:16:16 +0000 (05:16 -0400)
gcc/ada/

* debug.adb: Update comments to free usage of -gnatdF.

gcc/ada/debug.adb

index 316a798e58425502a13b56e13ffd4723ee787aa1..0e4a530a000dcb80dfaa18af6303f9fd1858f2f6 100644 (file)
@@ -69,7 +69,7 @@ package body Debug is
    --  dC   Output debugging information on check suppression
    --  dD   Delete elaboration checks in inner level routines
    --  dE   Apply elaboration checks to predefined units
-   --  dF   Perform the new SPARK checking rules for pointer aliasing
+   --  dF
    --  dG   Generate all warnings including those normally suppressed
    --  dH   Hold (kill) call to gigi
    --  dI   Inhibit internal name numbering in gnatG listing
@@ -602,12 +602,6 @@ package body Debug is
    --  dE   Apply compile time elaboration checking for with relations between
    --       predefined units. Normally no checks are made.
 
-   --  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
    --       suppresses warnings on instantiations in the main extended