[Ada] Fix Next_Actual when used on calls "inlined for proof"

Message ID 20180717082212.GA1058@adacore.com
State New
Headers show
Series
  • [Ada] Fix Next_Actual when used on calls "inlined for proof"
Related show

Commit Message

Pierre-Marie de Rodat July 17, 2018, 8:22 a.m.
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.

Tested on x86_64-pc-linux-gnu, committed on trunk

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.

Patch

--- gcc/ada/sem_util.adb
+++ 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;