[gcc r15-1136] ada: Add switch to disable expansion of assertions in CodePeer mode

[Marc Poulhi?s]

https://gcc.gnu.org/g:ba1b04fb59f555b1a641aa6e6a77cd0b902780dd

commit r15-1136-gba1b04fb59f555b1a641aa6e6a77cd0b902780dd
Author: Piotr Trojanek <trojanek@adacore.com>
Date:   Thu Apr 11 10:04:19 2024 +0200

    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.

Diff:
---
 gcc/ada/debug.adb    | 7 ++++++-
 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 18b4a5480b6..540db2a9942 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 55b5d565536..081d9435f4a 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).