[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
This commit is contained in:
Arnaud Charlet 2014-08-01 12:06:44 +02:00
parent b98a872b22
commit 39521a94f8
6 changed files with 38 additions and 16 deletions

View File

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

View File

@ -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 --

View File

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

View File

@ -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);

View File

@ -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

View File

@ -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);