Potential failing range checks not detected in model

[treiher]

We are unable to detect potential failing range checks in the model. Here is an example:

package Test is

   type A is mod 2 ** 32;

   type B is
      message
         C : A
            then D
               with Size => C * 8;
         D : Opaque;
      end message;

end Test;

rflx-test-generic_b.adb:78:72: medium: range check might fail, in instantiation at rflx-test-b.ads:6
rflx-test-generic_b.adb:97:56: medium: range check might fail, in instantiation at rflx-test-b.ads:6

 78                    Types.Bit_Length (Ctx.Cursors (F_C).Value.C_Value) * 8,
[...]
 96   function Field_Last (Ctx : Context; Fld : Field) return Types.Bit_Index is
 97     (Field_First (Ctx, Fld) + Field_Length (Ctx, Fld) - 1);

Bit_Length is defined as follows by default:

   type Length is new Natural;
   type Bit_Length is range 0 .. Length'Last * 8;

But a user is able to use a custom buffer type with another value range for its index (the upper limit of Index and Length must be equal). So I doubt we will be able to completely prevent such cases by adding a check to the model.