Expansion of "for X of Y loop" where Y is an array was differed in GNAT
(where it was correct) and GNATprove (where it was wrong).
Typically expansion is controlled by the Expander_Active variable. In
GNATprove mode this variable is always False, so we need to explicitly
enable expansion where required (which is subtle and prone to
errors...).
With this patch, a loop over an array is now expanded for GNATprove just
like for GNAT, in particular, we now get a renaming of the iterated
object:
R : ... renames Y;
-- This renaming is crucial to remove side effects from Y, but it
-- was missing in the GNATprove mode.
for X in _low_ .. _high_ loop ...
A similar loop over an object that is subject to aspect Iterable is
expanded into a WHILE loop for GNAT, but kept as "FOR ... OF ..." for
GNATprove. With this patch a similar renaming of the iterated object is
created in GNATprove mode:
R : ... renames Y;
for X of R loop ...
However, the reference to R must be analyzed, so that a special
expansion of renamed objects for GNATprove replaces it with a reference
to Y.
Tested on x86_64-pc-linux-gnu, committed on trunk
2020-06-17 Piotr Trojanek <troja...@adacore.com>
gcc/ada/
* sem_ch5.adb (Analyze_Iterator_Specification): Enable expansion
that creates a renaming that removes side effects from the
iterated object in the GNATprove mode; then analyze reference to
this renaming (it is required for GNATprove and harmless for
GNAT).--- gcc/ada/sem_ch5.adb
+++ gcc/ada/sem_ch5.adb
@@ -2214,8 +2214,8 @@ package body Sem_Ch5 is
-- 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.
+ -- The declaration must be a renaming (both in GNAT and GNATprove
+ -- modes), because the body of the loop may assign to elements.
if not Is_Entity_Name (Iter_Name)
@@ -2224,14 +2224,15 @@ package body Sem_Ch5 is
-- doing expansion.
and then (Nkind (Parent (N)) /= N_Quantified_Expression
- or else Operating_Mode = Check_Semantics)
+ or else (Operating_Mode = Check_Semantics
+ and then not GNATprove_Mode))
-- Do not perform this expansion when expansion is disabled, where the
-- temporary may hide the transformation of a selected component into
-- a prefixed function call, and references need to see the original
-- expression.
- and then Expander_Active
+ and then (Expander_Active or GNATprove_Mode)
then
declare
Id : constant Entity_Id := Make_Temporary (Loc, 'R', Iter_Name);
@@ -2319,6 +2320,7 @@ package body Sem_Ch5 is
Insert_Actions (Parent (Parent (N)), New_List (Decl));
Rewrite (Name (N), New_Occurrence_Of (Id, Loc));
+ Analyze (Name (N));
Set_Etype (Id, Typ);
Set_Etype (Name (N), Typ);
end;
