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