C99 support

[vogler]

CIL supports C90/GNU90 ("the CIL front-end is able to process not only ANSI-C programs but also those using Microsoft C or GNU C extensions")
Ugly examples: http://cil-project.github.io/cil/doc/html/cil/cil016.html

To check/implement from wiki/C99:

• inline functions
• intermingled declarations and code: variable declaration is no longer restricted to file scope or the start of a compound statement (block), facilitating static single assignment form
• several new data types
  • long long int long long
  • optional extended integer types (e.g. __int128, not supported by GCC, see here)
  • an explicit boolean data type _Bool (fixed by Unsoundness with regard to C99 _Bool type analyzer#76)
  • complex number types float _Complex, double _Complex, long double _Complex
    • types are parsed (somewhat incorrectly as when printing again it is turned into __attribute__ ((__complex__)) when it should really only be __complex__)
    • literals were added
  • improved support for IEEE floating point: see C99 fixed-width integer and floating-point types #8: fixed-width floats _Float128..., "float_t/double_t

From cil.mli:

(** Various kinds of integers *)
and ikind =
    IChar       (** [char] *)
  | ISChar      (** [signed char] *)
  | IUChar      (** [unsigned char] *)
  | IBool       (** [_Bool (C99)] *)
  | IInt        (** [int] *)
  | IUInt       (** [unsigned int] *)
  | IShort      (** [short] *)
  | IUShort     (** [unsigned short] *)
  | ILong       (** [long] *)
  | IULong      (** [unsigned long] *)
  | ILongLong   (** [long long] (or [_int64] on Microsoft Visual C) *)
  | IULongLong  (** [unsigned long long] (or [unsigned _int64] on Microsoft
                    Visual C) *)
(** Various kinds of floating-point numbers*)
and fkind =
    FFloat      (** [float] *)
  | FDouble     (** [double] *)
  | FLongDouble (** [long double] *)

• variable-length arrays (although subsequently relegated in C11 to a conditional feature that implementations are not required to support)
• flexible array members (a[] at end of struct, take up rest of malloc'ed space, example), already worked
• support for one-line comments beginning with //, as in BCPL, C++ and Java [nothing to do]
• new library functions, such as snprintf [nothing to do]
• new headers, such as <stdbool.h>, <complex.h>, <tgmath.h>, and <inttypes.h>
• type-generic math (macro) functions, in <tgmath.h>, which select a math library function based upon float, double, or long double arguments, etc.
  • The preprocessor expands those but turned it into something we could not parse correctly. See here for an explanation of what the expanded code does.
• designated initializers (for example, initializing a structure by field names: struct point p = { .x = 1, .y = 2 };)[5]
• compound literals (for instance, it is possible to construct structures in function calls: function((struct x) {1, 2}))[6]
• support for variadic macros (macros with a variable number of arguments) [nothing to do (cpp)]
• restrict qualification allows more aggressive code optimization, removing compile-time array access advantages previously held by FORTRAN over ANSI C (see here) [turned into attribute __restrict by CIL]
• universal character names, which allows user variables to contain other characters than the standard character set (see PR Support for C11 #24 ) example
• keyword static in array indices in parameter declarations [Fixed here? 804699f]

[michael-schwarz]

Tests for these things can be added to this branch of CIL: https://github.com/goblint/cil/tree/c99

[michael-schwarz]

The support for inline is not 100% complete, e.g. if I have two files like this:

#include "stdio.h"
void add(int x, int y) {
    printf("Called non-inline\n");
}

#include "stdio.h"
inline void add(int i, int j) { printf("Called inline\n"); }

int main() {
  add(4, 5);
  return 0;
}

For C99 (and its inline semantic) you can gcc -std=c99 -pedantic 01.c 02.c and it will work without any issues. Depending on the level of optimization used, either one of the add functions is the one that is called.

If we run cilly with --merge though, CIL will complain with

combine-c99inline_2.c:2: Warning: Formal i not shared (expecting name x) in add
  Context : GFun(add)
combine-c99inline_2.c:2: Warning: Formal j not shared (expecting name y) in add
  Context : GFun(add)
Bug: CIL's internal data structures are inconsistent (see the warnings above).  This may be a bug in CIL.

For GNU89 the example above does not compile.

It is a limitation, but I don't think it is obvious how this should be fixed and also not how common this actually is.

Relevant link on inline in GNU89 dialect vs C99.

[michael-schwarz]

tgmath.h and _Complex works as of 673fd85