2014-07-29 Yannick Moy <moy@adacore.com>

	* debug.adb Enable GNATprove inlining under debug flag -gnatdQ for now.
	* inline.ads, inline.adb (Can_Be_Inlined_In_GNATprove_Mode): New
	function to decide when a subprogram can be inlined in GNATprove mode.
	(Check_And_Build_Body_To_Inline): Include GNATprove_Mode as a
	condition for possible inlining.
	* sem_ch10.adb (Analyze_Compilation_Unit): Remove special case
	for Inline_Always in GNATprove mode.
	* sem_ch6.adb (Analyze_Subprogram_Body_Helper): Build inlined
	body for subprograms in GNATprove mode, under debug flag -gnatdQ.
	* sem_prag.adb Minor change in comments.
	* sem_res.adb (Resolve_Call): Only perform GNATprove inlining
	inside subprograms marked as SPARK_Mode On.
	* sinfo.ads: Minor typo fix.

From-SVN: r213205

1 files changed, 14 insertions, 5 deletions

diff --git a/gcc/ada/inline.ads b/gcc/ada/inline.ads
index e8b1c01..a4a9527 100644
--- a/gcc/ada/inline.ads
+++ b/gcc/ada/inline.ads
@@ -23,7 +23,7 @@
 --                                                                          --
 ------------------------------------------------------------------------------
 
---  This module handles three kinds of inlining activity:
+--  This module handles four kinds of inlining activity:
 
 --  a) Instantiation of generic bodies. This is done unconditionally, after
 --  analysis and expansion of the main unit.
@@ -37,10 +37,12 @@
 
 --  c) Front-end inlining for Inline_Always subprograms. This is primarily an
 --  expansion activity that is performed for performance reasons, and when the
---  target does not use the gcc backend. Inline_Always can also be used in the
---  context of GNATprove, to perform source transformations to simplify proof
---  obligations. The machinery used in both cases is similar, but there are
---  fewer restrictions on the source of subprograms in the latter case.
+--  target does not use the gcc backend.
+
+--  d) Front-end inlining for GNATprove, to perform source transformations
+--  to simplify formal verification. The machinery used is the same than for
+--  Inline_Always subprograms, but there are fewer restrictions on the source
+--  of subprograms.
 
 with Alloc;
 with Opt;    use Opt;
@@ -233,4 +235,11 @@ package Inline is
    --  If an instantiation appears in unreachable code, delete the pending
    --  body instance.
 
+   function Can_Be_Inlined_In_GNATprove_Mode
+     (Spec_Id : Entity_Id;
+      Body_Id : Entity_Id) return Boolean;
+   --  Returns True if the subprogram identified by Spec_Id (possibly Empty)
+   --  and Body_Id (not Empty) can be inlined in GNATprove mode. GNATprove
+   --  relies on this to adapt its treatment of the subprogram.
+
 end Inline;