sem_ch6.adb (Analyze_Subprogram_Body_Helper): Build body to inline in GNATprove mode when subprogran is marked Inline_Always.

2014-07-29  Ed Schonberg  <schonberg@adacore.com>

	* sem_ch6.adb (Analyze_Subprogram_Body_Helper): Build body to
	inline in GNATprove mode when subprogran is marked Inline_Always.
	* sem_res.adb (Resolve_Call): Expand call in place in GNATProve
	mode if body to inline is available.
	* sem_prag.adb (Analyze_Pragma, case Inline_Always): Make pragma
	effective in GNATprove mode.
	* sem_ch10.adb (Analyze_Compilation_Unit): Call
	Check_Package_Body_For_Inlining in GNATprove mode, so that body
	containing subprograms with Inline_Always can be available before
	calls to them.

From-SVN: r213182
This commit is contained in:
Ed Schonberg 2014-07-29 13:40:27 +00:00 committed by Arnaud Charlet
parent 1773d80bb6
commit ecad37f3e1
5 changed files with 35 additions and 5 deletions

View File

@ -1,3 +1,16 @@
2014-07-29 Ed Schonberg <schonberg@adacore.com>
* sem_ch6.adb (Analyze_Subprogram_Body_Helper): Build body to
inline in GNATprove mode when subprogran is marked Inline_Always.
* sem_res.adb (Resolve_Call): Expand call in place in GNATProve
mode if body to inline is available.
* sem_prag.adb (Analyze_Pragma, case Inline_Always): Make pragma
effective in GNATprove mode.
* sem_ch10.adb (Analyze_Compilation_Unit): Call
Check_Package_Body_For_Inlining in GNATprove mode, so that body
containing subprograms with Inline_Always can be available before
calls to them.
2014-07-29 Ed Schonberg <schonberg@adacore.com>
* inline.ads, inline.adb, sem_ch10.adb: Rename Check_Body_For_Inlining

View File

@ -1198,7 +1198,7 @@ package body Sem_Ch10 is
if Nkind (Unit_Node) = N_Package_Declaration
and then Get_Cunit_Unit_Number (N) /= Main_Unit
and then Expander_Active
and then (Expander_Active or GNATprove_Mode)
then
declare
Save_Style_Check : constant Boolean := Style_Check;

View File

@ -3340,11 +3340,14 @@ package body Sem_Ch6 is
-- Handle frontend inlining. There is no need to prepare us for inlining
-- if we will not generate the code.
-- However, in GNATprove_Mode we want to expand calls in place
-- whenever possible, even with expansion desabled.
-- Old semantics
if not Debug_Flag_Dot_K then
if Present (Spec_Id)
and then Expander_Active
and then (Expander_Active or else GNATprove_Mode)
and then
(Has_Pragma_Inline_Always (Spec_Id)
or else (Has_Pragma_Inline (Spec_Id) and Front_End_Inlining))
@ -3354,7 +3357,7 @@ package body Sem_Ch6 is
-- New semantics
elsif Expander_Active
elsif (Expander_Active or else GNATprove_Mode)
and then Serious_Errors_Detected = 0
and then Present (Spec_Id)
and then Has_Pragma_Inline (Spec_Id)

View File

@ -15379,10 +15379,12 @@ package body Sem_Prag is
when Pragma_Inline_Always =>
GNAT_Pragma;
-- Pragma always active unless in CodePeer or GNATprove mode,
-- Pragma always active unless in CodePeer mode,
-- since this causes walk order issues.
-- This was disabled as well in GNATprove_Mode, even though
-- walk order should not be an issue here. ???
if not (CodePeer_Mode or GNATprove_Mode) then
if not CodePeer_Mode then
Process_Inline (Enabled);
end if;

View File

@ -37,6 +37,7 @@ with Exp_Tss; use Exp_Tss;
with Exp_Util; use Exp_Util;
with Fname; use Fname;
with Freeze; use Freeze;
with Inline; use Inline;
with Itypes; use Itypes;
with Lib; use Lib;
with Lib.Xref; use Lib.Xref;
@ -6122,6 +6123,17 @@ package body Sem_Res is
Eval_Call (N);
Check_Elab_Call (N);
-- In GNATprove_Mode expansion is disabled, but we want to inline
-- subprograms that are marked Inline_Always.
if GNATprove_Mode
and then Nkind (Unit_Declaration_Node (Nam)) = N_Subprogram_Declaration
and then Present (Body_To_Inline (Unit_Declaration_Node (Nam)))
then
Expand_Inlined_Call (N, Nam, Nam);
end if;
Warn_On_Overlapping_Actuals (Nam, N);
end Resolve_Call;