By default in Frama-C, NaN values are considered as errors and should not be
produced by calls to library functions.