Support of 'L' suffix for floating-point literals of type long double, and `D` for literals of type double

[maroneze]

Currently, in ACSL, the long double type is not mentioned at all. However, for better compatibility with code using it, it would be nice to support the L suffix in floating-point literals (e.g. 1.0L) for type long double, as is the case in C.

More generally, it would be nice if ACSL standardized the usage of the D suffix for literal floating-point constants of type double, as is the case in WG14 N1176, Extension for the programming language C to support decimal floating-point arithmetic. While the document is mainly related to decimal floating-point constants (which are rarely used), it mentions adding an extension to the parsing of floating-point literals:

An unsuffixed floating constant has type double. If suffixed by the letter f or F, it has type float. If suffixed by the letter d or D, it has type double. If suffixed by the letter l or L, it has type long double.

For information, the D suffix is accepted by GCC (which mostly ignores it, since unsuffixed floating-point literals in C already have type double), but not supported by other compilers, such as Clang and CompCert.

Still, considering that, in ACSL, unsuffixed floating-point literals have type real (unlike in C), adding support for the D suffix avoids casts in some cases.

For long doubles, the L suffix maintains consistency with C literals, minimizing surprise, and avoiding casts.

[pbaudin]

There is an example of use of the proposed suffixes showing first what is done for the L suffix of integer literals as a basis for comparison:

/*@ axiomatic A {

   logic integer i1 = 1;
// logic long    i  = 1;  // Rejected (e.g. a cast is needed)
   logic long    i2 = (long) 1;
   logic long    i3 = 1L; // Same as i2 definition

   logic real    a1 = 0.5;
// logic double  a  = 0.5;  // Rejected (e.g. a cast is needed)
   logic double  a2 = (double) 0.5;
   logic double  a3 = 0.5D; // Unsupported (that is the purpose of that issue):
                            // - equivalent to a2 definition.

   logic real    b1 = 0.1;
   logic double  b2 = (double) 0.1;
   logic double  b3 = 0.1D; // Unsupported (that is the purpose of that issue):
                            // - same as b2 definition, but in that case,
                            //   the usage of the notation 0.1D could lead to
                            //   a warning since the defined literal value differs to 0.1

   logic float       c3 = 0.5F; // Unsupported (that is the purpose of that issue)
   logic long double d3 = 0.5D; // Unsupported (that is the purpose of that issue)
}
*/

[pbaudin]

Note: this issue extends #11 to the three suffixes D, F and L.