[Ada] Issue info message on inlined subprograms in GNATprove mode

Issue a positive message that inlining was performed in GNATprove mode,
when corresponding debug switch -gnatd_f is set.

2018-09-26  Yannick Moy  <moy@adacore.com>

gcc/ada/

	* errout.ads: Update comment for insertion character '?'.
	* inline.adb: Use simple insertion character '?' for GNATprove
	info messages.
	* sem_res.adb (Resolve_Call): Issue an info message on inlining
	in GNATprove mode.

From-SVN: r264633

diff --git a/gcc/ada/ChangeLog b/gcc/ada/ChangeLog
index 8a9d9e1db63bcadc3ccef4ea02bcc4b3d0be5ac2..f8281bde5439699006956605860fb88996a9d244 100644 (file)
--- a/gcc/ada/ChangeLog
+++ b/gcc/ada/ChangeLog
@@ -1,3 +1,11 @@
+2018-09-26  Yannick Moy  <moy@adacore.com>
+
+       * errout.ads: Update comment for insertion character '?'.
+       * inline.adb: Use simple insertion character '?' for GNATprove
+       info messages.
+       * sem_res.adb (Resolve_Call): Issue an info message on inlining
+       in GNATprove mode.
+
 2018-09-26  Ed Schonberg  <schonberg@adacore.com>
 
        * checks.adb (Apply_Type_Conversion_Checks): Do not generate a

diff --git a/gcc/ada/errout.ads b/gcc/ada/errout.ads
index f7807a1e0dcf8c2c8927c04f8a81504306a6a91b..e0525047eac0e5c76b197aa78c17b03c0e2c2f50 100644 (file)
--- a/gcc/ada/errout.ads
+++ b/gcc/ada/errout.ads
@@ -305,7 +305,9 @@ package Errout is
    --      Note: this usage is obsolete, use ?? ?*? ?$? ?x? ?X? to specify
    --      the string to be added when Warn_Doc_Switch is set to True. If this
    --      switch is True, then for simple ? messages it has no effect. This
-   --      simple form is to ease transition and will be removed later.
+   --      simple form is to ease transition and may be removed later except
+   --      for GNATprove-specific messages (info and warnings) which are not
+   --      subject to the same GNAT warning switches.
 
    --    Insertion character ?? (Two question marks: default warning)
    --      Like ?, but if the flag Warn_Doc_Switch is True, adds the string

diff --git a/gcc/ada/inline.adb b/gcc/ada/inline.adb
index 72991fad03e53075cd55ee899ca1c4250ee498bb..9dbc8ab8aaed7a6de9dae6ab78e0c103d7159f6c 100644 (file)
--- a/gcc/ada/inline.adb
+++ b/gcc/ada/inline.adb
@@ -1615,7 +1615,7 @@ package body Inline is
             Set_Is_Inlined_Always (Subp, False);
 
             if Debug_Flag_Underscore_F then
-               Error_Msg_NE (Msg & "p?", N, Subp);
+               Error_Msg_NE (Msg, N, Subp);
             end if;
 
          elsif Has_Pragma_Inline_Always (Subp) then
@@ -1645,7 +1645,7 @@ package body Inline is
          Set_Is_Inlined_Always (Subp, False);
 
          if Debug_Flag_Underscore_F then
-            Error_Msg_NE (Msg & "p?", N, Subp);
+            Error_Msg_NE (Msg, N, Subp);
          end if;
 
       else

diff --git a/gcc/ada/sem_res.adb b/gcc/ada/sem_res.adb
index 6a3dfb74c854e1e13273cab4867fc352f3deb064..800bf6929e5008bd9de2b54b9601bcec94be026c 100644 (file)
--- a/gcc/ada/sem_res.adb
+++ b/gcc/ada/sem_res.adb
@@ -6842,9 +6842,15 @@ package body Sem_Res is
                     ("cannot inline & (possible check on input parameters)?",
                      N, Nam_UA);
 
-               --  Otherwise, inline the call
+               --  Otherwise, inline the call, issuing an info message when
+               --  -gnatd_f is set.
 
                else
+                  if Debug_Flag_Underscore_F then
+                     Error_Msg_NE
+                       ("info: analyzing call to & in context?", N, Nam_UA);
+                  end if;
+
                   Expand_Inlined_Call (N, Nam_UA, Nam);
                end if;
             end if;