C99 fixed-width integer and floating-point types

[michael-schwarz]

When running tests such as testrun/math1 on a machine with a newer version of glibc, we produce a parse error, that seems to be related to the headers using the float128 type.

We encountered this not just with toy programs, but also with real-world examples.

Find some way of still being able to parse these headers, probably by introducing a new typ for float128. On the Goblint side of things, we can just treat it (almost) like normal floats as we don't do anything for them anyway.

Related links:

• Fails to compile when including <math.h> of recent glibc samee/obliv-c#48 (other project using CIL that has this problem)
• NixOS/nixpkgs@7f8bc04 (patch for the lexer & parser to handle float128 and complex)

[vogler]

That should be enough to parse those things, but I wonder whether we need all of them in typeSpecifier.
What's the difference between __int64 and int64_t or __float128 and Float128? The former are probably only extensions, while the latter were added in C99, see https://en.wikipedia.org/wiki/C_data_types#Fixed-width_integer_types. Should add all those to the lexer/parser as well, I guess.
Also float_t/double_t:

The C99 standard includes new real floating-point types float_t and double_t, defined in <math.h>. They correspond to the types used for the intermediate results of floating-point expressions when FLT_EVAL_METHOD is 0, 1, or 2. These types may be wider than long double.

At least those fixed width types are unambiguous. What we do for the more common int, long, float, double is another problem. We just assume they have the size of the machine CIL was built on, which might not be the case for the environment the analyzed program will run in.

_build/machdep.ml:

let gcc = {
(* Generated by code in src/machdep-ml.c *)
	 version_major    = 9;
	 version_minor    = 2;
	 version          = "9.2.0";
	 sizeof_short          = 2;
	 sizeof_int            = 4;
	 sizeof_bool           = 1;
	 sizeof_long           = 8;
	 sizeof_longlong       = 8;
	 sizeof_ptr            = 8;
	 sizeof_float          = 4;
	 sizeof_double         = 8;
	 sizeof_longdouble     = 16;
	 sizeof_void           = 1;
	 sizeof_fun            = 1;
	 size_t                = "unsigned long";
	 wchar_t               = "int";
	 alignof_short         = 2;
	 alignof_int           = 4;
	 alignof_bool          = 1;
	 alignof_long          = 8;
	 alignof_longlong      = 8;
	 alignof_ptr           = 8;
	 alignof_enum          = 4;
	 alignof_float         = 4;
	 alignof_double        = 8;
	 alignof_longdouble    = 16;
	 alignof_str           = 1;
	 alignof_fun           = 1;
	 alignof_aligned       = 16;
	 char_is_unsigned      = false;
	 const_string_literals = true;
	 underscore_name       = true;
	 __builtin_va_list     = true;
	 __thread_is_keyword   = true;
	 little_endian         = true;
}

So on my machine long double == __float128 == Float128.

[vogler]

Ok, those int64_t etc. are defined in <inttypes.h>, so they don't need to be added.
However, for floats there's apparently no such header and the types from here should be added. TODO how many? N=8,16,32,64,128?
https://gcc.gnu.org/onlinedocs/gcc/Floating-Types.html
https://stackoverflow.com/questions/2524737/fixed-size-floating-point-types

[michael-schwarz]

I added _Float128 for now, so I can use the math1 example to see which other changes are required.

Right now, we get Error: Invalid combination of type specifiers.

[michael-schwarz]

With #10, #60, #68, and #49 everything here seems to be covered.

The fixed-width integer types seem to be just type-defed to more usual types in GCC as evidenced by 9e3b8c6 (at least for Linux).

I'll wait and see what OS X CI says, but otherwise I think we can close this issue.