From: Jacob Sparre Andersen <jacob@jacob-sparre.dk>
Subject: Dynamic_Predicate failure -> Assertion_Error?
Date: Tue, 13 May 2014 13:22:27 +0200
Date: 2014-05-13T13:22:27+02:00 [thread overview]
Message-ID: <87tx8tncss.fsf@adaheads.sparre-andersen.dk> (raw)
I am experimenting a bit with GNAT-GPL-2013 and some of the new features
in Ada 2012.
% cat primes.ads
package Primes is
subtype Prime is Integer range 2 .. Integer'Last
with Dynamic_Predicate
=> (for all N in 2 .. Prime - 1 => Prime mod N /= 0);
end Primes;
% cat test_primes.adb
with Ada.Assertions,
Ada.Text_IO;
with Primes;
procedure Test_Primes is
use Primes;
P : Prime;
begin
for I in 1 .. 25 loop
begin
P := I;
Ada.Text_IO.Put_Line (Prime'Image (P) & " is a prime.");
exception
when Constraint_Error =>
Ada.Text_IO.Put_Line (Integer'Image (I) &
" is not a prime (constraint).");
when Ada.Assertions.Assertion_Error =>
Ada.Text_IO.Put_Line (Integer'Image (I) &
" is not a prime (predicate).");
end;
end loop;
end Test_Primes;
% gnatmake -gnat12 -gnata -gnato -fstack-check test_primes
gcc -c -gnat12 -gnata -gnato -fstack-check test_primes.adb
gcc -c -gnat12 -gnata -gnato -fstack-check primes.ads
gnatbind -x test_primes.ali
gnatlink test_primes.ali -fstack-check
% ./test_primes
1 is not a prime (constraint).
2 is a prime.
3 is a prime.
4 is not a prime (constraint).
[...]
As I read 3.2.4(31/3) the raised exception for 4 should be
Assertion_Error and not Constraint_Error. Is this correct?
If I am correct, is there any likelihood that I could get a test for
this into ACATS (assuming that I can figure out how to formulate it
properly)?
Greetings,
Jacob
--
"I don't want to gain immortality in my works.
I want to gain it by not dying."
next reply other threads:[~2014-05-13 11:22 UTC|newest]
Thread overview: 2+ messages / expand[flat|nested] mbox.gz Atom feed top
2014-05-13 11:22 Jacob Sparre Andersen [this message]
2014-05-13 21:26 ` Dynamic_Predicate failure -> Assertion_Error? Randy Brukardt
replies disabled
This is a public inbox, see mirroring instructions
for how to clone and mirror all data and code used for this inbox