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

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.

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.

From-SVN: r264629

diff --git a/gcc/ada/ChangeLog b/gcc/ada/ChangeLog
index 16855a7d23f3ce76b42dc2d30cedd27b38929459..0ba717d977ab5a1099bf9365227e4cb30fda8641 100644 (file)
--- a/gcc/ada/ChangeLog
+++ b/gcc/ada/ChangeLog
@@ -1,3 +1,10 @@
+2018-09-26  Yannick Moy  <moy@adacore.com>
+
+       * 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.
+
 2018-09-26  Javier Miranda  <miranda@adacore.com>
 
        * exp_disp.adb (Expand_Interface_Conversion): No displacement of

diff --git a/gcc/ada/debug.adb b/gcc/ada/debug.adb
index 95efedeb25b3171bafc3bf159aaa31ad31e5186c..65451a2c18a5f48f3fd9572a2f8cdd9c6cadc11b 100644 (file)
--- a/gcc/ada/debug.adb
+++ b/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.

diff --git a/gcc/ada/inline.adb b/gcc/ada/inline.adb
index 8f0b75d44a14f732182649ac47581a4684cd09e8..72991fad03e53075cd55ee899ca1c4250ee498bb 100644 (file)
--- a/gcc/ada/inline.adb
+++ b/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