Handling of Signaling NaN in pow functions

Basile Starynkevitch basile@starynkevitch.net
Wed May 21 17:57:32 GMT 2025


On Wed, 2025-05-21 at 18:17 +0200, Lorrens Pantelis via Libc-help wrote:
> Dear libc mailing list people,
> 
> I’m currently working on simulating non-determinism in floating-point
> operations within Rust’s Miri interpreter
> (https://github.com/rust-lang/miri). Specifically, we simulate
> imprecision by adding a 16 ULP relative error to the outputs of some
> floating-point operations. However, for certain operations (e.g.,
> involving fixed outputs), this is not applicable. While handling these
> cases, we encountered interesting behavior with the `pow` function
> between glibc and musl.

A related tool is https://www-pequan.lip6.fr/cadna/

it works on C++ & C & Fortran code

With a significant amount of work, it might be extended to handle GCC Gimple
internal representation (e.g. by your GCC plugin -which should be open source
emitting Cadna compatible C++ code from GIMPLE representations)

https://frama-c.com/ and proprietary tools sold by
https://www.absint.com/products.htm could also be relevant.

Regards
-- 
Basile STARYNKEVITCH                            <basile@starynkevitch.net>
8 rue de la Faïencerie                       http://starynkevitch.net/Basile/  
92340 Bourg-la-Reine                         https://github.com/bstarynk
France                                https://github.com/RefPerSys/RefPerSys


More information about the Libc-help mailing list