[PATCH] D143074: [LangRef] improve documentation of SNaN in the default FP environment

Wed Feb 1 08:32:07 PST 2023

RalfJung added a comment.

> No, arithmetic operations cannot produce signaling nans. Signaling nans only come from initialization.

In LLVM, arithmetic operations can produce signaling nans: `x * 1.0` can be optimized to `x`, so if `x` was a signalling NaN that will be the output of the multiplication.
(Maybe we are using the term "produce" differently here? I meant it as "can be the output of".)

> I think that is how it would be specified in Alive2 terminology, but I'm happy to avoid the controversy if possible!

No, in Alive2 this would be non-determinism, which is more like `freeze undef` than `undef`.

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

https://reviews.llvm.org/D143074