From: Yannick Moy Date: Tue, 26 May 2020 08:15:18 +0000 (+0200) Subject: [Ada] Remove use of debug flag -gnatdF for GNATprove X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=c24633fbbb88d0032008ab012e2e3204b9405ec4;p=gcc.git [Ada] Remove use of debug flag -gnatdF for GNATprove gcc/ada/ * debug.adb: Update comments to free usage of -gnatdF. --- 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