diff options
| author | Arnaud Charlet <charlet@gcc.gnu.org> | 2013-10-10 12:47:59 +0200 |
|---|---|---|
| committer | Arnaud Charlet <charlet@gcc.gnu.org> | 2013-10-10 12:47:59 +0200 |
| commit | 0c5dba7ff5ca748346488e651641e4b93eb53a17 (patch) | |
| tree | aef1bc519fb72a6d3e5a3e8a0d806e1fdf2b1d32 /gcc/ada/debug.adb | |
| parent | cd38efa560f565cb02cba62fe919e591dc110b74 (diff) | |
| download | gcc-0c5dba7ff5ca748346488e651641e4b93eb53a17.zip gcc-0c5dba7ff5ca748346488e651641e4b93eb53a17.tar.gz gcc-0c5dba7ff5ca748346488e651641e4b93eb53a17.tar.bz2 | |
[multiple changes]
2013-10-10 Robert Dewar <dewar@adacore.com>
* gnatlink.adb: Minor reformatting.
2013-10-10 Yannick Moy <moy@adacore.com>
* debug.adb: Free flag d.E and change doc for flag d.K.
2013-10-10 Ed Schonberg <schonberg@adacore.com>
* sem_prag.adb (Check_Precondition_Postcondition): If the
pragma comes from an aspect spec, and the subprogram is a
library unit, treat as a ppc in a declarative part in ASIS mode,
so that expression in aspect is properly analyzed. In this case
there is no later point at which the aspect specification would
be examined.
2013-10-10 Bob Duff <duff@adacore.com>
* opt.ads: Minor comment fix.
2013-10-10 Vadim Godunko <godunko@adacore.com>
* a-coinho-shared.ads, a-coinho-shared.adb: New file.
* s-atocou.ads: Add procedure to initialize counter.
* s-atocou.adb: Likewise.
* s-atocou-builtin.adb: Likewise.
* s-atocou-x86.adb: Likewise.
* gcc-interface/Makefile.in: Select special version of
Indefinite_Holders package on platforms where atomic built-ins
are supported. Update tools target pairs for PikeOS.
From-SVN: r203344
Diffstat (limited to 'gcc/ada/debug.adb')
| -rw-r--r-- | gcc/ada/debug.adb | 12 |
1 files changed, 4 insertions, 8 deletions
diff --git a/gcc/ada/debug.adb b/gcc/ada/debug.adb index 0162479..8775af7 100644 --- a/gcc/ada/debug.adb +++ b/gcc/ada/debug.adb @@ -122,13 +122,13 @@ package body Debug is -- d.B -- d.C Generate concatenation call, do not generate inline code -- d.D SPARK strict mode - -- d.E Force SPARK mode for gnat2why + -- d.E -- d.F SPARK mode -- d.G Frame condition mode for gnat2why -- d.H Standard package only mode for gnat2why -- d.I Do not ignore enum representation clauses in CodePeer mode -- d.J Disable parallel SCIL generation mode - -- d.K SPARK detection only mode for gnat2why + -- d.K SPARK check mode for gnat2why -- d.L Depend on back end for limited types in if and case expressions -- d.M Relaxed RM semantics -- d.N Add node to all entities @@ -597,10 +597,6 @@ package body Debug is -- d.D SPARK strict mode. Interpret compiler permissions as strictly as -- possible in SPARK mode. - -- d.E Force SPARK mode for gnat2why. In this mode, errors are issued for - -- all violations of SPARK in user code, and warnings are issued for - -- constructs not yet implemented in gnat2why. - -- d.F SPARK mode. Generate AST in a form suitable for formal -- verification, as well as additional cross reference information in -- ALI files to compute effects of subprograms. Note that ALI files @@ -624,8 +620,8 @@ package body Debug is -- done in parallel to speed processing. This switch disables this -- behavior. - -- d.K SPARK detection only mode for gnat2why. In this mode, gnat2why - -- does not generate Why code. + -- d.K SPARK check mode for gnat2why. In this mode, gnat2why does not + -- generate Why code. -- d.L Normally the front end generates special expansion for conditional -- expressions of a limited type. This debug flag removes this special |