sem_ch10.adb, [...]: Minor reformatting.

2014-07-29  Robert Dewar  <dewar@adacore.com>

	* sem_ch10.adb, debug.adb, sem_prag.adb, sem_res.adb, sem_ch6.adb:
	Minor reformatting.

From-SVN: r213183

6 files changed, 34 insertions, 12 deletions

diff --git a/gcc/ada/ChangeLog b/gcc/ada/ChangeLog
index 1aeabb2..78d81fd 100644
--- a/gcc/ada/ChangeLog
+++ b/gcc/ada/ChangeLog
@@ -1,3 +1,8 @@
+2014-07-29  Robert Dewar  <dewar@adacore.com>
+
+	* sem_ch10.adb, debug.adb, sem_prag.adb, sem_res.adb, sem_ch6.adb:
+	Minor reformatting.
+
 2014-07-29  Ed Schonberg  <schonberg@adacore.com>
 
 	* sem_ch6.adb (Analyze_Subprogram_Body_Helper): Build body to
diff --git a/gcc/ada/debug.adb b/gcc/ada/debug.adb
index 97277d6..d375205 100644
--- a/gcc/ada/debug.adb
+++ b/gcc/ada/debug.adb
@@ -541,8 +541,9 @@ package body Debug is
    --       to the backend. This is useful to locate skipped calls that must be
    --       inlined by the frontend.
 
-   --  d.k  Enable new semantics of frontend inlining.  This is useful to test
-   --       this new feature in all the platforms.
+   --  d.k  Enable new semantics of frontend inlining. This is useful to test
+   --       this new feature in all the platforms. What *is* this new semantics
+   --       which doesn't seem to be documented anywhere???
 
    --  d.l  Use Ada 95 semantics for limited function returns. This may be
    --       used to work around the incompatibility introduced by AI-318-2.
diff --git a/gcc/ada/sem_ch10.adb b/gcc/ada/sem_ch10.adb
index fac22c6..f0f0ba1 100644
--- a/gcc/ada/sem_ch10.adb
+++ b/gcc/ada/sem_ch10.adb
@@ -1196,8 +1196,16 @@ package body Sem_Ch10 is
 
       Set_Analyzed (N);
 
+      --  Call Check_Package_Body so that a body containing subprograms with
+      --  Inline_Always can be made available for front end inlining.
+
       if Nkind (Unit_Node) = N_Package_Declaration
         and then Get_Cunit_Unit_Number (N) /= Main_Unit
+
+        --  We don't need to do this if the Expander is not active, since there
+        --  is no code to inline. However an exception is that we do the call
+        --  in GNATprove mode, since the resulting inlining eases proofs.
+
         and then (Expander_Active or GNATprove_Mode)
       then
          declare
@@ -1209,6 +1217,7 @@ package body Sem_Ch10 is
             Save_Style_Check_Options (Options);
             Reset_Style_Check_Options;
             Opt.Warning_Mode := Suppress;
+
             Check_Package_Body_For_Inlining (N, Defining_Entity (Unit_Node));
 
             Reset_Style_Check_Options;
diff --git a/gcc/ada/sem_ch6.adb b/gcc/ada/sem_ch6.adb
index a9f2067..92e7998 100644
--- a/gcc/ada/sem_ch6.adb
+++ b/gcc/ada/sem_ch6.adb
@@ -3337,11 +3337,12 @@ package body Sem_Ch6 is
          return;
       end if;
 
-      --  Handle frontend inlining. There is no need to prepare us for inlining
-      --  if we will not generate the code.
+      --  Handle frontend inlining
 
-      --  However, in GNATprove_Mode we want to expand calls in place
-      --  whenever possible, even with expansion desabled.
+      --  Note: Normally we don't do any inlining if expansion is off, since
+      --  we won't generate code in any case. An exception arises in GNATprove
+      --  mode where we want to expand calls in place whenever possible, even
+      --  with expansion disabled since the inlining eases proofs.
 
       --  Old semantics
 
@@ -3355,7 +3356,7 @@ package body Sem_Ch6 is
             Build_Body_To_Inline (N, Spec_Id);
          end if;
 
-      --  New semantics
+      --  New semantics (enabled by debug flag gnatd.k for testing)
 
       elsif (Expander_Active or else GNATprove_Mode)
         and then Serious_Errors_Detected = 0
diff --git a/gcc/ada/sem_prag.adb b/gcc/ada/sem_prag.adb
index e2fa97e..c7967ca 100644
--- a/gcc/ada/sem_prag.adb
+++ b/gcc/ada/sem_prag.adb
@@ -15379,10 +15379,15 @@ package body Sem_Prag is
          when Pragma_Inline_Always =>
             GNAT_Pragma;
 
-            --  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. ???
+            --  Pragma always active unless in CodePeer mode. It is disabled
+            --  in CodePeer mode because inlining is not helpful, and enabling
+            --  if caused walk order issues.
+
+            --  Historical note: this pragma used to be disabled in GNATprove
+            --  mode as well, but that was odd since walk order shoult not be
+            --  an issue in that case. Furthermore, we now like to do as much
+            --  front-end inlining as possible in GNATprove mode since it makes
+            --  proving things easier.
 
             if not CodePeer_Mode then
                Process_Inline (Enabled);
diff --git a/gcc/ada/sem_res.adb b/gcc/ada/sem_res.adb
index 5e23d0a..221d15b 100644
--- a/gcc/ada/sem_res.adb
+++ b/gcc/ada/sem_res.adb
@@ -6125,7 +6125,8 @@ package body Sem_Res is
       Check_Elab_Call (N);
 
       --  In GNATprove_Mode expansion is disabled, but we want to inline
-      --  subprograms that are marked Inline_Always.
+      --  subprograms that are marked Inline_Always, since the inlining
+      --  is useful in making it easier to prove things about the inlined body.
 
       if GNATprove_Mode
         and then Nkind (Unit_Declaration_Node (Nam)) = N_Subprogram_Declaration