https://gcc.gnu.org/bugzilla/show_bug.cgi?id=108447
--- Comment #3 from Andrew Macleod <amacleod at redhat dot com> ---
Those specialized relations are handled within the floating point range-ops
code iirc. We established that none of the other floating point relations
needed to be exposed to non-floating point code.
The frange class has all the knowledge of NAN and such, and the oracle is
suppose to invokes a routine called "validate_relation" which invokes a fold
operation to find out if the operation is actually valid between 2 operands.
(this is how we were suppose to determine x == x may not be true)
I can't seem to find any application of the routine tho... It was supplied so
floating point x == x would not short-circuit in the oracle as it was
symbolically true. I'll have to sync with aldy and see what we currently do,
They theoretical application here would be to apply it to the
intersection/union routines too. ie
Registering value_relation (x_8(D) >= y_9(D)) on (2->3)
Intersecting with existing (x_8(D) <= y_9(D)) to produce (x_8(D) == y_9(D))
if we can determine that x == y isnt true.. or that somehow it has different
floating point characteristics from the inputs...
we'll get back to you.
