sem_ch6.adb (Analyze_Subprogram_Body_Helper): Build body to inline in GNATprove mode when subprogran is marked Inline_Always.

2014-07-29  Ed Schonberg  <schonberg@adacore.com>

	* sem_ch6.adb (Analyze_Subprogram_Body_Helper): Build body to
	inline in GNATprove mode when subprogran is marked Inline_Always.
	* sem_res.adb (Resolve_Call): Expand call in place in GNATProve
	mode if body to inline is available.
	* sem_prag.adb (Analyze_Pragma, case Inline_Always): Make pragma
	effective in GNATprove mode.
	* sem_ch10.adb (Analyze_Compilation_Unit): Call
	Check_Package_Body_For_Inlining in GNATprove mode, so that body
	containing subprograms with Inline_Always can be available before
	calls to them.

From-SVN: r213182

5 files changed, 35 insertions, 5 deletions

diff --git a/gcc/ada/ChangeLog b/gcc/ada/ChangeLog
index 5a21a5c..1aeabb2 100644
--- a/gcc/ada/ChangeLog
+++ b/gcc/ada/ChangeLog
@@ -1,5 +1,18 @@
 2014-07-29  Ed Schonberg  <schonberg@adacore.com>
 
+	* sem_ch6.adb (Analyze_Subprogram_Body_Helper): Build body to
+	inline in GNATprove mode when subprogran is marked Inline_Always.
+	* sem_res.adb (Resolve_Call): Expand call in place in GNATProve
+	mode if body to inline is available.
+	* sem_prag.adb (Analyze_Pragma, case Inline_Always): Make pragma
+	effective in GNATprove mode.
+	* sem_ch10.adb (Analyze_Compilation_Unit): Call
+	Check_Package_Body_For_Inlining in GNATprove mode, so that body
+	containing subprograms with Inline_Always can be available before
+	calls to them.
+
+2014-07-29  Ed Schonberg  <schonberg@adacore.com>
+
 	* inline.ads, inline.adb, sem_ch10.adb: Rename Check_Body_For_Inlining
 	to Check_Package_Body_For_Inlining, to prevent confusion with other
 	inlining subprograms.
diff --git a/gcc/ada/sem_ch10.adb b/gcc/ada/sem_ch10.adb
index a8e0078..fac22c6 100644
--- a/gcc/ada/sem_ch10.adb
+++ b/gcc/ada/sem_ch10.adb
@@ -1198,7 +1198,7 @@ package body Sem_Ch10 is
 
       if Nkind (Unit_Node) = N_Package_Declaration
         and then Get_Cunit_Unit_Number (N) /= Main_Unit
-        and then Expander_Active
+        and then (Expander_Active or GNATprove_Mode)
       then
          declare
             Save_Style_Check : constant Boolean := Style_Check;
diff --git a/gcc/ada/sem_ch6.adb b/gcc/ada/sem_ch6.adb
index 8caf19c..a9f2067 100644
--- a/gcc/ada/sem_ch6.adb
+++ b/gcc/ada/sem_ch6.adb
@@ -3340,11 +3340,14 @@ package body Sem_Ch6 is
       --  Handle frontend inlining. There is no need to prepare us for inlining
       --  if we will not generate the code.
 
+      --  However, in GNATprove_Mode we want to expand calls in place
+      --  whenever possible, even with expansion desabled.
+
       --  Old semantics
 
       if not Debug_Flag_Dot_K then
          if Present (Spec_Id)
-           and then Expander_Active
+           and then (Expander_Active or else GNATprove_Mode)
            and then
              (Has_Pragma_Inline_Always (Spec_Id)
                or else (Has_Pragma_Inline (Spec_Id) and Front_End_Inlining))
@@ -3354,7 +3357,7 @@ package body Sem_Ch6 is
 
       --  New semantics
 
-      elsif Expander_Active
+      elsif (Expander_Active or else GNATprove_Mode)
         and then Serious_Errors_Detected = 0
         and then Present (Spec_Id)
         and then Has_Pragma_Inline (Spec_Id)
diff --git a/gcc/ada/sem_prag.adb b/gcc/ada/sem_prag.adb
index f33f268..e2fa97e 100644
--- a/gcc/ada/sem_prag.adb
+++ b/gcc/ada/sem_prag.adb
@@ -15379,10 +15379,12 @@ package body Sem_Prag is
          when Pragma_Inline_Always =>
             GNAT_Pragma;
 
-            --  Pragma always active unless in CodePeer or GNATprove mode,
+            --  Pragma always active unless in CodePeer mode,
             --  since this causes walk order issues.
+            --  This was disabled as well in GNATprove_Mode, even though
+            --  walk order should not be an issue here. ???
 
-            if not (CodePeer_Mode or GNATprove_Mode) then
+            if not CodePeer_Mode then
                Process_Inline (Enabled);
             end if;
 
diff --git a/gcc/ada/sem_res.adb b/gcc/ada/sem_res.adb
index 9f304eed..5e23d0a 100644
--- a/gcc/ada/sem_res.adb
+++ b/gcc/ada/sem_res.adb
@@ -37,6 +37,7 @@ with Exp_Tss;  use Exp_Tss;
 with Exp_Util; use Exp_Util;
 with Fname;    use Fname;
 with Freeze;   use Freeze;
+with Inline;   use Inline;
 with Itypes;   use Itypes;
 with Lib;      use Lib;
 with Lib.Xref; use Lib.Xref;
@@ -6122,6 +6123,17 @@ package body Sem_Res is
 
       Eval_Call (N);
       Check_Elab_Call (N);
+
+      --  In GNATprove_Mode expansion is disabled, but we want to inline
+      --  subprograms that are marked Inline_Always.
+
+      if GNATprove_Mode
+        and then Nkind (Unit_Declaration_Node (Nam)) = N_Subprogram_Declaration
+        and then Present (Body_To_Inline (Unit_Declaration_Node (Nam)))
+      then
+         Expand_Inlined_Call (N, Nam, Nam);
+      end if;
+
       Warn_On_Overlapping_Actuals (Nam, N);
    end Resolve_Call;