From 85ee7b4903e320b8f22ac0350afcd07263d2a5d6 Mon Sep 17 00:00:00 2001 From: Yannick Moy Date: Fri, 5 Jul 2019 07:01:58 +0000 Subject: [PATCH] [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 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 --- gcc/ada/ChangeLog | 7 +++++++ gcc/ada/sem_res.adb | 9 +++++++++ gcc/ada/sem_util.adb | 19 +++++++++++++++++++ gcc/ada/sem_util.ads | 3 +++ 4 files changed, 38 insertions(+) diff --git a/gcc/ada/ChangeLog b/gcc/ada/ChangeLog index eacc5f28a9d..6f22a1ae5e6 100644 --- a/gcc/ada/ChangeLog +++ b/gcc/ada/ChangeLog @@ -1,3 +1,10 @@ +2019-07-05 Yannick Moy + + * 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 * doc/gnat_rm/standard_and_implementation_defined_restrictions.rst: diff --git a/gcc/ada/sem_res.adb b/gcc/ada/sem_res.adb index 8521478a671..9c226357483 100644 --- 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 868e93ea955..55e64432a75 100644 --- 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 3f8d2e75d68..43c0bc58913 100644 --- 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. -- 2.30.2