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

	* gnat1drv.adb (Adjust_Global_Switches): Set
	Ineffective_Inline_Warnings to True in GNATprove mode.
	* inline.adb (Cannot_Inline): Prepare new semantics for GNATprove
	mode of inlining.
	* opt.ads (Ineffective_Inline_Warnings): Add comment that
	describes use in GNATprove mode.
	* sem_prag.adb (Analyze_Pragma|SPARK_Mode): Ignore
	pragma when applied to the special body created for inlining.



git-svn-id: svn+ssh://gcc.gnu.org/svn/gcc/trunk@213245 138bc75d-0d04-0410-961f-82ee72b054a4

5 files changed, 33 insertions, 7 deletions

diff --git a/gcc/ada/ChangeLog b/gcc/ada/ChangeLog
index 463f3704dc2..e9542062c92 100644
--- a/gcc/ada/ChangeLog
+++ b/gcc/ada/ChangeLog
@@ -1,3 +1,14 @@
+2014-07-30  Yannick Moy  <moy@adacore.com>
+
+	* gnat1drv.adb (Adjust_Global_Switches): Set
+	Ineffective_Inline_Warnings to True in GNATprove mode.
+	* inline.adb (Cannot_Inline): Prepare new semantics for GNATprove
+	mode of inlining.
+	* opt.ads (Ineffective_Inline_Warnings): Add comment that
+	describes use in GNATprove mode.
+	* sem_prag.adb (Analyze_Pragma|SPARK_Mode): Ignore
+	pragma when applied to the special body created for inlining.
+
 2014-07-30  Robert Dewar  <dewar@adacore.com>
 
 	* inline.adb, exp_ch4.adb, sinput.adb, sem_ch6.adb, sem_ch13.adb:
diff --git a/gcc/ada/gnat1drv.adb b/gcc/ada/gnat1drv.adb
index 756961e3d2d..9a61d484d56 100644
--- a/gcc/ada/gnat1drv.adb
+++ b/gcc/ada/gnat1drv.adb
@@ -334,6 +334,12 @@ procedure Gnat1drv is
          Front_End_Inlining := False;
          Inline_Active      := False;
 
+         --  Issue warnings for failure to inline subprograms, as otherwise
+         --  expected in GNATprove mode for the local subprograms without
+         --  contracts.
+
+         Ineffective_Inline_Warnings := True;
+
          --  Disable front-end optimizations, to keep the tree as close to the
          --  source code as possible, and also to avoid inconsistencies between
          --  trees when using different optimization switches.
diff --git a/gcc/ada/inline.adb b/gcc/ada/inline.adb
index 749e4dca9ae..5c43580d44f 100644
--- a/gcc/ada/inline.adb
+++ b/gcc/ada/inline.adb
@@ -1339,7 +1339,7 @@ package body Inline is
          Restore_Env;
       end if;
 
-      --  If secondary stk used there is no point in inlining. We have
+      --  If secondary stack is used, there is no point in inlining. We have
       --  already issued the warning in this case, so nothing to do.
 
       if Uses_Secondary_Stack (Body_To_Analyze) then
@@ -1399,7 +1399,7 @@ package body Inline is
 
          Error_Msg_NE (Msg (Msg'First .. Msg'Last - 1), N, Subp);
 
-      elsif Optimization_Level = 0 then
+      elsif Optimization_Level = 0 or else GNATprove_Mode then
 
          --  Do not emit warning if this is a predefined unit which is not
          --  the main unit. This behavior is currently provided for backward
@@ -1436,7 +1436,7 @@ package body Inline is
 
             Error_Msg_NE (Msg (Msg'First .. Msg'Last - 1), N, Subp);
 
-         else pragma Assert (Front_End_Inlining);
+         else pragma Assert (Front_End_Inlining or GNATprove_Mode);
             Set_Is_Inlined (Subp, False);
 
             --  When inlining cannot take place we must issue an error.
diff --git a/gcc/ada/opt.ads b/gcc/ada/opt.ads
index d5de7980d77..27e50c08ad1 100644
--- a/gcc/ada/opt.ads
+++ b/gcc/ada/opt.ads
@@ -772,10 +772,11 @@ package Opt is
    --  use of pragma Implicit_Packing.
 
    Ineffective_Inline_Warnings : Boolean := False;
-   --  GNAT
-   --  Set True to activate warnings if front-end inlining (-gnatN) is not
-   --  able to actually inline a particular call (or all calls). Can be
-   --  controlled by use of -gnatwp/-gnatwP.
+   --  GNAT Set True to activate warnings if front-end inlining (-gnatN) is
+   --  not able to actually inline a particular call (or all calls). Can be
+   --  controlled by use of -gnatwp/-gnatwP. Also set True to activate warnings
+   --  if frontend inlining is not able to inline a subprogram expected to be
+   --  inlined in GNATprove mode.
 
    Init_Or_Norm_Scalars : Boolean := False;
    --  GNAT, GANTBIND
diff --git a/gcc/ada/sem_prag.adb b/gcc/ada/sem_prag.adb
index 714512e4e95..5c22206e593 100644
--- a/gcc/ada/sem_prag.adb
+++ b/gcc/ada/sem_prag.adb
@@ -19998,6 +19998,14 @@ package body Sem_Prag is
                   Spec_Id := Corresponding_Spec (Context);
                   Context := Specification (Context);
                   Body_Id := Defining_Entity (Context);
+
+                  --  Ignore pragma when applied to the special body created
+                  --  for inlining, recognized by its internal name _Parent.
+
+                  if Chars (Body_Id) = Name_uParent then
+                     return;
+                  end if;
+
                   Check_Library_Level_Entity (Body_Id);
 
                   if Present (Spec_Id) then