diff mbox

[Ada] Remove special case for actual of calls in SPARK expansion

Message ID 20131013162212.GA13633@adacore.com
State New
Headers show

Commit Message

Arnaud Charlet Oct. 13, 2013, 4:22 p.m. UTC 
The special SPARK expansion used for formal verification special-cased
calls to introduce temporaries for actuals in some cases. This is not
needed anymore, and this could prevent detection of aliasing later, so
it has been removed.

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

2013-10-13  Yannick Moy  <moy@adacore.com>

	* exp_spark.adb (Expand_SPARK_Call): Do not introduce temporaries for
	actuals.
diff mbox

Patch

Index: exp_spark.adb
===================================================================
--- exp_spark.adb	(revision 203502)
+++ exp_spark.adb	(working copy)
@@ -26,7 +26,6 @@ 
 with Atree;    use Atree;
 with Einfo;    use Einfo;
 with Exp_Ch4;  use Exp_Ch4;
-with Exp_Ch6;  use Exp_Ch6;
 with Exp_Dbug; use Exp_Dbug;
 with Exp_Util; use Exp_Util;
 with Sem_Aux;  use Sem_Aux;
@@ -43,9 +42,7 @@ 
 
    procedure Expand_SPARK_Call (N : Node_Id);
    --  This procedure contains common processing for function and procedure
-   --  calls:
-   --    * expansion of actuals to introduce necessary temporaries
-   --    * replacement of renaming by subprogram renamed
+   --  calls: replacement of renaming by subprogram renamed
 
    procedure Expand_SPARK_N_Object_Renaming_Declaration (N : Node_Id);
    --  Perform name evaluation for a renamed object
@@ -106,7 +103,6 @@ 
    procedure Expand_SPARK_Call (N : Node_Id) is
       Call_Node   : constant Node_Id := N;
       Parent_Subp : Entity_Id;
-      Subp        : Entity_Id;
 
    begin
       --  Ignore if previous error
@@ -120,14 +116,12 @@ 
       --  Call using access to subprogram with explicit dereference
 
       if Nkind (Name (Call_Node)) = N_Explicit_Dereference then
-         Subp        := Etype (Name (Call_Node));
          Parent_Subp := Empty;
 
       --  Case of call to simple entry, where the Name is a selected component
       --  whose prefix is the task, and whose selector name is the entry name
 
       elsif Nkind (Name (Call_Node)) = N_Selected_Component then
-         Subp        := Entity (Selector_Name (Name (Call_Node)));
          Parent_Subp := Empty;
 
       --  Case of call to member of entry family, where Name is an indexed
@@ -135,20 +129,14 @@ 
       --  task and entry family name, and the index being the entry index.
 
       elsif Nkind (Name (Call_Node)) = N_Indexed_Component then
-         Subp        := Entity (Selector_Name (Prefix (Name (Call_Node))));
          Parent_Subp := Empty;
 
       --  Normal case
 
       else
-         Subp        := Entity (Name (Call_Node));
-         Parent_Subp := Alias (Subp);
+         Parent_Subp := Alias (Entity (Name (Call_Node)));
       end if;
 
-      --  Various expansion activities for actuals are carried out
-
-      Expand_Actuals (N, Subp);
-
       --  If the subprogram is a renaming, replace it in the call with the name
       --  of the actual subprogram being called.