In Alfa mode for formal verification, the loop form with an iterator is not
expanded, thus the analysis of the loop body should be done during semantic
analysis.
Tested on x86_64-pc-linux-gnu, committed on trunk
2012-07-23 Yannick Moy <[email protected]>
* sem_ch5.adb (Analyze_Loop_Statement): Make sure the loop body
is analyzed in Alfa mode.
Index: sem_ch5.adb
===================================================================
--- sem_ch5.adb (revision 189768)
+++ sem_ch5.adb (working copy)
@@ -2633,14 +2633,14 @@
-- types the actual subtype of the components will only be determined
-- when the cursor declaration is analyzed.
- -- If the expander is not active, then we want to analyze the loop body
- -- now even in the Ada 2012 iterator case, since the rewriting will not
- -- be done. Insert the loop variable in the current scope, if not done
- -- when analysing the iteration scheme.
+ -- If the expander is not active, or in Alfa mode, then we want to
+ -- analyze the loop body now even in the Ada 2012 iterator case, since
+ -- the rewriting will not be done. Insert the loop variable in the
+ -- current scope, if not done when analysing the iteration scheme.
if No (Iter)
or else No (Iterator_Specification (Iter))
- or else not Expander_Active
+ or else not Full_Expander_Active
then
if Present (Iter)
and then Present (Iterator_Specification (Iter))
