https://gcc.gnu.org/bugzilla/show_bug.cgi?id=107569
--- Comment #7 from Andrew Macleod <amacleod at redhat dot com> --- (In reply to Jakub Jelinek from comment #6) > __builtin_isfinite (x) is implemented as > ~UNGT_EXPR<ABS_EXPR<x>, DBL_MAX>. > So, if we have: > _3 = ABS_EXPR <x_2(D)>; > _4 = _3 u> 1.79769313486231570814527423731704356798070567525844996599e+308; > _5 = ~_4; > return _5; > for assume function, we should start with [1,1] assumption on _5, that > implies > _4 [0,0], and from UNGT_EXPR being false, we should derive that > _3 is [-inf, > 1.79769313486231570814527423731704356798070567525844996599e+308] and not NaN > (if any operand is NaN, UNGT_EXPR is true, it stands for unordered or > greater). > And from _3 being [-inf, > 1.79769313486231570814527423731704356798070567525844996599e+308] not NaN > we should derive that x_2(D) is > [-1.79769313486231570814527423731704356798070567525844996599e+308, > 1.79769313486231570814527423731704356798070567525844996599e+308] not NaN > (aka finite number). oh, we're talking different cases. lets se. x_2(D) -> [frange] double [-1.79769313486231570814527423731704356798070567525844996599e+308 (-0x0.fffffffffffff8p+1024), 1.79769313486231570814527423731704356798070567525844996599e+308 (0x0.fffffffffffff8p+1024)] +-NAN _3 -> [frange] double [-Inf, 1.79769313486231570814527423731704356798070567525844996599e+308 (0x0.fffffffffffff8p+1024)] _4 -> [irange] bool [0, 0] NONZERO 0x0 _5 -> [irange] bool [1, 1] so we arent getting that x_2 is not NaN. THat would be a failing of foperator_abs::op1_range to not add the nans if the LHS has no NaNs then? it looks like the range is correct, but non the NaN. So I guess there are 2 different issues in this PR. I was orignally looking at the second one.