[Bug ada/116089] New: GNATprove raises Program_Error for loop frame condition when calling function with Side_Effects

[cthowie at netzero dot net]

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

            Bug ID: 116089
           Summary: GNATprove raises Program_Error for loop frame
                    condition when calling function with Side_Effects
           Product: gcc
           Version: unknown
            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 14.1 toolchain on Windows 10 Intel x64 using MSYS2 (mingw64).
          GNATprove FSF 14.1

ISSUE: Putting a conditional function with Side_Effects in a simple loop
triggers Program_Error from GNATprove

TRIVIAL SUBPROGRAM DEMONSTRATING THE BUG:

      procedure Demo_Bug
      with SPARK_Mode
      is
         type Buffer is array (1 .. 10) of Integer;

         -- -- -- -- -- -- -- -- -- -- -- -- -- -- -- -- -- -- -- -- --

         function Test
           (B     : Buffer;
            Idx   : Positive;
            Found : out Positive)   --  force the use of Side_Effects
           return Boolean
         with No_Inline,
           Side_Effects,
           Always_Terminates,
           Pre => Idx in B'Range
         is
         begin
            if B (Idx) > 0 then
               Found := Idx;
               return True;
            end if;
            Found := B'Last + 1;
            return False;
         end Test;

         -- -- -- -- -- -- -- -- -- -- -- -- -- -- -- -- -- -- -- -- --

         Value  : Positive;
         A      : Buffer := (others => 0);
         Idx    : Positive;
         Result : Boolean;
      begin
         for Idx in A'Range loop
            Result := Test (A, Idx, Value);
            if not Result then
               exit;               --  RAISES Program_Error
            end if;
         end loop;
      end Demo_Bug;


BUILD INSTRUCTIONS:
Save the above example program to e.g., "demo_bug.adb" then run:

   gnatprove demo_bug.adb

I got this output:

$ gnatprove demo_bug.adb
No project file given, using default.gpr
Phase 1 of 3: generation of data representation information ...
Phase 2 of 3: generation of Global contracts ...
Phase 3 of 3: flow analysis and proof ...
error in computation of loop frame condition for demo_bug__value
+===========================GNAT BUG DETECTED==============================+
| 1.0 (spark) Program_Error gnat2why-expr-loops-inv.adb:1052 explicit raise|
| Error detected at demo_bug.adb:37:10                                     |
| Compiling C:\temp\GNATprove_Bug\demo_bug.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.                                       |
+==========================================================================+