[Ada] Correctly mark subprogram as not always inlined in GNATprove mode

gcc/ada/

	* inline.adb (Cannot_Inline): Add No_Info parameter to disable
	info message.
	* inline.ads (Cannot_Inline): When No_Info is set to True, do
	not issue info message in GNATprove mode, but still mark the
	subprogram as not always inlined.
	* sem_res.adb (Resolve_Call): Always call Cannot_Inline inside
	an assertion expression.

1 files changed, 14 insertions, 13 deletions

diff --git a/gcc/ada/inline.adb b/gcc/ada/inline.adb
index c24763a..bb4d97c 100644
--- a/gcc/ada/inline.adb
+++ b/gcc/ada/inline.adb
@@ -1945,10 +1945,11 @@ package body Inline is
    -------------------
 
    procedure Cannot_Inline
-     (Msg        : String;
-      N          : Node_Id;
-      Subp       : Entity_Id;
-      Is_Serious : Boolean := False)
+     (Msg           : String;
+      N             : Node_Id;
+      Subp          : Entity_Id;
+      Is_Serious    : Boolean := False;
+      Suppress_Info : Boolean := False)
    is
    begin
       --  In GNATprove mode, inlining is the technical means by which the
@@ -1971,7 +1972,7 @@ package body Inline is
             New_Msg (1 .. Len2) := "info: no contextual analysis of";
             New_Msg (Len2 + 1 .. Msg'Length + Len2 - Len1) :=
               Msg (Msg'First + Len1 .. Msg'Last);
-            Cannot_Inline (New_Msg, N, Subp, Is_Serious);
+            Cannot_Inline (New_Msg, N, Subp, Is_Serious, Suppress_Info);
             return;
          end;
       end if;
@@ -1992,14 +1993,14 @@ package body Inline is
          then
             null;
 
-         --  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.
+         --  In GNATprove mode, issue an info message when -gnatd_f is set and
+         --  Suppress_Info is False, 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);
 
-            if Debug_Flag_Underscore_F then
+            if Debug_Flag_Underscore_F and not Suppress_Info then
                Error_Msg_NE (Msg, N, Subp);
             end if;
 
@@ -2022,14 +2023,14 @@ package body Inline is
 
          Error_Msg_NE (Msg (Msg'First .. Msg'Last - 1), N, Subp);
 
-      --  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.
+      --  In GNATprove mode, issue an info message when -gnatd_f is set and
+      --  Suppress_Info is False, 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);
 
-         if Debug_Flag_Underscore_F then
+         if Debug_Flag_Underscore_F and not Suppress_Info then
             Error_Msg_NE (Msg, N, Subp);
          end if;