https://gcc.gnu.org/g:5b30245800b1657f6c29212ca843c43bbfcffd20
commit r15-6195-g5b30245800b1657f6c29212ca843c43bbfcffd20
Author: Eric Botcazou <ebotca...@adacore.com>
Date: Thu Nov 28 23:05:52 2024 +0100
ada: Fix breakage of GNATprove introduced by latest change
gcc/ada/ChangeLog:
* sem_aggr.adb (Resolve_Aggr_Expr): Always perform a full analysis
of the expression in SPARK mode.
Diff:
---
gcc/ada/sem_aggr.adb | 5 +++--
1 file changed, 3 insertions(+), 2 deletions(-)
diff --git a/gcc/ada/sem_aggr.adb b/gcc/ada/sem_aggr.adb
index 8cc00ad3b27a..3a82e6620c5e 100644
--- a/gcc/ada/sem_aggr.adb
+++ b/gcc/ada/sem_aggr.adb
@@ -2057,13 +2057,14 @@ package body Sem_Aggr is
-- In an iterated context, preanalyze a copy of the expression to
-- verify legality. We use a copy because the expression will be
-- analyzed anew when the enclosing aggregate is expanded and the
- -- construct is rewritten as a loop with a new index variable.
+ -- construct is rewritten as a loop with a new iteration variable.
+ -- This does not apply to SPARK mode, where expansion is skipped.
-- If the parent is a component association, we also temporarily
-- point its Expression field to the copy, because analysis may
-- expect this invariant to hold.
- if Iterated_Expr then
+ if Iterated_Expr and then not GNATprove_Mode then
declare
In_Assoc : constant Boolean :=
Nkind (Parent (Expr)) in N_Component_Association
