Formal verification constraints already ensure that expressions are free from
side-effects, so no need for removal of side-effects in Alfa mode.
Tested on x86_64-pc-linux-gnu, committed on trunk
2011-11-21 Yannick Moy <m...@adacore.com>
* exp_util.adb (Remove_Side_Effects): Do nothing in Alfa mode.
Index: exp_util.adb
===================================================================
--- exp_util.adb (revision 181574)
+++ exp_util.adb (working copy)
@@ -6420,9 +6420,12 @@
-- Start of processing for Remove_Side_Effects
begin
- -- Handle cases in which there is nothing to do
+ -- Handle cases in which there is nothing to do. In particular,
+ -- side-effects are not removed in Alfa mode for formal verification.
+ -- Instead, formal verification is performed only on those expressions
+ -- provably side-effect free.
- if not Expander_Active then
+ if not Full_Expander_Active then
return;
-- Cannot generate temporaries if the invocation to remove side effects
@@ -6622,15 +6625,6 @@
-- Otherwise we generate a reference to the value
else
- -- An expression which is in Alfa mode is considered side effect free
- -- if the resulting value is captured by a variable or a constant.
-
- if Alfa_Mode
- and then Nkind (Parent (Exp)) = N_Object_Declaration
- then
- return;
- end if;
-
-- Special processing for function calls that return a limited type.
-- We need to build a declaration that will enable build-in-place
-- expansion of the call. This is not done if the context is already
@@ -6665,40 +6659,26 @@
Def_Id := Make_Temporary (Loc, 'R', Exp);
Set_Etype (Def_Id, Exp_Type);
- -- The regular expansion of functions with side effects involves the
- -- generation of an access type to capture the return value found on
- -- the secondary stack. Since Alfa (and why) cannot process access
- -- types, use a different approach which ignores the secondary stack
- -- and "copies" the returned object.
+ Res :=
+ Make_Explicit_Dereference (Loc,
+ Prefix => New_Reference_To (Def_Id, Loc));
- if Alfa_Mode then
- Res := New_Reference_To (Def_Id, Loc);
- Ref_Type := Exp_Type;
+ -- Generate:
+ -- type Ann is access all <Exp_Type>;
- -- Regular expansion utilizing an access type and 'reference
+ Ref_Type := Make_Temporary (Loc, 'A');
- else
- Res :=
- Make_Explicit_Dereference (Loc,
- Prefix => New_Reference_To (Def_Id, Loc));
+ Ptr_Typ_Decl :=
+ Make_Full_Type_Declaration (Loc,
+ Defining_Identifier => Ref_Type,
+ Type_Definition =>
+ Make_Access_To_Object_Definition (Loc,
+ All_Present => True,
+ Subtype_Indication =>
+ New_Reference_To (Exp_Type, Loc)));
- -- Generate:
- -- type Ann is access all <Exp_Type>;
+ Insert_Action (Exp, Ptr_Typ_Decl);
- Ref_Type := Make_Temporary (Loc, 'A');
-
- Ptr_Typ_Decl :=
- Make_Full_Type_Declaration (Loc,
- Defining_Identifier => Ref_Type,
- Type_Definition =>
- Make_Access_To_Object_Definition (Loc,
- All_Present => True,
- Subtype_Indication =>
- New_Reference_To (Exp_Type, Loc)));
-
- Insert_Action (Exp, Ptr_Typ_Decl);
- end if;
-
E := Exp;
if Nkind (E) = N_Explicit_Dereference then
New_Exp := Relocate_Node (Prefix (E));
