[Ada] Fix Next_Actual when used on calls "inlined for proof"
authorPiotr Trojanek <trojanek@adacore.com>
Tue, 17 Jul 2018 08:06:04 +0000 (08:06 +0000)
committerPierre-Marie de Rodat <pmderodat@gcc.gnu.org>
Tue, 17 Jul 2018 08:06:04 +0000 (08:06 +0000)
commit5ffc5c55091ba8a2d5290f7a0851c5d484e8ac85
treea68dd8dd6acbea5a39db1a660cf6a4183f4b0545
parentc70f758353d78fe242253031ab9764c419862ce2
[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
gcc/ada/ChangeLog
gcc/ada/sem_util.adb