[PATCH] D139312: ValueTracking: Teach CannotBeOrderedLessThanZero about copysign

Mon Dec 5 06:07:27 PST 2022

nlopes added a comment.

In D139312#3970743 <https://reviews.llvm.org/D139312#3970743>, @foad wrote:

> Seems reasonable. Can we get alive2 proofs for floating point things like this yet @nlopes?

Most FP stuff should be working now. Exceptions include: some fast-math flags (arcp/contract/reassoc/afn), exceptions, and some intrinsics. The rest should all be working; if not please file a bug report :)

In D139312#3970765 <https://reviews.llvm.org/D139312#3970765>, @arsenm wrote:

> Alive2 says this is ok and seems to understand copysign. For some of the other complex functions in other patches, it doesn’t complain but it also doesn’t complain when I try things that are obviously wrong

As noted above, most FP should be working. If Alive2 misses a bug, please do file a bug report. Alive2 is not supposed to miss (almost no) bugs.

CHANGES SINCE LAST ACTION
  https://reviews.llvm.org/D139312/new/

https://reviews.llvm.org/D139312