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. | +==========================================================================+