GitLab

Before, the line number had to start with a nonzero digit.  However,
the GCC 11 preprocessor was observed to produce `# 0 ...` directives.

Fixes: #398

E.g. __builtin_bswap.  Update Asm modeling of builtins accordingly.

Also: limit the max width of the page, to avoid very long lines.

The GPL makes sense for whole applications, but the dual-licensed Coq
and OCaml files are more like libraries to be combined with other
code, so the LGPL is more appropriate.

A bitfield assignment `x.b = f()` is expanded into a read-modify-write
on `x.carrier`.  Wrong results can occur if `x.carrier` is read before
the call to `f()`, and `f` itself modifies a bitfield with the same
carrier `x.carrier`.

In this temporary fix, we play on the evaluation order implemented by
the SimplExpr pass of CompCert (left-to-right for side-effecting
subexpression) to make sure the read part of the read-modify-write
sequence occurs after the evaluation of the right-hand side.

More substantial fixes will be considered later.

Fixes: #395

Not yet used for optimizations.

Actually, __builtin_expect is removed during C2C conversion, otherwise
the conversion to type "long" produces inefficient code on 64-bit platforms.

Not yet used for optimizations.

The following is correct but was causing a "wrong type for array initializer"
fatal error.

```
struct s { int n; int d[]; };
void f(void) { struct s x = {0}; }
```
Co-authored-by: Michael Schmidt <github@mschmidt.me>