diff options
| author | Eric Botcazou <ebotcazou@adacore.com> | 2024-11-28 23:05:52 +0100 |
|---|---|---|
| committer | Marc Poulhiès <dkm@gcc.gnu.org> | 2024-12-13 09:36:01 +0100 |
| commit | 5b30245800b1657f6c29212ca843c43bbfcffd20 (patch) | |
| tree | d238120f7ca3d41b2b7889aff76d45639db991b3 /gcc | |
| parent | 95711d6ba78efaf1b090185f7419518dcb287395 (diff) | |
| download | gcc-5b30245800b1657f6c29212ca843c43bbfcffd20.zip gcc-5b30245800b1657f6c29212ca843c43bbfcffd20.tar.gz gcc-5b30245800b1657f6c29212ca843c43bbfcffd20.tar.bz2 | |
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.
Diffstat (limited to 'gcc')
| -rw-r--r-- | gcc/ada/sem_aggr.adb | 5 |
1 files changed, 3 insertions, 2 deletions
diff --git a/gcc/ada/sem_aggr.adb b/gcc/ada/sem_aggr.adb index 8cc00ad..3a82e66 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 |