Patchwork [Ada] Skip special expansion in Alfa mode

login
register
mail settings
Submitter Arnaud Charlet
Date Aug. 6, 2012, 7:52 a.m.
Message ID <20120806075238.GA26736@adacore.com>
Download mbox | patch
Permalink /patch/175287/
State New
Headers show

Comments

Arnaud Charlet - Aug. 6, 2012, 7:52 a.m.
In Alfa mode for formal verification, a special expansion of the iterator is
not needed, as the formal verification backend directly deals with the source
form of the iterator. Thus, skip this expansion.

Tested on x86_64-pc-linux-gnu, committed on trunk

2012-08-06  Yannick Moy  <moy@adacore.com>

	* sem_ch5.adb (Analyze_Iterator_Specification): Do not perform
	an expansion of the iterator in Alfa mode.

Patch

Index: sem_ch5.adb
===================================================================
--- sem_ch5.adb	(revision 190158)
+++ sem_ch5.adb	(working copy)
@@ -1665,16 +1665,21 @@ 
       --  If the domain of iteration is an expression, create a declaration for
       --  it, so that finalization actions are introduced outside of the loop.
       --  The declaration must be a renaming because the body of the loop may
-      --  assign to elements. When the context is a quantified expression, the
-      --  renaming declaration is delayed until the expansion phase.
+      --  assign to elements.
 
       if not Is_Entity_Name (Iter_Name)
+
+        --  When the context is a quantified expression, the renaming
+        --  declaration is delayed until the expansion phase if we are
+        --  doing expansion.
+
         and then (Nkind (Parent (N)) /= N_Quantified_Expression
+                   or else Operating_Mode = Check_Semantics)
 
-                   --  The following two tests need comments ???
+        --  Do not perform this expansion in Alfa mode, since the formal
+        --  verification directly deals with the source form of the iterator.
 
-                   or else Operating_Mode = Check_Semantics
-                   or else Alfa_Mode)
+        and then not Alfa_Mode
       then
          declare
             Id   : constant Entity_Id := Make_Temporary (Loc, 'R', Iter_Name);
@@ -1711,7 +1716,7 @@ 
       --  Container is an entity or an array with uncontrolled components, or
       --  else it is a container iterator given by a function call, typically
       --  called Iterate in the case of predefined containers, even though
-      --  Iterate is not a reserved name. What matter is that the return type
+      --  Iterate is not a reserved name. What matters is that the return type
       --  of the function is an iterator type.
 
       elsif Is_Entity_Name (Iter_Name) then