This is the mail archive of the gcc-patches@gcc.gnu.org mailing list for the GCC project.


Index Nav: [Date Index] [Subject Index] [Author Index] [Thread Index]
Message Nav: [Date Prev] [Date Next] [Thread Prev] [Thread Next]
Other format: [Raw text]

[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.

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.
--- 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;


Index Nav: [Date Index] [Subject Index] [Author Index] [Thread Index]
Message Nav: [Date Prev] [Date Next] [Thread Prev] [Thread Next]