SPARK gnatprove 12.1.1: segfault: Ada 2022 array 'Image attribute

[ghost]

Running gnatprove 12.1.1 on a minimal test of using the Ada 2022 feature of 'Image attribute on an array triggers an EXCEPTION_ACCESS_VIOLATION message instructing me to report the bug.

There is no segfault when compiling and running the program normally without SPARK.

As gnatprove triggers the bug I am not sure if it should be reported to gcc.gnu.org/bugs, or here, or elsewhere.

The minimal test used:

--  proj1.adb
with Ada.Text_IO; use Ada.Text_IO;
pragma Extensions_Allowed (On);

procedure Proj1 with
   SPARK_Mode => On
is

   A : constant array (1 .. 3) of Positive := [3, 6, 9];

begin
   Put_Line ("A'Image: " & A'Image);
end Proj1;

Expected behavior: no segfault.

Observed behavior: this segfault:

gnatprove -PC:\spark\proj1\proj1.gpr -j0 -XADAFLAGS= --output=oneline --ide-progress-bar -u proj1.adb --level=0
Phase 1 of 2: generation of Global contracts ...
Phase 2 of 2: flow analysis and proof ...
+===========================GNAT BUG DETECTED==============================+
| 1.0 (spark) Program_Error EXCEPTION_ACCESS_VIOLATION                     |
| Error detected at proj1.adb:11:29                                        |
| Compiling C:\spark\proj1\src\proj1.adb                                   |
| Please submit a bug report; see https://gcc.gnu.org/bugs/ .              |
| Use a subject line meaningful to you and us to track the bug.            |
| Include the entire contents of this bug box in the report.               |
| Include the exact command that you entered.                              |
| Also include sources listed below.                                       |
+==========================================================================+

I'm using Alire. Here are my gnatprove and toolchain versions. I've elided output I think irrelevant:

C:\spark\proj1>alr show
[ ... ]
Dependencies (direct):
   gnatprove^12.1.1

C:\spark\proj1>alr version
APPLICATION
alr version:               1.2.1
libalire version:          1.2.1
compilation date:          2022-08-28 10:42:22
compiler version:          Community 2021 (20210519-103)

CONFIGURATION
[ ... ]
community index branch:    stable-1.2.1
compatible index versions: ^1.1 & <=1.2.1
[ ... ]
git+https://github.com/alire-project/alire-index#stable-1.2.1
toolchain assistant:       disabled
tool #1 gnat:              gnat_native=12.1.2
tool #2 gprbuild:          gprbuild=22.0.1

[ ... ]

SYSTEM
distribution:              MSYS2
host-arch:                 X86_64
os:                        WINDOWS
target:                    NATIVE
toolchain:                 USER
word-size:                 BITS_64

[kanigsson]

Thanks for your report. This issue is already fixed in the development version of gnatprove, though the current/expected behavior might not be what you want:

$ gnatprove 
No project file given, creating default.gpr
Phase 1 of 2: generation of Global contracts ...
Phase 2 of 2: flow analysis and proof ...

proj1.adb:11:29: error: attribute "Image" on non-scalar type is not yet supported
   11 |   Put_Line ("A'Image: " & A'Image);
      |                           ~^~~~~~
warning: no bodies have been analyzed by GNATprove
enable analysis of a non-generic body using SPARK_Mode
Summary logged in /home/kanig/tickets/40/gnatprove/gnatprove.out