[Bug ada/128034] New: GNAT 16.2 crashes if Assume pragma with quantified expression placed after array overlay

[cthowie at netzero dot net via Gcc-bugs]

https://gcc.gnu.org/bugzilla/show_bug.cgi?id=128034

            Bug ID: 128034
           Summary: GNAT 16.2 crashes if Assume pragma with quantified
                    expression placed after array overlay
           Product: gcc
           Version: 16.2.0
            Status: UNCONFIRMED
          Severity: normal
          Priority: P3
         Component: ada
          Assignee: unassigned at gcc dot gnu.org
          Reporter: cthowie at netzero dot net
                CC: dkm at gcc dot gnu.org
  Target Milestone: ---

PLATFORM: GCC, GNAT 16.2 toolchain on Windows 10 Intel x64 using MSYS2

ISSUE: use of pragma Assume can crash the compiler in a trivial code sample
involving an array overlay followed by an Assume pragma that uses a quantified
expression across the array.

STEPS TO TRIGGER BUG:

1) Extract the 3 files, whose contents are listed below: main.adb,
   operations.ads, and operations.adb.

2) Run this command:   gnatmake main.adb

3) On my machine, the following compiler crash report is issued:

   $ gnatmake main.adb
   gcc -c operations.adb
   +===========================GNAT BUG DETECTED==============================+
   | 16.2.0 (x86_64-w64-mingw32) GCC error:                                   |
   | in gnat_to_gnu_entity, at ada/gcc-interface/decl.cc:489                  |
   | Error detected at operations.adb:9:14                                    |
   | Compiling operations.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.                                       |
   +==========================================================================+

4) To prevent the crash and get a successful compilation, simply comment out
the Assume pragma in the Trigger_Bug function:

      --pragma Assume (for all K in Ints'Range => Ints (K) >= 0);

   Or remove the quantified expression e.g.,

      pragma Assume (Ints (1) >= 0);

   thus proving the quantified expression has something to do with the bug.

HERE'S ADA CODE FOR THE 3 DEMONSTRATION FILES

----- operations.ads --------------------------

with System; use System;
package Operations is
   type Int_Array is array (Positive range <>) of Integer;
   function Trigger_Bug
     (Num_Ints : Positive; Ints_Addr : Address) return Integer;
end Operations;


----- operations.adb --------------------------

package body Operations is
   function Trigger_Bug
     (Num_Ints : Positive; Ints_Addr : Address) return Integer
   is
      Ints : Int_Array (1 .. Num_Ints)
      with Import, Address => Ints_Addr;
      pragma Assume (for all K in Ints'Range => Ints (K) >= 0);
   begin
      return Ints (1);
   end Trigger_Bug;
end Operations;


----- main.adb --------------------------

with Operations; use Operations;
procedure Main is
   A : Int_Array (1 .. 10);
begin
   A (1) := 99;
   A (2) := Trigger_Bug (A'Length, A'Address);
end Main;