[gcc/devel/autopar_devel] [Ada] Remove use of debug flag -gnatdF for GNATprove

Giuliano Belinassi giulianob@gcc.gnu.org
Sat Aug 22 23:30:22 GMT 2020


https://gcc.gnu.org/g:2d3c39eccc32cd94814d9e09543720927b26267c

commit 2d3c39eccc32cd94814d9e09543720927b26267c
Author: Yannick Moy <moy@adacore.com>
Date:   Tue May 26 10:15:18 2020 +0200

    [Ada] Remove use of debug flag -gnatdF for GNATprove
    
    gcc/ada/
    
            * debug.adb: Update comments to free usage of -gnatdF.

Diff:
---
 gcc/ada/debug.adb | 8 +-------
 1 file changed, 1 insertion(+), 7 deletions(-)

diff --git a/gcc/ada/debug.adb b/gcc/ada/debug.adb
index 316a798e584..0e4a530a000 100644
--- a/gcc/ada/debug.adb
+++ b/gcc/ada/debug.adb
@@ -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


More information about the Gcc-cvs mailing list