Dynamic_Predicate failure -> Assertion_Error?

Dynamic_Predicate failure -> Assertion_Error?

[Jacob Sparre Andersen]

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."

Re: Dynamic_Predicate failure -> Assertion_Error?

[Randy Brukardt]

"Jacob Sparre Andersen" <jacob@jacob-sparre.dk> wrote in message 
news:87tx8tncss.fsf@adaheads.sparre-andersen.dk...
>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?

No, but the reason is subtle. (I fooled around with your test program for a 
while before I figured out the problem.)

And on top of that, there is some weird behavior.

If one removes the 1 from the loop (so it starts at 2), then I get:

   2 is a prime.
   3 is a prime.
   4 is a prime.
   5 is a prime.
   6 is a prime.
   ...

11.4.2(10.4/3) says that "if no such Assertion_Policy pragma exists, the 
policy is implementation-defined". That means, that if you want to ensure 
assertions to be checked (in an ACATS test or in your code), you need a 
pragma Assertion_Policy(Check) somewhere. GNAT seems to default to Ignore or 
something similar; definitely not full Check.

If you put that pragma into Test_Prime:

with Ada.Assertions, Ada.Text_IO;
with Primes;
procedure TestP is
  pragma Assertion_Policy(Check); -- <<---!!!!
  use Primes;
  P : Prime;
...

Then I get the following if the loop starts at 2:

 2 is a prime.
 3 is a prime.
 4 is not a prime (predicate).
 5 is a prime.
 6 is not a prime (predicate).
 7 is a prime.
...

But if the loop starts at 1, I get your original result.

Your guess is as good as mine as to why that would be. It's obviously some 
sort of weird compiler bug. It seems to be keeping the first exception 
raised through the loop and reusing it on subsequent iterations, rather that 
treating each separately as one would hope.

> 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)?

Well, as this is a weird compiler bug and not an outright mistake in the 
implementation (since it depends solely on the bounds of the loop - it works 
properly when no loop is involved), it's not a good candidate for the ACATS. 
Especially as it seems to be more likely an exception processing problem 
rather than an assertion problem.

Moreover, AI12-0054-2 and AI12-0071-1 extensively changed the rules in this 
area (they were much too loose for practical usability). There will need to 
be tests for those AIs, but they have to wait until AI12-0071-1 is approved 
by WG 9 (expected in June).

That said, we'd love to have more tests for Ada 2012's contract assertions. 
A variety of programming styles helps the quality of the ACATS. Contact me 
at agent@ada-auth.org if you need more information, or see Annex E in the 
ACATS documentation (http://www.ada-auth.org/acats-files/3.1/docs/UG-E.HTM).

                                           Randy.