+2014-07-29 Robert Dewar <dewar@adacore.com>
+
+ * sem_ch10.adb, debug.adb, sem_prag.adb, sem_res.adb, sem_ch6.adb:
+ Minor reformatting.
+
2014-07-29 Ed Schonberg <schonberg@adacore.com>
* sem_ch6.adb (Analyze_Subprogram_Body_Helper): Build body to
-- to the backend. This is useful to locate skipped calls that must be
-- inlined by the frontend.
- -- d.k Enable new semantics of frontend inlining. This is useful to test
- -- this new feature in all the platforms.
+ -- d.k Enable new semantics of frontend inlining. This is useful to test
+ -- this new feature in all the platforms. What *is* this new semantics
+ -- which doesn't seem to be documented anywhere???
-- d.l Use Ada 95 semantics for limited function returns. This may be
-- used to work around the incompatibility introduced by AI-318-2.
Set_Analyzed (N);
+ -- Call Check_Package_Body so that a body containing subprograms with
+ -- Inline_Always can be made available for front end inlining.
+
if Nkind (Unit_Node) = N_Package_Declaration
and then Get_Cunit_Unit_Number (N) /= Main_Unit
+
+ -- We don't need to do this if the Expander is not active, since there
+ -- is no code to inline. However an exception is that we do the call
+ -- in GNATprove mode, since the resulting inlining eases proofs.
+
and then (Expander_Active or GNATprove_Mode)
then
declare
Save_Style_Check_Options (Options);
Reset_Style_Check_Options;
Opt.Warning_Mode := Suppress;
+
Check_Package_Body_For_Inlining (N, Defining_Entity (Unit_Node));
Reset_Style_Check_Options;
return;
end if;
- -- Handle frontend inlining. There is no need to prepare us for inlining
- -- if we will not generate the code.
+ -- Handle frontend inlining
- -- However, in GNATprove_Mode we want to expand calls in place
- -- whenever possible, even with expansion desabled.
+ -- Note: Normally we don't do any inlining if expansion is off, since
+ -- we won't generate code in any case. An exception arises in GNATprove
+ -- mode where we want to expand calls in place whenever possible, even
+ -- with expansion disabled since the inlining eases proofs.
-- Old semantics
Build_Body_To_Inline (N, Spec_Id);
end if;
- -- New semantics
+ -- New semantics (enabled by debug flag gnatd.k for testing)
elsif (Expander_Active or else GNATprove_Mode)
and then Serious_Errors_Detected = 0
when Pragma_Inline_Always =>
GNAT_Pragma;
- -- 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. ???
+ -- Pragma always active unless in CodePeer mode. It is disabled
+ -- in CodePeer mode because inlining is not helpful, and enabling
+ -- if caused walk order issues.
+
+ -- Historical note: this pragma used to be disabled in GNATprove
+ -- mode as well, but that was odd since walk order shoult not be
+ -- an issue in that case. Furthermore, we now like to do as much
+ -- front-end inlining as possible in GNATprove mode since it makes
+ -- proving things easier.
if not CodePeer_Mode then
Process_Inline (Enabled);
Check_Elab_Call (N);
-- In GNATprove_Mode expansion is disabled, but we want to inline
- -- subprograms that are marked Inline_Always.
+ -- subprograms that are marked Inline_Always, since the inlining
+ -- is useful in making it easier to prove things about the inlined body.
if GNATprove_Mode
and then Nkind (Unit_Declaration_Node (Nam)) = N_Subprogram_Declaration