So in the case above, the set of permissible values is
[1, 0x7fffffff] after the addition, right?
Well, not quite. The addition isn't done in type X, but in type X'Base,
which does not have the restricted TYPE_{MIN,MAX}_VALUES. But, as we've all
said, there are conversions in there so VRP can use it's normal logic.
If you have a different case:
type X is range 0 .. 16#7fff_ffff#;
Y, Z : X;
Z : = Y + 1;
you can then conclude that [1, 0x7fffffff] is the permissible values
for Z. But what the last statement actually becomes (in pseudo-C) is:
Z = (X) ((X'Base) Y + (X'Base) 1);
So the above is not the range for the *addition* (which has the type
unrestricted by the bounds), just for Z. The reason this distinction is
relevant is that if checking is enabled, the conversion to X will involve
a bounds check. VRP should be able to deduce that the bounds check can
be replaced by "/= 0x80000000" and that is indeed a correct deduction.
