Floating-point Bugs in Embedded GNU C Library
Soonho Kong, Sicun Gao, Edmund M. Clarke · 2013
We report serious bugs in floating-point computations for evaluating elementary functions in the Embedded GNU C Library. For instance, the sine function can return values larger than 1053 in certain rounding modes. Further investigation also exposed faulty implementations in the most re-cent version of the library, which seemingly fixed some bugs, but only by discarding user-specified rounding-mode requirements.