gnat1drv.adb (Adjust_Global_Switches): Set Ineffective_Inline_Warnings to True in...

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.

From-SVN: r213245

diff --git a/gcc/ada/ChangeLog b/gcc/ada/ChangeLog
index 463f3704dc2f29dda23609dd18c3f02c055ff15b..e9542062c924a85cf814babda7a7c613d537fe43 100644 (file)
--- 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 756961e3d2da83347d1cae7c6b9c382844321e24..9a61d484d568da8c0f249c8d6035e9c348862ab2 100644 (file)
--- 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 749e4dca9ae069ce0360175fa163266cfe65b19b..5c43580d44f8695e06cfd7056d223b84d4359f35 100644 (file)
--- 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 d5de7980d77dae7c0f0a9b6ea5d1a95c59ded24d..27e50c08ad16d4b6ce8ee73db764e28dd2a74eeb 100644 (file)
--- 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 714512e4e958eba80e5b6a583319f5100dba014e..5c22206e593af4dd10ceca8a501e13ea2c4f98de 100644 (file)
--- 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