From: Johannes Kanig <[email protected]>
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
Tested on x86_64-pc-linux-gnu, committed on master.
---
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 0f6622cbf82..bdb683bcf70 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 93ec997ce33..abaf997d9c2 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 bc21838b432..fa90ea7c300 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 9ea8edc5259..680a9d683b6 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;
--
2.53.0
