diff options
| author | Yannick Moy <moy@adacore.com> | 2014-07-29 14:55:24 +0000 |
|---|---|---|
| committer | Arnaud Charlet <charlet@gcc.gnu.org> | 2014-07-29 16:55:24 +0200 |
| commit | 2d180af122bda9206c06441fee99f9adf873bdde (patch) | |
| tree | 28bb3481554fc9b101482e1edc13c60506976e79 /gcc/ada/debug.adb | |
| parent | 5ae243127908fa14634e086d2e55b8a996f95a2c (diff) | |
| download | gcc-2d180af122bda9206c06441fee99f9adf873bdde.zip gcc-2d180af122bda9206c06441fee99f9adf873bdde.tar.gz gcc-2d180af122bda9206c06441fee99f9adf873bdde.tar.bz2 | |
2014-07-29 Yannick Moy <moy@adacore.com>
* debug.adb Enable GNATprove inlining under debug flag -gnatdQ for now.
* inline.ads, inline.adb (Can_Be_Inlined_In_GNATprove_Mode): New
function to decide when a subprogram can be inlined in GNATprove mode.
(Check_And_Build_Body_To_Inline): Include GNATprove_Mode as a
condition for possible inlining.
* sem_ch10.adb (Analyze_Compilation_Unit): Remove special case
for Inline_Always in GNATprove mode.
* sem_ch6.adb (Analyze_Subprogram_Body_Helper): Build inlined
body for subprograms in GNATprove mode, under debug flag -gnatdQ.
* sem_prag.adb Minor change in comments.
* sem_res.adb (Resolve_Call): Only perform GNATprove inlining
inside subprograms marked as SPARK_Mode On.
* sinfo.ads: Minor typo fix.
From-SVN: r213205
Diffstat (limited to 'gcc/ada/debug.adb')
| -rw-r--r-- | gcc/ada/debug.adb | 6 |
1 files changed, 5 insertions, 1 deletions
diff --git a/gcc/ada/debug.adb b/gcc/ada/debug.adb index d375205..5e9c0da 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 + -- dQ Enable inlining 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,6 +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. + -- 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 |