diff options
author | charlet <charlet@138bc75d-0d04-0410-961f-82ee72b054a4> | 2011-08-04 08:18:13 +0000 |
---|---|---|
committer | charlet <charlet@138bc75d-0d04-0410-961f-82ee72b054a4> | 2011-08-04 08:18:13 +0000 |
commit | 2ff12f45be16cc24972f57d91fcfff6b98965243 (patch) | |
tree | d0172f181b3e0387bab1071971a969a1d5197954 /gcc/ada/back_end.adb | |
parent | b1967e1d69d0a1d071945bfd1bbc9dff375138ea (diff) | |
download | gcc-2ff12f45be16cc24972f57d91fcfff6b98965243.tar.gz |
2011-08-04 Yannick Moy <moy@adacore.com>
* einfo.adb, einfo.ads (Formal_Proof_On): new flag set on subprogram
entities whose body contains an Annotate pragma which forces formal
proof on this body.
* sem_ch11.adb, sem_ch2.adb, sem_ch3.adb, sem_ch4.adb, sem_ch5.adb,
sem_ch6.adb, sem_ch9.adb, sem_res.adb: Adapt call to
Mark_Non_ALFA_Subprogram to pass in a message and node.
* sem_prag.adb (Analyze_Pragma): add treatment of pragma Annotate
(Forma_Proof, On) which sets the flag Formal_Proof_On in the
surrounding subprogram.
* sem_util.adb, sem_util.ads (Mark_Non_ALFA_Subprogram,
Mark_Non_ALFA_Subprogram_Unconditional): if the subprogram being marked
as not in ALFA is annotated with Formal_Proof being On, then an error
is issued based on the additional parameters for message and node.
* snames.ads-tmpl (Name_Formal_Proof): new name for annotation.
* gcc-interface/Make-lang.in: Update dependencies.
2011-08-04 Hristian Kirtchev <kirtchev@adacore.com>
* exp_ch3.adb (Expand_Freeze_Class_Wide_Type): Do not generate
Finalize_Address when CodePeer is enabled.
2011-08-04 Pascal Obry <obry@adacore.com>
* adaint.c (__gnat_tmp_name): Use _tempnam() instead of tempnam() as
the latter returns a pointer to a static buffer which is deallocated
at the end of the routine.
git-svn-id: svn+ssh://gcc.gnu.org/svn/gcc/trunk@177328 138bc75d-0d04-0410-961f-82ee72b054a4
Diffstat (limited to 'gcc/ada/back_end.adb')
0 files changed, 0 insertions, 0 deletions