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