diff options
| author | Arnaud Charlet <charlet@gcc.gnu.org> | 2014-07-30 15:54:18 +0200 |
|---|---|---|
| committer | Arnaud Charlet <charlet@gcc.gnu.org> | 2014-07-30 15:54:18 +0200 |
| commit | 2178830b048787f68c0b8b7c3dd3d26580a795aa (patch) | |
| tree | 4d659dd4ed85f83c6aebe912ce1e774a2e95d1f2 /gcc/ada/debug.adb | |
| parent | d3e16619ae38fba5a464064046114a6638d1816f (diff) | |
| download | gcc-2178830b048787f68c0b8b7c3dd3d26580a795aa.zip gcc-2178830b048787f68c0b8b7c3dd3d26580a795aa.tar.gz gcc-2178830b048787f68c0b8b7c3dd3d26580a795aa.tar.bz2 | |
[multiple changes]
2014-07-30 Pat Rogers <rogers@adacore.com>
* gnat_rm.texi: Minor word error.
2014-07-30 Ed Schonberg <schonberg@adacore.com>
* exp_prag.adb (Expand_Old): Insert declarationss of temporaries
created to capture the value of the prefix of 'Old at the
beginning of the current declarative part, to prevent data flow
anomalies in the postcondition procedure that will follow.
2014-07-30 Yannick Moy <moy@adacore.com>
* debug.adb: Retire debug flag -gnatdQ.
* inline.adb (Can_Be_Inlined_In_GNATprove_Mode): Check SPARK_Mode
on decl, not on body. Ignore predicate functions.
* sem_ch6.adb (Analyze_Subprogram_Body_Helper): Remove use of
debug flag -gnatdQ. Correctly analyze SPARK_Mode on decl and
body when generating a decl for a body on which SPARK_Mode aspect
is given.
* sem_prag.adb (Analyze_Pragma|SPARK_Mode): Reorder tests for
attaching pragma to entity, to account for declaration not coming
from source.
* sem_res.adb (Resolve_Call): Issue warning and flag subprogram
as not always inlined in GNATprove mode, when called in an
assertion context.
From-SVN: r213271
Diffstat (limited to 'gcc/ada/debug.adb')
| -rw-r--r-- | gcc/ada/debug.adb | 7 |
1 files changed, 1 insertions, 6 deletions
diff --git a/gcc/ada/debug.adb b/gcc/ada/debug.adb index a93af0f..64162ef 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 of bodies-without-decl in GNATprove mode + -- dQ -- 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,11 +438,6 @@ package body Debug is -- in preelaborable packages, but this restriction is a huge pain, -- especially in the predefined library units. - -- 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 -- of stubs generation without needing to have GLADE (or some |