In formal verification mode, pragma check and enclosed expression are not
expanded, so no transient scope should be introduced for a pragma check as a
result of the introduction of temporary variables during expansion.
Tested on x86_64-pc-linux-gnu, committed on trunk
2011-08-05 Yannick Moy <m...@adacore.com>
* exp_ch7.adb (Establish_Transient_Scope): in formal verification mode,
if the node to wrap is a pragma check, this node and enclosed
expression are not expanded, so do not apply any transformations here.
* exp_prag.adb (Expand_Pragma_Check): document the need to avoid
introducing transient scopes.
Index: exp_prag.adb
===================================================================
--- exp_prag.adb (revision 177382)
+++ exp_prag.adb (working copy)
@@ -321,7 +321,10 @@
-- be an explicit conditional in the source, not an implicit if, so we
-- do not call Make_Implicit_If_Statement.
- -- In formal verification mode, we keep the pragma check in the code
+ -- In formal verification mode, we keep the pragma check in the code,
+ -- and its enclosed expression is not expanded. This requires that no
+ -- transient scope is introduced for pragma check in this mode in
+ -- Exp_Ch7.Establish_Transient_Scope.
if ALFA_Mode then
return;
Index: exp_ch7.adb
===================================================================
--- exp_ch7.adb (revision 177407)
+++ exp_ch7.adb (working copy)
@@ -3532,6 +3532,16 @@
elsif Nkind (Wrap_Node) = N_Iteration_Scheme then
null;
+ -- In formal verification mode, if the node to wrap is a pragma check,
+ -- this node and enclosed expression are not expanded, so do not apply
+ -- any transformations here.
+
+ elsif ALFA_Mode
+ and then Nkind (Wrap_Node) = N_Pragma
+ and then Get_Pragma_Id (Wrap_Node) = Pragma_Check
+ then
+ null;
+
else
Push_Scope (New_Internal_Entity (E_Block, Current_Scope, Loc, 'B'));
Set_Scope_Is_Transient;
