diff options
| author | Piotr Trojanek <trojanek@adacore.com> | 2024-04-11 10:04:19 +0200 |
|---|---|---|
| committer | Marc Poulhiès <poulhies@adacore.com> | 2024-06-10 11:03:58 +0200 |
| commit | ba1b04fb59f555b1a641aa6e6a77cd0b902780dd (patch) | |
| tree | 7734a3c1434bf53534e52cefee7215859ff1e750 /gcc | |
| parent | 8ce93cc22e06639ff82d2ec9e75da1f998dc70ad (diff) | |
| download | gcc-ba1b04fb59f555b1a641aa6e6a77cd0b902780dd.zip gcc-ba1b04fb59f555b1a641aa6e6a77cd0b902780dd.tar.gz gcc-ba1b04fb59f555b1a641aa6e6a77cd0b902780dd.tar.bz2 | |
ada: Add switch to disable expansion of assertions in CodePeer mode
A new debug switch -gnatd_k is added, which has only effect in CodePeer
mode. When enabled, assertion expressions are no longer expanded (which
is the default in the CodePeer mode); instead, their expansion needs to
be explicitly enabled by pragma Assertion_Policy.
gcc/ada/
* debug.adb (d_k): Use first available debug switch.
* gnat1drv.adb (Adjust_Global_Switches): If new debug switch is
active then don't expand assertion expressions by default.
Diffstat (limited to 'gcc')
| -rw-r--r-- | gcc/ada/debug.adb | 7 | ||||
| -rw-r--r-- | gcc/ada/gnat1drv.adb | 8 |
2 files changed, 12 insertions, 3 deletions
diff --git a/gcc/ada/debug.adb b/gcc/ada/debug.adb index 18b4a54..540db2a 100644 --- a/gcc/ada/debug.adb +++ b/gcc/ada/debug.adb @@ -148,7 +148,7 @@ package body Debug is -- d_h Disable the use of (perfect) hash functions for enumeration Value -- d_i Ignore activations and calls to instances for elaboration -- d_j Read JSON files and populate Repinfo tables (opposite of -gnatRjs) - -- d_k + -- d_k In CodePeer mode disable expansion of assertion checks -- d_l -- d_m -- d_n @@ -990,6 +990,11 @@ package body Debug is -- compilation session if -gnatRjs was passed, in order to populate -- the internal tables of the Repinfo unit from them. + -- d_k In CodePeer mode assertion expressions are expanded by default + -- (regardless of the -gnata compiler switch); when this switch is + -- enabled, expansion of assertion expressions is controlled by + -- pragma Assertion_Policy. + -- d_p The compiler ignores calls to subprograms which verify the run-time -- semantics of invariants and postconditions in both the static and -- dynamic elaboration models. diff --git a/gcc/ada/gnat1drv.adb b/gcc/ada/gnat1drv.adb index 55b5d56..081d943 100644 --- a/gcc/ada/gnat1drv.adb +++ b/gcc/ada/gnat1drv.adb @@ -357,9 +357,13 @@ procedure Gnat1drv is Generate_SCIL := True; - -- Enable assertions, since they give CodePeer valuable extra info + -- Enable assertions, since they give CodePeer valuable extra info; + -- however, when switch -gnatd_k is active, then keep assertions + -- disabled by default and only enable them when explicitly + -- requested by pragma Assertion_Policy, just like in ordinary + -- compilation. - Assertions_Enabled := True; + Assertions_Enabled := not Debug_Flag_Underscore_K; -- Set normal RM validity checking and checking of copies (to catch -- e.g. wrong values used in unchecked conversions). |