[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  <moy@adacore.com>

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 8c0708271dfad509e8bb00e42f0dc20e5e0c8306..b74910d2e1f01b66ce56babbd332492f0d8c66f7 100644 (file)
--- a/gcc/ada/ChangeLog
+++ b/gcc/ada/ChangeLog
@@ -1,3 +1,8 @@
+2019-07-09  Yannick Moy  <moy@adacore.com>
+
+       * freeze.adb (Build_Renamed_Body): Do not set body to inline in
+       GNATprove mode.
+
 2019-07-09  Yannick Moy  <moy@adacore.com>
 
        * exp_util.adb (Expand_Subtype_From_Expr): Still expand the type

diff --git a/gcc/ada/freeze.adb b/gcc/ada/freeze.adb
index 5b843f22519516c05e445b7d36fbf6095b469413..b29ff6705d790f41f4e9b29ba902a4c9d1c8e2bd 100644 (file)
--- 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;