sem_ch6.adb (Analyze_Subprogram_Body_Helper): Build body to inline in GNATprove mode...

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

diff --git a/gcc/ada/ChangeLog b/gcc/ada/ChangeLog
index 5a21a5cc62c6d572ae68decd8bfe7a0e1c4c92a4..1aeabb2a4f541466531bddd4017ee13b60d37b3e 100644 (file)
--- a/gcc/ada/ChangeLog
+++ b/gcc/ada/ChangeLog
@@ -1,3 +1,16 @@
+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

diff --git a/gcc/ada/sem_ch10.adb b/gcc/ada/sem_ch10.adb
index a8e0078c1f2f7044a152ff00eb708b0bf045bc1c..fac22c606e0fd042a067e3fb47425d8ac9a569c0 100644 (file)
--- 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 8caf19c49a6ff326f37603b57a2262d1f6cdd258..a9f206769d8a3e6abeb341700bad0be717155d93 100644 (file)
--- 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 f33f268732ad2deec1245e61d08889279ca30cb6..e2fa97e62293557c5b62d7ef7d6ebd3172e473d7 100644 (file)
--- 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 9f304eedb8b9b94f0c4c9b8ddd1cf155c6f937cc..5e23d0a0c20ec1a48b1bdcdd9a19c8d025d5f2b4 100644 (file)
--- 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;