diff mbox series

[Ada] Do not issue by default info messages for inlining in GNATprove

Message ID 20180926092538.GA126159@adacore.com
State New
Headers show
Series [Ada] Do not issue by default info messages for inlining in GNATprove | expand

Commit Message

Pierre-Marie de Rodat Sept. 26, 2018, 9:25 a.m. UTC 
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  <moy@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.
diff mbox series

Patch

--- 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