Expansion for set membership in normal mode is also useful in Alfa mode for
formal verification, hence apply it too in that case.
Tested on x86_64-pc-linux-gnu, committed on trunk
2011-09-19 Yannick Moy <m...@adacore.com>
* exp_alfa.adb, exp_alfa.ads (Expand_Alfa_N_In): New function
for expansion of set membership.
(Expand_Alfa): Call expansion for N_In and N_Not_In nodes.
* exp_ch4.adb, exp_ch4.ads (Expand_Set_Membership): Make procedure
visible for use in Alfa expansion.
* sem_ch5.adb (Analyze_Iterator_Specification): Introduce loop
variable in Alfa mode.
Index: exp_alfa.adb
===================================================================
--- exp_alfa.adb (revision 178955)
+++ exp_alfa.adb (working copy)
@@ -26,8 +26,10 @@
with Atree; use Atree;
with Einfo; use Einfo;
with Exp_Attr; use Exp_Attr;
+with Exp_Ch4; use Exp_Ch4;
with Exp_Ch6; use Exp_Ch6;
with Exp_Dbug; use Exp_Dbug;
+with Nlists; use Nlists;
with Rtsfind; use Rtsfind;
with Sem_Aux; use Sem_Aux;
with Sem_Res; use Sem_Res;
@@ -51,6 +53,9 @@
procedure Expand_Alfa_N_Attribute_Reference (N : Node_Id);
-- Expand attributes 'Old and 'Result only
+ procedure Expand_Alfa_N_In (N : Node_Id);
+ -- Expand set membership into individual ones
+
procedure Expand_Alfa_N_Simple_Return_Statement (N : Node_Id);
-- Insert conversion on function return if necessary
@@ -81,6 +86,12 @@
when N_Attribute_Reference =>
Expand_Alfa_N_Attribute_Reference (N);
+ when N_In =>
+ Expand_Alfa_N_In (N);
+
+ when N_Not_In =>
+ Expand_N_Not_In (N);
+
when others =>
null;
end case;
@@ -167,6 +178,18 @@
end case;
end Expand_Alfa_N_Attribute_Reference;
+ ----------------------
+ -- Expand_Alfa_N_In --
+ ----------------------
+
+ procedure Expand_Alfa_N_In (N : Node_Id) is
+ begin
+ if Present (Alternatives (N)) then
+ Expand_Set_Membership (N);
+ return;
+ end if;
+ end Expand_Alfa_N_In;
+
-------------------------------------------
-- Expand_Alfa_N_Simple_Return_Statement --
-------------------------------------------
Index: exp_alfa.ads
===================================================================
--- exp_alfa.ads (revision 178955)
+++ exp_alfa.ads (working copy)
@@ -37,7 +37,7 @@
-- conversions, expand actuals in calls to introduce temporaries)
-- 2. Facilitate treatment for the formal verification back-end (fully
--- qualify names)
+-- qualify names, set membership)
-- 3. Avoid the introduction of low-level code that is difficult to analyze
-- formally, as typically done in the full expansion for high-level
Index: exp_ch4.adb
===================================================================
--- exp_ch4.adb (revision 178955)
+++ exp_ch4.adb (working copy)
@@ -4630,68 +4630,6 @@
Ltyp : Entity_Id;
Rtyp : Entity_Id;
- procedure Expand_Set_Membership;
- -- For each choice we create a simple equality or membership test.
- -- The whole membership is rewritten connecting these with OR ELSE.
-
- ---------------------------
- -- Expand_Set_Membership --
- ---------------------------
-
- procedure Expand_Set_Membership is
- Alt : Node_Id;
- Res : Node_Id;
-
- function Make_Cond (Alt : Node_Id) return Node_Id;
- -- If the alternative is a subtype mark, create a simple membership
- -- test. Otherwise create an equality test for it.
-
- ---------------
- -- Make_Cond --
- ---------------
-
- function Make_Cond (Alt : Node_Id) return Node_Id is
- Cond : Node_Id;
- L : constant Node_Id := New_Copy (Lop);
- R : constant Node_Id := Relocate_Node (Alt);
-
- begin
- if (Is_Entity_Name (Alt) and then Is_Type (Entity (Alt)))
- or else Nkind (Alt) = N_Range
- then
- Cond :=
- Make_In (Sloc (Alt),
- Left_Opnd => L,
- Right_Opnd => R);
- else
- Cond :=
- Make_Op_Eq (Sloc (Alt),
- Left_Opnd => L,
- Right_Opnd => R);
- end if;
-
- return Cond;
- end Make_Cond;
-
- -- Start of processing for Expand_Set_Membership
-
- begin
- Alt := Last (Alternatives (N));
- Res := Make_Cond (Alt);
-
- Prev (Alt);
- while Present (Alt) loop
- Res :=
- Make_Or_Else (Sloc (Alt),
- Left_Opnd => Make_Cond (Alt),
- Right_Opnd => Res);
- Prev (Alt);
- end loop;
-
- Rewrite (N, Res);
- Analyze_And_Resolve (N, Standard_Boolean);
- end Expand_Set_Membership;
-
procedure Substitute_Valid_Check;
-- Replaces node N by Lop'Valid. This is done when we have an explicit
-- test for the left operand being in range of its subtype.
@@ -4721,8 +4659,7 @@
-- If set membership case, expand with separate procedure
if Present (Alternatives (N)) then
- Remove_Side_Effects (Lop);
- Expand_Set_Membership;
+ Expand_Set_Membership (N);
return;
end if;
@@ -9717,6 +9654,67 @@
return Result;
end Expand_Record_Equality;
+ ---------------------------
+ -- Expand_Set_Membership --
+ ---------------------------
+
+ procedure Expand_Set_Membership (N : Node_Id) is
+ Lop : constant Node_Id := Left_Opnd (N);
+ Alt : Node_Id;
+ Res : Node_Id;
+
+ function Make_Cond (Alt : Node_Id) return Node_Id;
+ -- If the alternative is a subtype mark, create a simple membership
+ -- test. Otherwise create an equality test for it.
+
+ ---------------
+ -- Make_Cond --
+ ---------------
+
+ function Make_Cond (Alt : Node_Id) return Node_Id is
+ Cond : Node_Id;
+ L : constant Node_Id := New_Copy (Lop);
+ R : constant Node_Id := Relocate_Node (Alt);
+
+ begin
+ if (Is_Entity_Name (Alt) and then Is_Type (Entity (Alt)))
+ or else Nkind (Alt) = N_Range
+ then
+ Cond :=
+ Make_In (Sloc (Alt),
+ Left_Opnd => L,
+ Right_Opnd => R);
+ else
+ Cond :=
+ Make_Op_Eq (Sloc (Alt),
+ Left_Opnd => L,
+ Right_Opnd => R);
+ end if;
+
+ return Cond;
+ end Make_Cond;
+
+ -- Start of processing for Expand_Set_Membership
+
+ begin
+ Remove_Side_Effects (Lop);
+
+ Alt := Last (Alternatives (N));
+ Res := Make_Cond (Alt);
+
+ Prev (Alt);
+ while Present (Alt) loop
+ Res :=
+ Make_Or_Else (Sloc (Alt),
+ Left_Opnd => Make_Cond (Alt),
+ Right_Opnd => Res);
+ Prev (Alt);
+ end loop;
+
+ Rewrite (N, Res);
+ Analyze_And_Resolve (N, Standard_Boolean);
+ end Expand_Set_Membership;
+
-----------------------------------
-- Expand_Short_Circuit_Operator --
-----------------------------------
Index: exp_ch4.ads
===================================================================
--- exp_ch4.ads (revision 178955)
+++ exp_ch4.ads (working copy)
@@ -91,6 +91,11 @@
-- to insert those bodies at the right place. Nod provides the Sloc
-- value for generated code.
+ procedure Expand_Set_Membership (N : Node_Id);
+ -- For each choice of a set membership, we create a simple equality or
+ -- membership test. The whole membership is rewritten connecting these
+ -- with OR ELSE.
+
function Integer_Promotion_Possible (N : Node_Id) return Boolean;
-- Returns true if the node is a type conversion whose operand is an
-- arithmetic operation on signed integers, and the base type of the
Index: sem_ch5.adb
===================================================================
--- sem_ch5.adb (revision 178955)
+++ sem_ch5.adb (working copy)
@@ -2302,10 +2302,12 @@
Typ : Entity_Id;
begin
- -- In semantics mode, introduce loop variable so that loop body can be
- -- properly analyzed. Otherwise this is one after expansion.
+ -- In semantics and Alfa modes, introduce loop variable so that loop
+ -- body can be properly analyzed. Otherwise this is one after expansion.
- if Operating_Mode = Check_Semantics then
+ if Operating_Mode = Check_Semantics
+ or else Alfa_Mode
+ then
Enter_Name (Def_Id);
end if;
