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

3 files changed, 25 insertions, 23 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;
 
diff --git a/gcc/ada/inline.ads b/gcc/ada/inline.ads
index 51eab9c..6790f15 100644
--- a/gcc/ada/inline.ads
+++ b/gcc/ada/inline.ads
@@ -154,15 +154,17 @@ package Inline is
    --  its treatment of the subprogram.
 
    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);
    --  This procedure is called if the node N, an instance of a call to
    --  subprogram Subp, cannot be inlined. Msg is the message to be issued,
    --  which ends with ? (it does not end with ?p?, this routine takes care of
-   --  the need to change ? to ?p?). The behavior of this routine depends on
-   --  the value of Back_End_Inlining:
+   --  the need to change ? to ?p?). Suppress_Info is set to True to prevent
+   --  issuing an info message in GNATprove mode. The behavior of this routine
+   --  depends on the value of Back_End_Inlining:
    --
    --    * If Back_End_Inlining is not set (ie. legacy frontend inlining model)
    --      then if Subp has a pragma Always_Inlined, then an error message is
diff --git a/gcc/ada/sem_res.adb b/gcc/ada/sem_res.adb
index ed744ea..659db86 100644
--- a/gcc/ada/sem_res.adb
+++ b/gcc/ada/sem_res.adb
@@ -7122,10 +7122,9 @@ package body Sem_Res is
             --  on expression functions.
 
             elsif In_Assertion_Expr /= 0 then
-               if Present (Body_Id) then
-                  Cannot_Inline
-                    ("cannot inline & (in assertion expression)?", N, Nam_UA);
-               end if;
+               Cannot_Inline
+                 ("cannot inline & (in assertion expression)?", N, Nam_UA,
+                  Suppress_Info => No (Body_Id));
 
             --  Calls cannot be inlined inside default expressions