[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

diff --git a/gcc/ada/ChangeLog b/gcc/ada/ChangeLog
index f174a297681548db422d2d6966ca20d5cfa841b7..88c0e79103d0eb19079925bd3a069cf9d8daac97 100644 (file)
--- 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 a91380f7425252a99f14d0c09326ba7a402f5327..235951ebca3229f8b82466819e3a80f92a8221d1 100644 (file)
--- 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 d5db0f6a5a5b72e4749b84692fa0de09d6d337a3..0483f8f31f15c3aa7b9c4846085db57100b01a04 100644 (file)
--- 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 6434159b4376fcfe3f92754eaa9ec10896a79344..b9531c6c0687d8b1ad020550945202d90deb4e62 100644 (file)
--- 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 2faed4c7a9e0be6a9085dd72e4f4ee7f2e2906e5..3c783764b5d196d9338bda7cd4aa6083d755ebab 100644 (file)
--- 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 dd7aedd1e8f70d0967e4430f6245efc8fa3c5eee..2d5766e27b1e64d6f2f253b5db17588e9df41d73 100644 (file)
--- 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);