From: Eric Botcazou Date: Thu, 28 Nov 2024 22:05:52 +0000 (+0100) Subject: ada: Fix breakage of GNATprove introduced by latest change X-Git-Tag: basepoints/gcc-16~3358 X-Git-Url: http://git.ipfire.org/cgi-bin/gitweb.cgi?a=commitdiff_plain;h=5b30245800b1657f6c29212ca843c43bbfcffd20;p=thirdparty%2Fgcc.git 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 --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