[Ada] Improve messages for lack of inlining in GNATprove mode

[Arnaud Charlet]

Expression functions with a separate declarations should never be inlined
in GNATprove mode, hence no message should be issued for these. Correct a
problem in call resolution which lead to such a message. Also change the
message for lack of inlining in GNATprove mode, so that an info message is
issued instead of a warning.

Tested on x86_64-pc-linux-gnu, committed on trunk

2014-08-01  Yannick Moy  <m...@adacore.com>

        * inline.adb (Cannot_Inline): Issue info message instead of
        warning for subprograms not inlined in GNATprove mode.
        * sem_res.adb (Resolve_Call): Take body into account for deciding
        whether subprogram can be inlined in GNATprove mode or not.


Index: inline.adb
===================================================================
--- inline.adb  (revision 213437)
+++ inline.adb  (working copy)
@@ -1239,11 +1239,12 @@
         and then Msg (Msg'First .. Msg'First + 12) = "cannot inline"
       then
          declare
-            Len1 : constant Positive := 13;  --  "cannot inline"
-            Len2 : constant Positive := 25;  --  "no contextual analysis of"
+            Len1 : constant Positive := 13;  --  length of "cannot inline"
+            Len2 : constant Positive := 31;
+            --  lenth of "info: no contextual analysis of"
             New_Msg : String (1 .. Msg'Length + Len2 - Len1);
          begin
-            New_Msg (1 .. Len2) := "no contextual analysis of";
+            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);
Index: sem_res.adb
===================================================================
--- sem_res.adb (revision 213441)
+++ sem_res.adb (working copy)
@@ -6217,8 +6217,9 @@
          --  being inlined.
 
          declare
-            Nam_UA : constant Entity_Id := Ultimate_Alias (Nam);
-            Decl   : constant Node_Id   := Unit_Declaration_Node (Nam_UA);
+            Nam_UA  : constant Entity_Id := Ultimate_Alias (Nam);
+            Decl    : constant Node_Id   := Unit_Declaration_Node (Nam_UA);
+            Body_Id : constant Entity_Id := Corresponding_Body (Decl);
 
          begin
             --  If the subprogram is not eligible for inlining in GNATprove
@@ -6226,7 +6227,7 @@
 
             if Nkind (Decl) /= N_Subprogram_Declaration
               or else not Is_Inlined_Always (Nam_UA)
-              or else not Can_Be_Inlined_In_GNATprove_Mode (Nam_UA, Empty)
+              or else not Can_Be_Inlined_In_GNATprove_Mode (Nam_UA, Body_Id)
             then
                null;
 
@@ -6245,7 +6246,7 @@
                --  With the one-pass inlining technique, a call cannot be
                --  inlined if the corresponding body has not been seen yet.
 
-               if No (Corresponding_Body (Decl)) then
+               if No (Body_Id) then
                   Error_Msg_NE
                     ("?no contextual analysis of & (body not seen yet)",
                      N, Nam);