diff options
| author | Yannick Moy <moy@adacore.com> | 2020-05-26 10:15:18 +0200 |
|---|---|---|
| committer | Pierre-Marie de Rodat <derodat@adacore.com> | 2020-07-10 05:16:16 -0400 |
| commit | c24633fbbb88d0032008ab012e2e3204b9405ec4 (patch) | |
| tree | cb765a48ce1e26815ae3ac6734921e46c8c2ee02 | |
| parent | a9d72b1bcfc86f7dbd0e82dd8b44a6eb513cad3b (diff) | |
| download | gcc-c24633fbbb88d0032008ab012e2e3204b9405ec4.zip gcc-c24633fbbb88d0032008ab012e2e3204b9405ec4.tar.gz gcc-c24633fbbb88d0032008ab012e2e3204b9405ec4.tar.bz2 | |
[Ada] Remove use of debug flag -gnatdF for GNATprove
gcc/ada/
* debug.adb: Update comments to free usage of -gnatdF.
| -rw-r--r-- | gcc/ada/debug.adb | 8 |
1 files changed, 1 insertions, 7 deletions
diff --git a/gcc/ada/debug.adb b/gcc/ada/debug.adb index 316a798..0e4a530 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 |