gnatprove ICE: Storage_Error on an iterated component association in an expression function

Summary

gnatprove crashes with GNAT BUG DETECTED — Storage_Error stack overflow or erroneous memory access in the SPARK front-end (1.0 (spark)) when an expression function returns an array
aggregate written as an iterated component association.

Six-line reproducer, no recursion, no contracts, no dependencies:

package Case_D with SPARK_Mode is
   subtype Cnt is Natural range 1 .. 8;
   type Outp is array (Cnt) of Natural;
   function Build (C : Cnt) return Outp is
     ((for I in Cnt range 1 .. C => I));
end Case_D;

$ gnatprove -P p.gpr --mode=flow      # -gnat2022
+===========================GNAT BUG DETECTED==============================+
| 1.0 (spark) Storage_Error stack overflow or erroneous memory access      |
| Error detected at case_d.ads:5:17                                        |

Versions and platforms

Reproduced on three independent installations, two architectures:

host	OS / arch	install
1	macOS, arm64	Alire
2	Ubuntu, x86-64	Alire
3	Ubuntu, x86-64	standalone gnatprove-x86_64-linux-15.1.0-1

• gnatprove FSF 15.0, Why3 for gnatprove version 1.7.1+git
• GNAT 15.0.1 20250418 (prerelease)
• Compiled with -gnat2022

⚠ Not yet tested on any other gnatprove version — all three installations are FSF 15.0.
If this is already fixed on a newer release, please say so and I will confirm and close.

Why I think this is a bug rather than a documented limitation

The GNATprove Limitations
page lists, under Tool Limitations Leading to an Error Message:

• an iterated component association with an iterator specification (for … of) in an array
  aggregate (unsupported-iterator-in-component-assoc)
• an iterated element association in a container aggregate
  (unsupported-iterated-element-association)

The reproducer is neither: it is a loop parameter specification (for I in …) in an array
aggregate. If that form is also unsupported, the crash still seems wrong — that section documents
these as producing an error message.

Notes that may narrow it down

Bisection. The crash needs only the iterated component association. Three variants, all on
the same toolchain:

case	contains	result
A	recursive expression function with Subprogram_Variant, no aggregate	analyses cleanly to Phase 3
B	iterated aggregate calling a non-recursive function	crash
C	iterated aggregate calling a recursive function, no variant	crash
D	iterated aggregate, no call, no recursion, no variant (above)	crash

Raising the stack does not fix it — it removes the diagnostic. With ulimit -s unlimited
the GNAT BUG box disappears and gnatprove still exits 1 at Phase 2 with only:

Phase 2 of 3: generation of Global contracts ...
gnatprove: error during generation of Global contracts

The macOS diagnostic is much less useful than the Linux one. On arm64 macOS the same input
reports raised PROGRAM_ERROR : finalize/adjust raised exception with no source location;
Linux gives Storage_Error with file:line:column. The Linux output is the one worth acting on.

Possibly related, not the same: Ada Forum — "Bidimensional iterated array aggregate causes
gnat to crash"
(Oct 2024) — two-dimensional, and a GNAT crash rather than a SPARK front-end one.

Project file used

project P is
   for Source_Dirs use (".");
   for Object_Dir use "obj";
   package Compiler is for Default_Switches ("Ada") use ("-gnat2022"); end Compiler;
end P;

Reproduce the failure with the six-line case_d.ads example and p.gpr project using gnatprove -P p.gpr --mode=flow and -gnat2022. Compare the Phase 2 failure and Storage_Error with the documented limitation cases; done means this iterated component association no longer causes an internal crash and receives an appropriate result.