Re: PR 23046. Folding predicates involving TYPE_MAX_VALUE/TYPE_MIN_VALUE (Ada RFC)

[Florian Weimer <fw at deneb dot enyo dot de>]

* Richard Kenner:

>      Both ARM 13.9.1 and the GNAT User Guide (in Section 3.2.4 Validity
>      Checking) require that such reads are NOT erroneous.
>
> It depends what "such reads" mean.  13.9.1(12) clearly says that the
> result of an Unchecked_Conversion is erroneous if it isn't a valid
> representation.  There are some cases, however, where an out-of-range
> value is a bounded error instead of being erroneous.
>
> However, note 20 (13.9.2) says that 'Valid is not considered a "read"
> and hence its use is not erroneous.

I'm sorry for my rude discussion style.  I was a bit frustrated
because of some unrelated matters.

I think the GNAT documentation makes additional guarantees.  If you
think this is wrong, the documentation can be fixed, of course.  In
addition, the first example in PR21573 follows your advice and applies
'Valid to the result of an instantiation of Ada.Unchecked_Conversion.
This still doesn't work.

If this still doesn't convince you, here's an example which doesn't
use Ada.Unchecked_Conversion at all.

--  Another test case for PR21573.  Note that if PR23354 is fixed and
--  X is initialized to a different value, this test case might no
--  longer check the same bug (but it should still print SUCCESS).
--  (The Bug3_P package is necessary to prevent compile-time
--  evaluation.)

pragma Normalize_Scalars;

with Bug3_P; use Bug3_P;

procedure Bug3 is

   X : U;
   --  The subtype causes X to be initialized with 0, according to the 
   --  current Normalize_Scalars rules.

begin
   Test (X);
end Bug3;

with Ada.Text_IO; use Ada.Text_IO;

package Bug3_P is

   type T is (A, B, C, D);
   for T'Size use 8;
   for T use (A => 2, B => 3, C => 5, D => 7);

   subtype U is T range B .. D;

   procedure Test (X : T);

end Bug3_P;

package body Bug3_P is

   procedure Test (X : T) is
   begin
      --  Check with a debugger that X is zero at this point.
      if X'Valid then
         Put_Line ("FAIL");
      else
         Put_Line ("SUCCESS");
      end if;
   end Test;
end Bug3_P;