Info messages about lack of inlining for analysis in GNATprove may be
confusing to users. They are now only issued when GNATprove is called
with switch --info, which it passes on to gnat2why with switch -gnatd_f.
There is no effect on compilation.
Tested on x86_64-pc-linux-gnu, committed on trunk
2018-09-26 Yannick Moy <m...@adacore.com>
gcc/ada/
* debug.adb: Add use for -gnatd_f switch.
* inline.adb (Cannot_Inline): Only issue info message for
failure to inline in GNATprove mode when switch -gnatd_f is
used.--- gcc/ada/debug.adb
+++ gcc/ada/debug.adb
@@ -150,7 +150,7 @@ package body Debug is
-- d_c
-- d_d
-- d_e Ignore entry calls and requeue statements for elaboration
- -- d_f
+ -- d_f Issue info messages related to GNATprove usage
-- d_g
-- d_h
-- d_i Ignore activations and calls to instances for elaboration
@@ -831,6 +831,11 @@ package body Debug is
-- control, conditional entry calls, timed entry calls, and requeue
-- statements in both the static and dynamic elaboration models.
+ -- d_f Issue info messages related to GNATprove usage to help users
+ -- understand analysis results. By default these are not issued as
+ -- beginners find them confusing. Set automatically by GNATprove when
+ -- switch --info is used.
+
-- d_i The compiler ignores calls and task activations when they target a
-- subprogram or task type defined in an external instance for both
-- the static and dynamic elaboration models.
--- gcc/ada/inline.adb
+++ gcc/ada/inline.adb
@@ -1607,13 +1607,16 @@ package body Inline is
then
null;
- -- In GNATprove mode, issue a warning, and indicate that the
- -- subprogram is not always inlined by setting flag Is_Inlined_Always
- -- to False.
+ -- In GNATprove mode, issue a warning when -gnatd_f is set, and
+ -- indicate that the subprogram is not always inlined by setting
+ -- flag Is_Inlined_Always to False.
elsif GNATprove_Mode then
Set_Is_Inlined_Always (Subp, False);
- Error_Msg_NE (Msg & "p?", N, Subp);
+
+ if Debug_Flag_Underscore_F then
+ Error_Msg_NE (Msg & "p?", N, Subp);
+ end if;
elsif Has_Pragma_Inline_Always (Subp) then
@@ -1634,12 +1637,16 @@ package body Inline is
Error_Msg_NE (Msg (Msg'First .. Msg'Last - 1), N, Subp);
- -- In GNATprove mode, issue a warning, and indicate that the subprogram
- -- is not always inlined by setting flag Is_Inlined_Always to False.
+ -- In GNATprove mode, issue a warning when -gnatd_f is set, and
+ -- indicate that the subprogram is not always inlined by setting
+ -- flag Is_Inlined_Always to False.
elsif GNATprove_Mode then
Set_Is_Inlined_Always (Subp, False);
- Error_Msg_NE (Msg & "p?", N, Subp);
+
+ if Debug_Flag_Underscore_F then
+ Error_Msg_NE (Msg & "p?", N, Subp);
+ end if;
else
