diff mbox

[Ada] Skip unneeded expansion for Alfa mode

Message ID 20120806075231.GA26669@adacore.com
State New
Headers show

Commit Message

Arnaud Charlet Aug. 6, 2012, 7:52 a.m. UTC 
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  <moy@adacore.com>

	* sem_attr.adb (Analyze_Attribute): In the case for 'Old,
	skip a special expansion which is not needed in Alfa mode.
diff mbox

Patch

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);