diff options
| author | Arnaud Charlet <charlet@gcc.gnu.org> | 2014-07-30 13:01:18 +0200 |
|---|---|---|
| committer | Arnaud Charlet <charlet@gcc.gnu.org> | 2014-07-30 13:01:18 +0200 |
| commit | 93a87598b928f58f9e467bea8c718c5e2c91e498 (patch) | |
| tree | 3d747f395017502c088251df59226e37086a5feb /gcc/ada/debug.adb | |
| parent | 1399d355cb74c0de280637c1ce678df71f4adb38 (diff) | |
| download | gcc-93a87598b928f58f9e467bea8c718c5e2c91e498.zip gcc-93a87598b928f58f9e467bea8c718c5e2c91e498.tar.gz gcc-93a87598b928f58f9e467bea8c718c5e2c91e498.tar.bz2 | |
[multiple changes]
2014-07-30 Doug Rupp <rupp@adacore.com>
* adaint.c (__gnat_tmp_name) [__ANDROID__]: Default to putting
temp files in /cache directory unless overridden by TMPDIR.
2014-07-30 Jose Ruiz <ruiz@adacore.com>
* s-tassta.adb, s-tarest.adb (Initialize, Create_Task,
Create_Restricted_Task): Remove redundant check. Number_Of_CPUs returns
type CPU, so it can never be greater than CPU_Range'Last.
2014-07-30 Bob Duff <duff@adacore.com>
* s-taskin.ads: Minor comment fix.
2014-07-30 Thomas Quinot <quinot@adacore.com>
* g-socket.adb: Remove now useless WITH, USE, and USE TYPE
clauses.
2014-07-30 Yannick Moy <moy@adacore.com>
* debug.adb: Free debug flag dQ used for frontend inlining in
GNATprove mode..
* sem_ch6.adb (Analyze_Subprogram_Body_Helper): Remove test of
debug flag..
2014-07-30 Thomas Quinot <quinot@adacore.com>
* Make-generated.in: Remove generation of s-oscons.ads, only
generate the xoscons utility, in runtime-agnostic rules.
* gcc-interface/Makefile.in: Clean up rules. Remove VMS parts,
no longer supported.
From-SVN: r213250
Diffstat (limited to 'gcc/ada/debug.adb')
| -rw-r--r-- | gcc/ada/debug.adb | 9 |
1 files changed, 5 insertions, 4 deletions
diff --git a/gcc/ada/debug.adb b/gcc/ada/debug.adb index 1f7c8e2..b96ce833 100644 --- a/gcc/ada/debug.adb +++ b/gcc/ada/debug.adb @@ -80,7 +80,7 @@ package body Debug is -- dN No file name information in exception messages -- dO Output immediate error messages -- dP Do not check for controlled objects in preelaborable packages - -- dQ Enable inlining in GNATprove mode + -- dQ Enable inlining of bodies-without-decl in GNATprove mode -- dR Bypass check for correct version of s-rpc -- dS Never convert numbers to machine numbers in Sem_Eval -- dT Convert to machine numbers only for constant declarations @@ -438,9 +438,10 @@ package body Debug is -- in preelaborable packages, but this restriction is a huge pain, -- especially in the predefined library units. - -- dQ Enable inlining in GNATprove mode. Although expansion is not set in - -- GNATprove mode, inlining is useful for improving the precision of - -- formal verification. Under a debug flag until fully reliable. + -- dQ Enable inlining of bodies-without-decl in GNATprove mode. A decl is + -- created by the frontend so that the usual frontend inlining + -- mechanism can be used for formal verification. Under a debug flag + -- until fully reliable. -- dR Bypass the check for a proper version of s-rpc being present -- to use the -gnatz? switch. This allows debugging of the use |