public inbox for gcc-bugs@sourceware.org
help / color / mirror / Atom feed
* [Bug ada/105303] New: Assertion_Policy (Pre => Ignore) executes precondition
@ 2022-04-18 15:10 simon at pushface dot org
2022-04-20 7:06 ` [Bug ada/105303] " ebotcazou at gcc dot gnu.org
` (2 more replies)
0 siblings, 3 replies; 4+ messages in thread
From: simon at pushface dot org @ 2022-04-18 15:10 UTC (permalink / raw)
To: gcc-bugs
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.
^ permalink raw reply [flat|nested] 4+ messages in thread
* [Bug ada/105303] Assertion_Policy (Pre => Ignore) executes precondition
2022-04-18 15:10 [Bug ada/105303] New: Assertion_Policy (Pre => Ignore) executes precondition simon at pushface dot org
@ 2022-04-20 7:06 ` ebotcazou at gcc dot gnu.org
2022-05-30 8:29 ` cvs-commit at gcc dot gnu.org
2022-05-30 8:35 ` charlet at gcc dot gnu.org
2 siblings, 0 replies; 4+ messages in thread
From: ebotcazou at gcc dot gnu.org @ 2022-04-20 7:06 UTC (permalink / raw)
To: gcc-bugs
https://gcc.gnu.org/bugzilla/show_bug.cgi?id=105303
Eric Botcazou <ebotcazou at gcc dot gnu.org> changed:
What |Removed |Added
----------------------------------------------------------------------------
Ever confirmed|0 |1
Last reconfirmed| |2022-04-20
CC| |ebotcazou at gcc dot gnu.org
Status|UNCONFIRMED |NEW
--- Comment #1 from Eric Botcazou <ebotcazou at gcc dot gnu.org> ---
Confusing indeed.
^ permalink raw reply [flat|nested] 4+ messages in thread
* [Bug ada/105303] Assertion_Policy (Pre => Ignore) executes precondition
2022-04-18 15:10 [Bug ada/105303] New: Assertion_Policy (Pre => Ignore) executes precondition simon at pushface dot org
2022-04-20 7:06 ` [Bug ada/105303] " ebotcazou at gcc dot gnu.org
@ 2022-05-30 8:29 ` cvs-commit at gcc dot gnu.org
2022-05-30 8:35 ` charlet at gcc dot gnu.org
2 siblings, 0 replies; 4+ messages in thread
From: cvs-commit at gcc dot gnu.org @ 2022-05-30 8:29 UTC (permalink / raw)
To: gcc-bugs
https://gcc.gnu.org/bugzilla/show_bug.cgi?id=105303
--- Comment #2 from CVS Commits <cvs-commit at gcc dot gnu.org> ---
The master branch has been updated by Pierre-Marie de Rodat
<pmderodat@gcc.gnu.org>:
https://gcc.gnu.org/g:5b7630f2f266346173eb2172a9a96e925010afc5
commit r13-826-g5b7630f2f266346173eb2172a9a96e925010afc5
Author: Yannick Moy <moy@adacore.com>
Date: Tue Apr 19 14:37:58 2022 +0200
[Ada] PR ada/105303 Fix use of Assertion_Policy in internal generics unit
The internal unit System.Generic_Array_Operations defines only generic
subprograms. Thus, pragma Assertion_Policy inside the spec has no
effect, as each instantiation is only subject to the assertion policy at
the program point of the instantiation. Remove this confusing pragma,
and add the pragma inside each generic body making use of additional
assertions or ghost code, so that running time of instantiations is not
impacted by assertions meant for formal verification.
gcc/ada/
PR ada/105303
* libgnat/s-gearop.adb: Add pragma Assertion_Policy in generic
bodies making use of additional assertions or ghost code.
* libgnat/s-gearop.ads: Remove confusing Assertion_Policy.
^ permalink raw reply [flat|nested] 4+ messages in thread
* [Bug ada/105303] Assertion_Policy (Pre => Ignore) executes precondition
2022-04-18 15:10 [Bug ada/105303] New: Assertion_Policy (Pre => Ignore) executes precondition simon at pushface dot org
2022-04-20 7:06 ` [Bug ada/105303] " ebotcazou at gcc dot gnu.org
2022-05-30 8:29 ` cvs-commit at gcc dot gnu.org
@ 2022-05-30 8:35 ` charlet at gcc dot gnu.org
2 siblings, 0 replies; 4+ messages in thread
From: charlet at gcc dot gnu.org @ 2022-05-30 8:35 UTC (permalink / raw)
To: gcc-bugs
https://gcc.gnu.org/bugzilla/show_bug.cgi?id=105303
Arnaud Charlet <charlet at gcc dot gnu.org> changed:
What |Removed |Added
----------------------------------------------------------------------------
Status|NEW |RESOLVED
CC| |charlet at gcc dot gnu.org
Resolution|--- |FIXED
Target Milestone|--- |13.0
--- Comment #3 from Arnaud Charlet <charlet at gcc dot gnu.org> ---
fixed on master
^ permalink raw reply [flat|nested] 4+ messages in thread
end of thread, other threads:[~2022-05-30 8:35 UTC | newest]
Thread overview: 4+ messages (download: mbox.gz / follow: Atom feed)
-- links below jump to the message on this page --
2022-04-18 15:10 [Bug ada/105303] New: Assertion_Policy (Pre => Ignore) executes precondition simon at pushface dot org
2022-04-20 7:06 ` [Bug ada/105303] " ebotcazou at gcc dot gnu.org
2022-05-30 8:29 ` cvs-commit at gcc dot gnu.org
2022-05-30 8:35 ` charlet at gcc dot gnu.org
This is a public inbox, see mirroring instructions
for how to clone and mirror all data and code used for this inbox;
as well as URLs for read-only IMAP folder(s) and NNTP newsgroup(s).