Notation for non-finite floating-point values

[maroneze]

Constants such as \plus_infinity, \minus_infinity and \NaN would be useful to have in ACSL.

Currently, specifications dealing with non-finite floating-point values must resort to using expressions such as 1.0f/0.0 or 0.0f/0.0, or they need to include math.h and rely on C99 macros such as INFINITY and NAN. The specifications become much less clear and may induce unnecessary dependency on libc headers.

[vprevosto]

A few points:

• technically, there exist quite a few values for NaN (2^53 for double) [very minor, though]
• you seem to imply that these constants should have type float. This seems consistent with the macros from math.h, but raises the question of having \plus_infinity_double and so on.
• What is the intended use of these constants apart from an equality, for which predicates \is_plus_infinity, \is_minus_infinity and \is_NaN already exist, both for double and float?

[maroneze]

Indeed, I couldn't find yet an example where ensures \result == \plus_infinity could not be replaced with ensures \is_plus_infinity(\result), or something similar (assuming the plugins handle this case precisely).

I think the only case where these constants seem necessary is when trying to use INFINITY/NAN in logic functions, e.g.:

logic float _infinity(ℤ x) = \plus_infinity;
logic float _nan(ℤ x) = \NaN;

With definitions such as the above, it is possible to use the same macros for INFINITY/NAN in logic functions as well as in other specifications, assuming the underlying C library (e.g. Frama-C's) uses a compatible definition for the macro.