The use of a specific light expansion for SPARK verification has rendered
obsolete a number of special handling cases only triggered in the normal
full expansion. Remove these useless cases now.
Tested on x86_64-pc-linux-gnu, committed on trunk
2013-10-17 Yannick Moy <m...@adacore.com>
* exp_ch3.adb (Expand_Freeze_Class_Wide_Type,
Expand_Freeze_Class_Wide_Type, Expand_Freeze_Class_Wide_Type):
Remove useless special cases.
* exp_ch4.adb (Expand_Allocator_Expression, Expand_N_Allocator,
Expand_N_Op_Expon): Remove useless special cases.
* exp_ch6.adb (Is_Build_In_Place_Function_Call): Disable build-in-place
in SPARK mode by testing Full_Expander_Active instead of
Expander_Active.
(Make_Build_In_Place_Call_In_Allocator): Remove useless special case.
* exp_util.adb (Build_Allocate_Deallocate_Proc): Remove
useless special case.
* sem_eval.adb (Compile_Time_Known_Value): Remove special handling of
deferred constant.
Index: exp_util.adb
===================================================================
--- exp_util.adb (revision 203568)
+++ exp_util.adb (working copy)
@@ -560,13 +560,6 @@
-- Start of processing for Build_Allocate_Deallocate_Proc
begin
- -- Do not perform this expansion in SPARK mode because it is not
- -- necessary.
-
- if SPARK_Mode then
- return;
- end if;
-
-- Obtain the attributes of the allocation / deallocation
if Nkind (N) = N_Free_Statement then
Index: exp_ch4.adb
===================================================================
--- exp_ch4.adb (revision 203568)
+++ exp_ch4.adb (working copy)
@@ -1268,14 +1268,10 @@
-- * .NET/JVM - these targets do not support address arithmetic
-- and unchecked conversion, key elements of Finalize_Address.
- -- * SPARK mode - the call is useless and results in unwanted
- -- expansion.
-
-- * CodePeer mode - TSS primitive Finalize_Address is not
-- created in this mode.
if VM_Target = No_VM
- and then not SPARK_Mode
and then not CodePeer_Mode
and then Present (Finalization_Master (PtrT))
and then Present (Temp_Decl)
@@ -4295,16 +4291,13 @@
end if;
-- The finalization master must be inserted and analyzed as part of
- -- the current semantic unit. This form of expansion is not carried
- -- out in SPARK mode because it is useless. Note that the master is
- -- updated when analysis changes current units.
+ -- the current semantic unit. Note that the master is updated when
+ -- analysis changes current units.
- if not SPARK_Mode then
- if Present (Rel_Typ) then
- Set_Finalization_Master (PtrT, Finalization_Master (Rel_Typ));
- else
- Set_Finalization_Master (PtrT, Current_Anonymous_Master);
- end if;
+ if Present (Rel_Typ) then
+ Set_Finalization_Master (PtrT, Finalization_Master (Rel_Typ));
+ else
+ Set_Finalization_Master (PtrT, Current_Anonymous_Master);
end if;
end if;
@@ -4839,15 +4832,11 @@
-- Set_Finalize_Address
-- (<PtrT>FM, <T>FD'Unrestricted_Access);
- -- Do not generate this call in the following cases:
- --
- -- * SPARK mode - the call is useless and results in
- -- unwanted expansion.
- --
- -- * CodePeer mode - TSS primitive Finalize_Address is
- -- not created in this mode.
+ -- Do not generate this call in CodePeer mode, as TSS
+ -- primitive Finalize_Address is not created in this
+ -- mode.
- elsif not (SPARK_Mode or CodePeer_Mode) then
+ elsif not CodePeer_Mode then
Insert_Action (N,
Make_Set_Finalize_Address_Call
(Loc => Loc,
@@ -7321,9 +7310,9 @@
begin
Binary_Op_Validity_Checks (N);
- -- CodePeer and GNATprove want to see the unexpanded N_Op_Expon node
+ -- CodePeer wants to see the unexpanded N_Op_Expon node
- if CodePeer_Mode or SPARK_Mode then
+ if CodePeer_Mode then
return;
end if;
Index: exp_ch6.adb
===================================================================
--- exp_ch6.adb (revision 203568)
+++ exp_ch6.adb (working copy)
@@ -9599,7 +9599,11 @@
-- disabled (such as with -gnatc) since those would trip over the raise
-- of Program_Error below.
- if not Expander_Active then
+ -- In SPARK mode, build-in-place calls are not expanded, so that we
+ -- may end up with a call that is neither resolved to an entity, nor
+ -- an indirect call.
+
+ if not Full_Expander_Active then
return False;
end if;
@@ -9616,14 +9620,7 @@
return False;
else
- -- In SPARK mode, build-in-place calls are not expanded, so that we
- -- may end up with a call that is neither resolved to an entity, nor
- -- an indirect call.
-
- if SPARK_Mode then
- return False;
-
- elsif Is_Entity_Name (Name (Exp_Node)) then
+ if Is_Entity_Name (Name (Exp_Node)) then
Function_Id := Entity (Name (Exp_Node));
-- In the case of an explicitly dereferenced call, use the subprogram
@@ -10092,14 +10089,10 @@
then
null;
- -- Do not generate the call to Set_Finalize_Address in SPARK mode
- -- because it is not necessary and results in unwanted expansion.
- -- This expansion is also not carried out in CodePeer mode because
- -- Finalize_Address is never built.
+ -- Do not generate the call to Set_Finalize_Address in CodePeer mode
+ -- because Finalize_Address is never built.
- elsif not SPARK_Mode
- and then not CodePeer_Mode
- then
+ elsif not CodePeer_Mode then
Insert_Action (Allocator,
Make_Set_Finalize_Address_Call (Loc,
Typ => Etype (Function_Id),
Index: sem_eval.adb
===================================================================
--- sem_eval.adb (revision 203568)
+++ sem_eval.adb (working copy)
@@ -1353,16 +1353,7 @@
if Ekind (E) = E_Enumeration_Literal then
return True;
- -- In SPARK mode, the value of deferred constants should be
- -- ignored outside the scope of their full view. This allows
- -- parameterized formal verification, in which a deferred constant
- -- value if not known from client units.
-
- elsif Ekind (E) = E_Constant
- and then not (SPARK_Mode
- and then Present (Full_View (E))
- and then not In_Open_Scopes (Scope (E)))
- then
+ elsif Ekind (E) = E_Constant then
V := Constant_Value (E);
return Present (V) and then Compile_Time_Known_Value (V);
end if;
Index: exp_ch3.adb
===================================================================
--- exp_ch3.adb (revision 203568)
+++ exp_ch3.adb (working copy)
@@ -6151,12 +6151,6 @@
elsif CodePeer_Mode then
return;
-
- -- Do not create TSS routine Finalize_Address when compiling in SPARK
- -- mode because it is not necessary and results in useless expansion.
-
- elsif SPARK_Mode then
- return;
end if;
-- Create the body of TSS primitive Finalize_Address. This automatically
@@ -6903,13 +6897,9 @@
-- be done before the bodies of all predefined primitives are
-- created. If Def_Id is limited, Stream_Input and Stream_Read
-- may produce build-in-place allocations and for those the
- -- expander needs Finalize_Address. Do not create the body of
- -- Finalize_Address in SPARK mode since it is not needed.
+ -- expander needs Finalize_Address.
- if not SPARK_Mode then
- Make_Finalize_Address_Body (Def_Id);
- end if;
-
+ Make_Finalize_Address_Body (Def_Id);
Predef_List := Predefined_Primitive_Bodies (Def_Id, Renamed_Eq);
Append_Freeze_Actions (Def_Id, Predef_List);
end if;
