In Alfa mode for formal verification, a special expansion done in the frontend
turns out to be both harmful and unneeded, because the formal verification
backend relies on the types of nodes (hence is not robust w.r.t. a change to
base type here), and does not suffer from the out-of-order issue targetted by
the special expansion. Thus, this expansion is skipped in Alfa mode.
Tested on x86_64-pc-linux-gnu, committed on trunk
2012-08-06 Yannick Moy <[email protected]>
* sem_attr.adb (Analyze_Attribute): In the case for 'Old,
skip a special expansion which is not needed in Alfa mode.
Index: sem_attr.adb
===================================================================
--- sem_attr.adb (revision 190155)
+++ sem_attr.adb (working copy)
@@ -4034,7 +4034,13 @@
-- enclosing subprogram. This is properly an expansion activity
-- but it has to be performed now to prevent out-of-order issues.
- if not Is_Entity_Name (P) then
+ -- This expansion is both harmful and not needed in Alfa mode, since
+ -- the formal verification backend relies on the types of nodes
+ -- (hence is not robust w.r.t. a change to base type here), and does
+ -- not suffer from the out-of-order issue described above. Thus, this
+ -- expansion is skipped in Alfa mode.
+
+ if not Is_Entity_Name (P) and then not Alfa_Mode then
P_Type := Base_Type (P_Type);
Set_Etype (N, P_Type);
Set_Etype (P, P_Type);
