[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

gcc/ada/ChangeLog

 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
 	of static expressions in GNATprove_Mode.
 	* sem_ch3.adb (Analyze_Object_Declaration): Remove obsolete

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;