https://gcc.gnu.org/bugzilla/show_bug.cgi?id=105303
Bug ID: 105303
Summary: Assertion_Policy (Pre => Ignore) executes precondition
Product: gcc
Version: 12.0
Status: UNCONFIRMED
Severity: normal
Priority: P3
Component: ada
Assignee: unassigned at gcc dot gnu.org
Reporter: simon at pushface dot org
Target Milestone: ---
System.Generic_Array_Operations starts with
-- Preconditions in this unit are meant for analysis only, not for run-time
-- checking, so that the expected exceptions are raised. This is enforced
-- by setting the corresponding assertion policy to Ignore. Postconditions
-- and contract cases should not be executed at runtime as well, in order
-- not to slow down the execution of these functions.
pragma Assertion_Policy (Pre => Ignore,
Post => Ignore,
Contract_Cases => Ignore,
Ghost => Ignore);
and yet, given this clearly wrong code (compiled with -gnata)
with System.Generic_Array_Operations;
procedure Transposition is
type Matrix is array (Integer range <>, Integer range <>) of Float;
procedure Transpose is new System.Generic_Array_Operations.Transpose
(Scalar => Float,
Matrix => Matrix);
Input : Matrix (1 .. 3, 1 .. 4);
Output : Matrix (1 .. 3, 1 .. 2);
begin
Transpose (Input, Output);
end Transposition;
Ada.Assertions.Assertion_Error is in fact raised, contrary to ARM2012
11.4.2(10):
$ ./transposition
raised ADA.ASSERTIONS.ASSERTION_ERROR : failed precondition from
s-gearop.ads:569 instantiated at transposition.adb:4
The comment noted above is confusing, if not wrong:
"Preconditions ... not meant for runtime checking, so that the expected
exceptions are raised" -- the checks should not be performed, and the
exceptions should not be raised.
