[multiple changes]
authorArnaud Charlet <charlet@gcc.gnu.org>
Tue, 12 Sep 2017 09:52:00 +0000 (11:52 +0200)
committerArnaud Charlet <charlet@gcc.gnu.org>
Tue, 12 Sep 2017 09:52:00 +0000 (11:52 +0200)
commitfb69239a00b85f787c649b0454f0e93cc03132f8
treeb1763ab58debeb29cae0326e3c99664162305894
parent7f9fcce8343219550bb754890c178f34ccdddce7
[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
gcc/ada/ChangeLog
gcc/ada/debug.adb
gcc/ada/gcc-interface/Make-lang.in
gcc/ada/gnat1drv.adb
gcc/ada/libgnat/system.ads
gcc/ada/sem_ch6.adb
gcc/ada/sem_spark.adb [new file with mode: 0644]
gcc/ada/sem_spark.ads [new file with mode: 0644]
gcc/ada/sem_util.adb
gcc/ada/sem_util.ads