diff options
Diffstat (limited to 'gcc')
| -rw-r--r-- | gcc/ada/ChangeLog | 4 | ||||
| -rw-r--r-- | gcc/ada/debug.adb | 9 |
2 files changed, 9 insertions, 4 deletions
diff --git a/gcc/ada/ChangeLog b/gcc/ada/ChangeLog index 15b90e3..a5273a8 100644 --- a/gcc/ada/ChangeLog +++ b/gcc/ada/ChangeLog @@ -1,5 +1,9 @@ 2019-07-11 Yannick Moy <moy@adacore.com> + * debug.adb: Flip meaning of debug switch -gnatdF. + +2019-07-11 Yannick Moy <moy@adacore.com> + * sem_eval.adb (Is_Same_Value): Add special case for rewritten Loop_Entry attribute. diff --git a/gcc/ada/debug.adb b/gcc/ada/debug.adb index 6df3d6f..6a5d0ea 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 |