C11 Support

[coslu]

CIL lacks support for various additions to the C language that come with the C11 specification. It would be beneficial to identify and implement features to improve CIL's support for C11.

To check/implement from wiki/C11:

• Alignment specification (_Alignas specifier, _Alignof operator, aligned_alloc function, <stdalign.h> header file).
• The _Noreturn function specifier and the <stdnoreturn.h> header file.
• Type-generic expressions using the _Generic keyword. For example, the following macro cbrt(x) translates to cbrtl(x), cbrt(x) or cbrtf(x) depending on the type of x:

  #define cbrt(x) _Generic((x), long double: cbrtl, \
                                default: cbrt, \
                                float: cbrtf)(x)

• Multi-threading support (_Thread_local storage-class specifier, <threads.h> header including thread creation/management functions, mutex, condition variable and thread-specific storage functionality, as well as <stdatomic.h> for atomic operations supporting the C11 memory model).
• Improved Unicode support based on the C Unicode Technical Report ISO/IEC TR 19769:2004 (char16_t and char32_t types for storing UTF-16/UTF-32 encoded data, including conversion functions in <uchar.h> and the corresponding u and U string literal prefixes, as well as the u8 prefix for UTF-8 encoded literals).
• Removal of the gets function, deprecated in the previous C language standard revision, ISO/IEC 9899:1999/Cor.3:2007(E).
• Bounds-checking interfaces (Annex K). (Nothing to be done, GCC chose not to implement it)
• Analyzability features (Annex L). (Nothing to be done, GCC chose not to implement it)
• More macros for querying the characteristics of floating point types, concerning subnormal floating point numbers and the number of decimal digits the type is able to store.
• Anonymous structures and unions, useful when unions and structures are nested, e.g. in
  struct T { int tag; union { float x; int n; }; };.
• Static assertions, which are evaluated during translation at a later phase than #if and #error, when types are understood by the translator.
• An exclusive create-and-open mode ("…x" suffix) for fopen. This behaves like O_CREAT|O_EXCL in POSIX, which is commonly used for lock files.
• The quick_exit function as a third way to terminate a program, intended to do at least minimal deinitialization if termination with exit fails.
• A new timespec_get function and corresponding structure in <time.h> with a degree of POSIX compatibility.
• Macros for the construction of complex values (partly because real + imaginary*I might not yield the expected value if imaginary is infinite or NaN).

[edwintorok]

The _Alignas implementation is incomplete (only parser, but doesn't change alignment), which causes goblint to fail to parse OCaml 5.0 domain_state.h with a static assertion failure (array length negative).
A workaround is to use the following, which seems to work (the GCC aligned attribute seems to have the desired effect and change alignment):

--set 'pre.cppflags[+]' -D'_Alignas(x)=__attribute__((__aligned__(x)))'

[michael-schwarz]

@edwintorok thanks for the information and the workaround. I'll try to fix this issue in CIL (shouldn't be too difficult if the equivalent GCC attribute works), but it'll likely be only after the holidays.

[edwintorok]

Thanks, no rush I can use the workaround meanwhile.