From: Yannick Moy Date: Thu, 11 Jul 2019 08:03:19 +0000 (+0000) Subject: [Ada] Flip the meaning of debug switch -gnatdF X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=d99ef225ac0722ab011cd39386fed4e346311edb;p=gcc.git [Ada] Flip the meaning of debug switch -gnatdF 2019-07-11 Yannick Moy gcc/ada/ * debug.adb: Flip meaning of debug switch -gnatdF. From-SVN: r273404 --- diff --git a/gcc/ada/ChangeLog b/gcc/ada/ChangeLog index 15b90e379cb..a5273a8644d 100644 --- a/gcc/ada/ChangeLog +++ b/gcc/ada/ChangeLog @@ -1,3 +1,7 @@ +2019-07-11 Yannick Moy + + * debug.adb: Flip meaning of debug switch -gnatdF. + 2019-07-11 Yannick Moy * sem_eval.adb (Is_Same_Value): Add special case for rewritten diff --git a/gcc/ada/debug.adb b/gcc/ada/debug.adb index 6df3d6fab9c..6a5d0eaebea 100644 --- a/gcc/ada/debug.adb +++ b/gcc/ada/debug.adb @@ -602,10 +602,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. + -- 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