From 39521a94f844f6c6462b4b7849e7f1e2780be6fa Mon Sep 17 00:00:00 2001 From: Arnaud Charlet Date: Fri, 1 Aug 2014 12:06:44 +0200 Subject: [multiple changes] 2014-08-01 Yannick Moy * 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 * 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 --- gcc/ada/ChangeLog | 15 +++++++++++++++ gcc/ada/exp_util.adb | 14 +++++++------- gcc/ada/exp_util.ads | 2 +- gcc/ada/inline.adb | 7 ++++--- gcc/ada/sem_ch12.adb | 7 ++++++- gcc/ada/sem_res.adb | 9 +++++---- 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 + + * 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 + + * 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 * 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); -- cgit v1.1