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 <m...@adacore.com>
* sem_ch5.adb (Analyze_Iterator_Specification): Do not perform
an expansion of the iterator in Alfa mode.
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
