Base type overflows integer range

[senier]

The following spec

package Foo is
   type Len is range 1 .. 16 with Size => 64;
   type Req is
       message
           Len : Len;
       end message;
end Foo;

fails to compile:

rflx-foo.ads:13:21: integer type definition bounds out of range

The reason is that the base type for Len is generated such that the constant for the upper range exceeds 2**64-1:

type Len_Base is range 0 .. 2**64 - 1 with Size => 64; 

Could we use a non-wrapping modular type as base type to simplify the issue?

[treiher]

I was not aware that a non-wrapping modular type in Ada exists. Is there an aspect for this purpose?

[senier]

Yes, I just have to look up its name every single time. It's a gnatprove annotation called No_Wrap_Around. See the docs for details.

[treiher]

Using a non-wrapping modular type seems to solve this issue, but leads to the issue seen in #182. So we have to fix #182 first.

[senier]

Thanks for trying. Yes, I was expecting #182 to be an issue her, too. In that ticket I already hypothesized that No_Wrap_Around may also be helpful.