[Ada] Fix inlining in GNATprove inside quantified expressions

Calls to local subprograms in GNATprove may be inlined in some case, but
it should not be the case inside quantified expressions which are
handled as expressions inside GNATprove. Because quantified expressions
are only preanalayzed, the detection of the impossible inlining was not
performed.  Now fixed.

There is no impact on compilation.

2019-07-05  Yannick Moy  <moy@adacore.com>

gcc/ada/

	* sem_res.adb (Resolve_Call): Cannot inline in quantified
	expressions.
	* sem_util.adb, sem_util.ads (In_Quantified_Expression): New
	function.

From-SVN: r273105

diff --git a/gcc/ada/ChangeLog b/gcc/ada/ChangeLog
index eacc5f28a9da444b1b75ea79eb5096c010b01d9e..6f22a1ae5e69f66c97db0845a031563a586578d1 100644 (file)
--- a/gcc/ada/ChangeLog
+++ b/gcc/ada/ChangeLog
@@ -1,3 +1,10 @@
+2019-07-05  Yannick Moy  <moy@adacore.com>
+
+       * sem_res.adb (Resolve_Call): Cannot inline in quantified
+       expressions.
+       * sem_util.adb, sem_util.ads (In_Quantified_Expression): New
+       function.
+
 2019-07-05  Bob Duff  <duff@adacore.com>
 
        * doc/gnat_rm/standard_and_implementation_defined_restrictions.rst:

diff --git a/gcc/ada/sem_res.adb b/gcc/ada/sem_res.adb
index 8521478a6710beb26d6eef269b6a66cc65810e75..9c226357483e63444f6098dc2356835f178215e9 100644 (file)
--- a/gcc/ada/sem_res.adb
+++ b/gcc/ada/sem_res.adb
@@ -6768,6 +6768,15 @@ package body Sem_Res is
                Cannot_Inline
                  ("cannot inline & (in default expression)?", N, Nam_UA);
 
+            --  Calls cannot be inlined inside quantified expressions, which
+            --  are left in expression form for GNATprove. Since these
+            --  expressions are only preanalyzed, we need to detect the failure
+            --  to inline outside of the case for Full_Analysis below.
+
+            elsif In_Quantified_Expression (N) then
+               Cannot_Inline
+                 ("cannot inline & (in quantified expression)?", N, Nam_UA);
+
             --  Inlining should not be performed during preanalysis
 
             elsif Full_Analysis then

diff --git a/gcc/ada/sem_util.adb b/gcc/ada/sem_util.adb
index 868e93ea9559184a660a48aee300c087892e226e..55e64432a756a2deb6cd79fef71a47cab17044db 100644 (file)
--- a/gcc/ada/sem_util.adb
+++ b/gcc/ada/sem_util.adb
@@ -12305,6 +12305,25 @@ package body Sem_Util is
       end if;
    end In_Pre_Post_Condition;
 
+   ------------------------------
+   -- In_Quantified_Expression --
+   ------------------------------
+
+   function In_Quantified_Expression (N : Node_Id) return Boolean is
+      P : Node_Id;
+   begin
+      P := Parent (N);
+      loop
+         if No (P) then
+            return False;
+         elsif Nkind (P) = N_Quantified_Expression then
+            return True;
+         else
+            P := Parent (P);
+         end if;
+      end loop;
+   end In_Quantified_Expression;
+
    -------------------------------------
    -- In_Reverse_Storage_Order_Object --
    -------------------------------------

diff --git a/gcc/ada/sem_util.ads b/gcc/ada/sem_util.ads
index 3f8d2e75d68d2dc9dae060e081bcccfe1f13e29c..43c0bc589133af1f6871a9c302a2d20246859b77 100644 (file)
--- a/gcc/ada/sem_util.ads
+++ b/gcc/ada/sem_util.ads
@@ -1410,6 +1410,9 @@ package Sem_Util is
    --  Returns True if node N appears within a pre/postcondition pragma. Note
    --  the pragma Check equivalents are NOT considered.
 
+   function In_Quantified_Expression (N : Node_Id) return Boolean;
+   --  Returns true if the expression N occurs within a quantified expression
+
    function In_Reverse_Storage_Order_Object (N : Node_Id) return Boolean;
    --  Returns True if N denotes a component or subcomponent in a record or
    --  array that has Reverse_Storage_Order.