[Ada] Do not generate wrong transient scopes for pragma check in ALFA mode

[Arnaud Charlet]

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  <moy@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.

-------------- next part --------------
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;