Clarifications w.r.t. floating-point

Question 1

In section 2.2.3 (Typing):

C types float and double are subtypes of type real .

Section 2.2.5. Real numbers and floating point numbers later explains that this is not entirely true:

Unlike the promotion of C integer types to mathematical integers, there are special float values that do not naturally map to a real number, namely the IEEE-754 special values for "not-a-number", +∞ and −∞. See below for a detailed discussion on such special values. However, remember that ACSL’s logic has only total functions. Thus, there are implicit promotion functions real_of_float and real_of_double whose results on the 3 values above is left unspecified.

Maybe a small footnote or mention in 2.2.3 could help avoiding hasty interpretations.

Question 2

It is unfortunate that the \sign predicate is not applicable to NaN. The signbit equivalent in C99 does accept NaN. This complicates writing an ACSL specification for that function. If there are advantages to making \sign partial, maybe they could be listed in the document (or should there be a "ACSL Rationale" with such details?).

Question 3

Floating-point constants and operations are interpreted as mathematical real numbers: a C variable of type float or double is implicitly promoted to a real.

Does that mean that one cannot write -0.0 in ACSL (otherwise it is converted to the real zero, which is unsigned)?

acsl-language / acsl