https://gcc.gnu.org/bugzilla/show_bug.cgi?id=107569
--- Comment #10 from Jakub Jelinek <jakub at gcc dot gnu.org> ---
So:
--- gcc/range-op-float.cc.jj 2022-11-06 11:56:27.138137781 +0100
+++ gcc/range-op-float.cc 2022-11-08 18:13:18.026974667 +0100
@@ -1280,9 +1280,10 @@ foperator_abs::op1_range (frange &r, tre
return true;
// Then add the negative of each pair:
// ABS(op1) = [5,20] would yield op1 => [-20,-5][5,20].
- r.union_ (frange (type,
- real_value_negate (&positives.upper_bound ()),
- real_value_negate (&positives.lower_bound ())));
+ frange negatives (type, real_value_negate (&positives.upper_bound ()),
+ real_value_negate (&positives.lower_bound ()));
+ negatives.clear_nan ();
+ r.union_ (negatives);
return true;
}
fixes the abs backwards propagation, but for some reason it doesn't help to
help the assume case.
*.assumptions has:
x_2(D) -> [frange] double
[-1.79769313486231570814527423731704356798070567525844996599e+308
(-0x0.fffffffffffff8p+1024),
1.79769313486231570814527423731704356798070567525844996599e+3
08 (0x0.fffffffffffff8p+1024)]
but
# RANGE [frange] double
[-1.79769313486231570814527423731704356798070567525844996599e+308
(-0x0.fffffffffffff8p+1024),
1.79769313486231570814527423731704356798070567525844996599e+3
08 (0x0.fffffffffffff8p+1024)] +-NAN
double x_2(D) = x;
but then say vrp2:
_Z3bard._assume.0 assume inferred range of x_1(D) (param x) = [frange] double
[-1.79769313486231570814527423731704356798070567525844996599e+308
(-0x0.fffffffffffff8p+1024), 1.7976931
3486231570814527423731704356798070567525844996599e+308
(0x0.fffffffffffff8p+1024)] +-NAN
Global Exported: _3 = [frange] double [0.0 (0x0.0p+0),
1.79769313486231570814527423731704356798070567525844996599e+308
(0x0.fffffffffffff8p+1024)] +NAN
so it uses the range with +-NAN rather than without it.
