aboutsummaryrefslogtreecommitdiff
path: root/gcc
diff options
context:
space:
mode:
authorPiotr Trojanek <trojanek@adacore.com>2018-07-17 08:06:04 +0000
committerPierre-Marie de Rodat <pmderodat@gcc.gnu.org>2018-07-17 08:06:04 +0000
commit5ffc5c55091ba8a2d5290f7a0851c5d484e8ac85 (patch)
treea68dd8dd6acbea5a39db1a660cf6a4183f4b0545 /gcc
parentc70f758353d78fe242253031ab9764c419862ce2 (diff)
downloadgcc-5ffc5c55091ba8a2d5290f7a0851c5d484e8ac85.zip
gcc-5ffc5c55091ba8a2d5290f7a0851c5d484e8ac85.tar.gz
gcc-5ffc5c55091ba8a2d5290f7a0851c5d484e8ac85.tar.bz2
[Ada] Fix Next_Actual when used on calls "inlined for proof"
The GNATprove backend needs to apply antialiasing checks to subprogram calls that have been rewritten into null statements while "inlining for proof". This requires the First_Actual/Next_Actual to use the Original_Node and not the N_Null_Statement that rewriting leaves as a parent. Only effective in GNATprove mode, so no frontend test provided. 2018-07-17 Piotr Trojanek <trojanek@adacore.com> gcc/ada/ * sem_util.adb (Next_Actual): If the parent is a N_Null_Statement, which happens for inlined calls, then fetch the next actual from the original AST. From-SVN: r262773
Diffstat (limited to 'gcc')
-rw-r--r--gcc/ada/ChangeLog6
-rw-r--r--gcc/ada/sem_util.adb22
2 files changed, 23 insertions, 5 deletions
diff --git a/gcc/ada/ChangeLog b/gcc/ada/ChangeLog
index f813f88..2be7d3b 100644
--- a/gcc/ada/ChangeLog
+++ b/gcc/ada/ChangeLog
@@ -1,3 +1,9 @@
+2018-07-17 Piotr Trojanek <trojanek@adacore.com>
+
+ * sem_util.adb (Next_Actual): If the parent is a N_Null_Statement,
+ which happens for inlined calls, then fetch the next actual from the
+ original AST.
+
2018-07-17 Ed Schonberg <schonberg@adacore.com>
* einfo.ads: Update documentation for Scalar_Range.
diff --git a/gcc/ada/sem_util.adb b/gcc/ada/sem_util.adb
index 3b14252..fa24d4a 100644
--- a/gcc/ada/sem_util.adb
+++ b/gcc/ada/sem_util.adb
@@ -21033,7 +21033,8 @@ package body Sem_Util is
-----------------
function Next_Actual (Actual_Id : Node_Id) return Node_Id is
- N : Node_Id;
+ N : Node_Id;
+ Par : constant Node_Id := Parent (Actual_Id);
begin
-- If we are pointing at a positional parameter, it is a member of a
@@ -21053,11 +21054,22 @@ package body Sem_Util is
-- In case of a build-in-place call, the call will no longer be a
-- call; it will have been rewritten.
- if Nkind_In (Parent (Actual_Id), N_Entry_Call_Statement,
- N_Function_Call,
- N_Procedure_Call_Statement)
+ if Nkind_In (Par, N_Entry_Call_Statement,
+ N_Function_Call,
+ N_Procedure_Call_Statement)
then
- return First_Named_Actual (Parent (Actual_Id));
+ return First_Named_Actual (Par);
+
+ -- In case of a call rewritten in GNATprove mode while "inlining
+ -- for proof" go to the original call.
+
+ elsif Nkind (Par) = N_Null_Statement then
+ pragma Assert
+ (GNATprove_Mode
+ and then
+ Nkind (Original_Node (Par)) in N_Subprogram_Call);
+
+ return First_Named_Actual (Original_Node (Par));
else
return Empty;
end if;