Meeting
[-INF, y_6(D) + -1] EQUIVALENCES: { z_5 } (1 elements)
and
[-INF(OVF), 30]
to
VARYING
optimally we'd be able to extract a conservative integer range from
the symbolic range - [-INF, +INF - 1] in this case - and meet them
to [-INF(OVF), +INF - 1] (assuming that y_6 did not overflow).
Meeting
[-INF, y_6(D) + -1] EQUIVALENCES: { z_5 } (1 elements)
and
[-INF(OVF), 30]
to
[-INF(OVF), y_6(D) + -1] EQUIVALENCES: { } (0 elements)
Found new range for z_1: [-INF(OVF), y_6(D) + -1]
is obviously wrong. We run into
else if ((operand_less_p (*vr0min, vr1max) == 1
|| operand_equal_p (*vr0min, vr1max, 0))
&& operand_less_p (vr1min, *vr0min) == 1)
{
/* ( [ ) ] or ( )[ ] */
if (*vr0type == VR_RANGE
&& vr1type == VR_RANGE)
*vr0min = vr1min;
where -INF < 30 and -INF(OVF) < -INF. But we have vr0max and vr1max unordered.
Thus we fail to verify that, assuming we've catched this case via
else if ((maxeq || operand_less_p (vr1max, *vr0max) == 1)
&& (mineq || operand_less_p (*vr0min, vr1min) == 1))
{
/* [ ( ) ] or [( ) ] or [ ( )] */
...
else if ((maxeq || operand_less_p (*vr0max, vr1max) == 1)
&& (mineq || operand_less_p (vr1min, *vr0min) == 1))
{
/* ( [ ] ) or ([ ] ) or ( [ ]) */
Fixing that does
Meeting
[-INF, y_6(D) + -1] EQUIVALENCES: { z_5 } (1 elements)
and
[-INF(OVF), 30]
to
VARYING
optimally we'd be able to extract a conservative integer range from
the symbolic range - [-INF, +INF - 1] in this case - and meet them
to [-INF(OVF), +INF - 1] (assuming that y_6 did not overflow).