diff options
| author | Arnaud Charlet <charlet@gcc.gnu.org> | 2017-09-12 11:52:00 +0200 |
|---|---|---|
| committer | Arnaud Charlet <charlet@gcc.gnu.org> | 2017-09-12 11:52:00 +0200 |
| commit | fb69239a00b85f787c649b0454f0e93cc03132f8 (patch) | |
| tree | b1763ab58debeb29cae0326e3c99664162305894 /gcc/ada/debug.adb | |
| parent | 7f9fcce8343219550bb754890c178f34ccdddce7 (diff) | |
| download | gcc-fb69239a00b85f787c649b0454f0e93cc03132f8.zip gcc-fb69239a00b85f787c649b0454f0e93cc03132f8.tar.gz gcc-fb69239a00b85f787c649b0454f0e93cc03132f8.tar.bz2 | |
[multiple changes]
2017-09-12 Bob Duff <duff@adacore.com>
* sem_ch6.adb (Analyze_Expression_Function): Initialize Def_Id to
Empty.
2017-09-12 Georges-Axel Jaloyan <jaloyan@adacore.com>
* debug.adb: Reserving flag -gnatdF for safe pointer checking.
* gnat1drv.adb (gnat1drv): Adding the call to the analysis on
dF flag.
* sem_spark.adb, sem_spark.ads: Implementation of the analysis,
in preparation for the evolution of the SPARK language that
includes a pointer analysis for checking non-aliasing of access
types. The Check_Safe_Pointers function is the entry point, and
will traverse the AST and raise compile-time errors everytime
it detects non-begign aliasing. Detailed comments are present
in the sem_spark.ads file.
* sem_util.adb, sem_util.ads (First_Global, Next_Global): New
functions to iterate over the list of globals of a subprogram.
* libgnat/system.ads: Add restriction No_Finalization.
* gcc-interface/Make-lang.in: Add new file sem_spark.adb and
dependency on g-dynhta.adb.
From-SVN: r252000
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 |