GNAT bug maybe?

Help
,
1

This is the minimum I could do to reproduce it, but I’m not sure it’s a bug in the compiler or my code is doing something that shouldn’t.

pragma Ada_2022;

with Interfaces;

package Core.Bug
  with SPARK_Mode => On
is

   subtype Data_Index is Positive range 1 .. 10;

   type Byte is new Interfaces.Unsigned_8;

   type Data_Array is array (Data_Index range <>) of Byte
   with Default_Component_Value => 0;

   type Some_Record (Data_Length : Positive) is record
      Data : Data_Array (1 .. Data_Length) := [others => <>];
   end record;

   function Test_Bug (Value : Byte) return Some_Record
   with
     Global => null,
     Post   =>
       (declare
          R : constant Some_Record := Test_Bug'Result;
        begin
          R.Data'Length = 1 and then Has_Value (R.Data, Value));

   function Has_Value (Data : Data_Array; Value : Byte) return Boolean
   is (Data (1) = Value)
   with Pre => Data'Length >= 1 and then Data'First = 1, Ghost;

end Core.Bug;

--  Body

pragma Ada_2022;

package body Core.Bug
  with SPARK_Mode => On
is

   function Test_Bug (Value : Byte) return Some_Record is
   begin
      return (Data_Length => 1, Data => [others => Value]);
   end Test_Bug;

end Core.Bug;

+===========================GNAT BUG DETECTED==============================+
| 15.2.0 (x86_64-pc-linux-gnu) in gimplify_expr, at gimplify.cc:20381 |
| Error detected around core-bug.ads:25:38|
| Compiling core-bug.adb|
| Please submit a bug report; see GCC Bugs - GNU Project . |
| 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. |
+==========================================================================+

Build with alr build --validation

1 Like