https://gcc.gnu.org/g:3dd180a818e74059c5de878d1557629093aa6748
commit r17-1307-g3dd180a818e74059c5de878d1557629093aa6748 Author: Johannes Kanig <[email protected]> Date: Wed Apr 29 08:33:13 2026 +0000 ada: GNATprove inlining/unrolling messages now controlled by two Booleans The GNATprove-related messages for inlining and unrolling are now controlled by two package-level Booleans instead of a Debug flag. gcc/ada/ChangeLog: * inline.ads: Introduce two new Boolean flags * inline.adb (Cannot_Inline): Modify the negative message into a warning, and use new flag * sem_res.adb (Resolve_Call): Use new flag to guard issue of msg * debug.adb: Debug flag now unused for GNATprove Diff: --- gcc/ada/debug.adb | 2 +- gcc/ada/inline.adb | 4 ++-- gcc/ada/inline.ads | 7 +++++++ gcc/ada/sem_res.adb | 2 +- 4 files changed, 11 insertions(+), 4 deletions(-) diff --git a/gcc/ada/debug.adb b/gcc/ada/debug.adb index 0f6622cbf825..bdb683bcf706 100644 --- a/gcc/ada/debug.adb +++ b/gcc/ada/debug.adb @@ -143,7 +143,7 @@ package body Debug is -- d_c CUDA compilation : compile for the host -- d_d CUDA compilation : compile for the device -- d_e Ignore entry calls and requeue statements for elaboration - -- d_f Issue info messages related to GNATprove usage + -- d_f -- d_g Disable large static aggregates -- d_h Disable the use of (perfect) hash functions for enumeration Value -- d_i Ignore activations and calls to instances for elaboration diff --git a/gcc/ada/inline.adb b/gcc/ada/inline.adb index 93ec997ce333..abaf997d9c28 100644 --- a/gcc/ada/inline.adb +++ b/gcc/ada/inline.adb @@ -2161,7 +2161,6 @@ package body Inline is Suppress_Info : Boolean := False) is Inline_Prefix : constant String := "cannot inline"; - function Starts_With (S, Prefix : String) return Boolean is (S (S'First .. S'First + Prefix'Length - 1) = Prefix); @@ -2207,7 +2206,8 @@ package body Inline is elsif GNATprove_Mode then Set_Is_Inlined_Always (Subp, False); - if Debug_Flag_Underscore_F and not Suppress_Info then + if GNATprove_Inline_Failure_Msg and not Suppress_Info + then Error_Msg_NE (Msg, N, Subp); end if; diff --git a/gcc/ada/inline.ads b/gcc/ada/inline.ads index bc21838b4321..fa90ea7c300a 100644 --- a/gcc/ada/inline.ads +++ b/gcc/ada/inline.ads @@ -50,6 +50,13 @@ with Warnsw; use Warnsw; package Inline is + GNATprove_Inline_Success_Msg : Boolean := False; + -- Emit info messages for successful contextual analysis in GNATprove mode + + GNATprove_Inline_Failure_Msg : Boolean := False; + -- Emit info messages when contextual analysis cannot be performed in + -- GNATprove mode. + -------------------------------- -- Generic Body Instantiation -- -------------------------------- diff --git a/gcc/ada/sem_res.adb b/gcc/ada/sem_res.adb index 9ea8edc52597..680a9d683b6c 100644 --- a/gcc/ada/sem_res.adb +++ b/gcc/ada/sem_res.adb @@ -7487,7 +7487,7 @@ package body Sem_Res is -- -gnatd_f is set. else - if Debug_Flag_Underscore_F then + if GNATprove_Inline_Success_Msg then Error_Msg_NE ("info: analyzing call to & in context?", N, Nam_UA); end if;
