From: Yannick Moy Date: Tue, 9 Jul 2019 07:54:00 +0000 (+0000) Subject: [Ada] Prevent inconsistent state for inlining in GNATprove X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=554a9844f74932d2c6e9a690d04bfd96b361055b;p=gcc.git [Ada] Prevent inconsistent state for inlining in GNATprove 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. 2019-07-09 Yannick Moy gcc/ada/ * freeze.adb (Build_Renamed_Body): Do not set body to inline in GNATprove mode. From-SVN: r273274 --- diff --git a/gcc/ada/ChangeLog b/gcc/ada/ChangeLog index 8c0708271df..b74910d2e1f 100644 --- a/gcc/ada/ChangeLog +++ b/gcc/ada/ChangeLog @@ -1,3 +1,8 @@ +2019-07-09 Yannick Moy + + * freeze.adb (Build_Renamed_Body): Do not set body to inline in + GNATprove mode. + 2019-07-09 Yannick Moy * exp_util.adb (Expand_Subtype_From_Expr): Still expand the type diff --git a/gcc/ada/freeze.adb b/gcc/ada/freeze.adb index 5b843f22519..b29ff6705d7 100644 --- a/gcc/ada/freeze.adb +++ b/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;