[multiple changes]

2014-08-01  Yannick Moy  <moy@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.

2014-08-01  Claire Dross  <dross@adacore.com>

	* exp_util.ads (Get_First_Parent_With_Ext_Axioms_For_Entity): Renaming
	of Get_First_Parent_With_External_Axiomatization_For_Entity for
	shorter.
	* sem_ch12.adb (Analyze_Associations): Only call Build_Wrapper
	for parameters of packages with external axiomatization.

From-SVN: r213443

6 files changed, 38 insertions, 16 deletions

diff --git a/gcc/ada/ChangeLog b/gcc/ada/ChangeLog
index f174a29..88c0e79 100644
--- a/gcc/ada/ChangeLog
+++ b/gcc/ada/ChangeLog
@@ -1,3 +1,18 @@
+2014-08-01  Yannick Moy  <moy@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.
+
+2014-08-01  Claire Dross  <dross@adacore.com>
+
+	* exp_util.ads (Get_First_Parent_With_Ext_Axioms_For_Entity): Renaming
+	of Get_First_Parent_With_External_Axiomatization_For_Entity for
+	shorter.
+	* sem_ch12.adb (Analyze_Associations): Only call Build_Wrapper
+	for parameters of packages with external axiomatization.
+
 2014-08-01  Robert Dewar  <dewar@adacore.com>
 
 	* sem_res.adb: Minor comment addition.
diff --git a/gcc/ada/exp_util.adb b/gcc/ada/exp_util.adb
index a91380f..235951eb 100644
--- a/gcc/ada/exp_util.adb
+++ b/gcc/ada/exp_util.adb
@@ -3228,11 +3228,11 @@ package body Exp_Util is
       end;
    end Get_Current_Value_Condition;
 
-   --------------------------------------------------------------
-   -- Get_First_Parent_With_External_Axiomatization_For_Entity --
-   --------------------------------------------------------------
+   -------------------------------------------------
+   -- Get_First_Parent_With_Ext_Axioms_For_Entity --
+   -------------------------------------------------
 
-   function Get_First_Parent_With_External_Axiomatization_For_Entity
+   function Get_First_Parent_With_Ext_Axioms_For_Entity
      (E : Entity_Id) return Entity_Id is
 
       Decl : Node_Id;
@@ -3259,13 +3259,13 @@ package body Exp_Util is
       elsif Ekind (E) = E_Package
         and then Present (Generic_Parent (Decl))
       then
-         return Get_First_Parent_With_External_Axiomatization_For_Entity
+         return Get_First_Parent_With_Ext_Axioms_For_Entity
            (Generic_Parent (Decl));
 
          --  Otherwise, look at E's scope instead if present
 
       elsif Present (Scope (E)) then
-         return Get_First_Parent_With_External_Axiomatization_For_Entity
+         return Get_First_Parent_With_Ext_Axioms_For_Entity
              (Scope (E));
 
          --  Else there is no such axiomatized package
@@ -3273,7 +3273,7 @@ package body Exp_Util is
       else
          return Empty;
       end if;
-   end Get_First_Parent_With_External_Axiomatization_For_Entity;
+   end Get_First_Parent_With_Ext_Axioms_For_Entity;
 
    ---------------------
    -- Get_Stream_Size --
diff --git a/gcc/ada/exp_util.ads b/gcc/ada/exp_util.ads
index d5db0f6..0483f8f 100644
--- a/gcc/ada/exp_util.ads
+++ b/gcc/ada/exp_util.ads
@@ -525,7 +525,7 @@ package Exp_Util is
    --  N_Op_Eq), or to determine the result of some other test in other cases
    --  (e.g. no access check required if N_Op_Ne Null).
 
-   function Get_First_Parent_With_External_Axiomatization_For_Entity
+   function Get_First_Parent_With_Ext_Axioms_For_Entity
      (E : Entity_Id) return Entity_Id;
    --  Returns the package entity with an external axiomatization containing E,
    --  if any, or Empty if none.
diff --git a/gcc/ada/inline.adb b/gcc/ada/inline.adb
index 6434159..b9531c6 100644
--- a/gcc/ada/inline.adb
+++ b/gcc/ada/inline.adb
@@ -1239,11 +1239,12 @@ package body Inline is
         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);
diff --git a/gcc/ada/sem_ch12.adb b/gcc/ada/sem_ch12.adb
index 2faed4c..3c78376 100644
--- a/gcc/ada/sem_ch12.adb
+++ b/gcc/ada/sem_ch12.adb
@@ -30,6 +30,7 @@ with Elists;   use Elists;
 with Errout;   use Errout;
 with Expander; use Expander;
 with Exp_Disp; use Exp_Disp;
+with Exp_Util; use Exp_Util;
 with Fname;    use Fname;
 with Fname.UF; use Fname.UF;
 with Freeze;   use Freeze;
@@ -1669,7 +1670,11 @@ package body Sem_Ch12 is
 
                   else
                      if GNATprove_Mode
-                        and then Ekind (Defining_Entity (Analyzed_Formal))
+                       and then
+                         Present
+                           (Get_First_Parent_With_Ext_Axioms_For_Entity
+                              (Defining_Entity (Analyzed_Formal)))
+                       and then Ekind (Defining_Entity (Analyzed_Formal))
                           = E_Function
                      then
 
diff --git a/gcc/ada/sem_res.adb b/gcc/ada/sem_res.adb
index dd7aedd..2d5766e 100644
--- a/gcc/ada/sem_res.adb
+++ b/gcc/ada/sem_res.adb
@@ -6217,8 +6217,9 @@ package body Sem_Res is
          --  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 @@ package body Sem_Res is
 
             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 @@ package body Sem_Res is
                --  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);