diff mbox

[Ada] Remove special expansion for membership tests in SPARK mode

Message ID 20130425104815.GA14342@adacore.com
State New
Headers show

Commit Message

Arnaud Charlet April 25, 2013, 10:48 a.m. UTC 
We now deal directly in the formal verification back-end with complex
membership tests, so this special expansion is useless and can be removed.

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

2013-04-25  Yannick Moy  <moy@adacore.com>

	* exp_spark.adb (Expand_SPARK_N_In): Remove procedure.
	(Expand_SPARK): Remove special expansion for membership tests.
diff mbox

Patch

Index: exp_spark.adb
===================================================================
--- exp_spark.adb	(revision 198234)
+++ exp_spark.adb	(working copy)
@@ -30,7 +30,6 @@ 
 with Exp_Ch6;  use Exp_Ch6;
 with Exp_Dbug; use Exp_Dbug;
 with Exp_Util; use Exp_Util;
-with Nlists;   use Nlists;
 with Rtsfind;  use Rtsfind;
 with Sem_Aux;  use Sem_Aux;
 with Sem_Res;  use Sem_Res;
@@ -55,9 +54,6 @@ 
    procedure Expand_SPARK_N_Attribute_Reference (N : Node_Id);
    --  Expand attributes 'Old and 'Result only
 
-   procedure Expand_SPARK_N_In (N : Node_Id);
-   --  Expand set membership into individual ones
-
    procedure Expand_SPARK_N_Object_Renaming_Declaration (N : Node_Id);
    --  Perform name evaluation for a renamed object
 
@@ -102,9 +98,6 @@ 
               N_Identifier    =>
             Expand_Potential_Renaming (N);
 
-         when N_In =>
-            Expand_SPARK_N_In (N);
-
          --  A NOT IN B gets transformed to NOT (A IN B). This is the same
          --  expansion used in the normal case, so shared the code.
 
@@ -204,17 +197,6 @@ 
       end case;
    end Expand_SPARK_N_Attribute_Reference;
 
-   -----------------------
-   -- Expand_SPARK_N_In --
-   -----------------------
-
-   procedure Expand_SPARK_N_In (N : Node_Id) is
-   begin
-      if Present (Alternatives (N)) then
-         Expand_Set_Membership (N);
-      end if;
-   end Expand_SPARK_N_In;
-
    ------------------------------------------------
    -- Expand_SPARK_N_Object_Renaming_Declaration --
    ------------------------------------------------