In GNATprove mode, subprograms with a body to inline should have been
filtered in Analyze_Subprogram_Body_Helper to match the conditions for
inlining subprograms in GNATprove. Prevent a call to Set_Body_To_Inline
in GNATprove mode that did not go through this filtering.
There is no impact on compilation.
Tested on x86_64-pc-linux-gnu, committed on trunk
2019-07-09 Yannick Moy <m...@adacore.com>
gcc/ada/
* freeze.adb (Build_Renamed_Body): Do not set body to inline in
GNATprove mode.--- gcc/ada/freeze.adb
+++ gcc/ada/freeze.adb
@@ -407,11 +407,14 @@ package body Freeze is
-- calls to the renamed entity. The body must be generated in any case
-- for calls that may appear elsewhere. This is not done in the case
-- where the subprogram is an instantiation because the actual proper
- -- body has not been built yet.
+ -- body has not been built yet. This is also not done in GNATprove mode
+ -- as we need to check other conditions for creating a body to inline
+ -- in that case, which are controlled in Analyze_Subprogram_Body_Helper.
if Ekind_In (Old_S, E_Function, E_Procedure)
and then Nkind (Decl) = N_Subprogram_Declaration
and then not Is_Generic_Instance (Old_S)
+ and then not GNATprove_Mode
then
Set_Body_To_Inline (Decl, Old_S);
end if;
