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 <m...@adacore.com>
* exp_spark.adb (Expand_SPARK_N_In): Remove procedure.
(Expand_SPARK): Remove special expansion for membership tests.
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 --
------------------------------------------------
