Patchwork [Ada] Always analyze loop body during semantic analysis in Alfa mode

login
register
mail settings
Submitter Arnaud Charlet
Date July 23, 2012, 8:29 a.m.
Message ID <20120723082940.GA18881@adacore.com>
Download mbox | patch
Permalink /patch/172578/
State New
Headers show

Comments

Arnaud Charlet - July 23, 2012, 8:29 a.m.
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  <moy@adacore.com>

	* sem_ch5.adb (Analyze_Loop_Statement): Make sure the loop body
	is analyzed in Alfa mode.

Patch

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