diff options
Diffstat (limited to 'gcc/ada/debug.adb')
| -rw-r--r-- | gcc/ada/debug.adb | 7 |
1 files changed, 6 insertions, 1 deletions
diff --git a/gcc/ada/debug.adb b/gcc/ada/debug.adb index c45a188..77afd4b 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 + -- dF Perform the new SPARK checking rules for pointer aliasing -- dG Generate all warnings including those normally suppressed -- dH Hold (kill) call to gigi -- dI Inhibit internal name numbering in gnatG listing @@ -383,6 +383,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. + -- 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 |