- 01 Jun, 2021 13 commits
-
-
Cyril SIX authored
-
Cyril SIX authored
-
Cyril SIX authored
-
Cyril SIX authored
-
Cyril SIX authored
-
Cyril SIX authored
-
Cyril SIX authored
-
Cyril SIX authored
-
Xavier Leroy authored
Before, the line number had to start with a nonzero digit. However, the GCC 11 preprocessor was observed to produce `# 0 ...` directives. Fixes: #398
-
Cyril SIX authored
-
Cyril SIX authored
-
Cyril SIX authored
-
Léo Gourdin authored
-
- 31 May, 2021 2 commits
-
-
Léo Gourdin authored
-
Léo Gourdin authored
-
- 29 May, 2021 1 commit
-
-
Léo Gourdin authored
-
- 19 May, 2021 2 commits
-
-
Léo Gourdin authored
-
Léo Gourdin authored
-
- 18 May, 2021 1 commit
-
-
Léo Gourdin authored
-
- 13 May, 2021 1 commit
-
-
Xavier Leroy authored
E.g. __builtin_bswap. Update Asm modeling of builtins accordingly.
-
- 11 May, 2021 4 commits
-
-
David Monniaux authored
-
David Monniaux authored
-
David Monniaux authored
-
David Monniaux authored
-
- 10 May, 2021 5 commits
-
-
David Monniaux authored
-
David Monniaux authored
-
David Monniaux authored
-
David Monniaux authored
-
Xavier Leroy authored
-
- 09 May, 2021 2 commits
-
-
Xavier Leroy authored
-
Xavier Leroy authored
Also: limit the max width of the page, to avoid very long lines.
-
- 08 May, 2021 2 commits
-
-
Xavier Leroy authored
-
Xavier Leroy authored
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.
-
- 04 May, 2021 1 commit
-
-
Cyril SIX authored
-
- 02 May, 2021 4 commits
-
-
Xavier Leroy authored
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
-
Xavier Leroy authored
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.
-
Xavier Leroy authored
Not yet used for optimizations.
-
Xavier Leroy authored
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>
-
- 30 Apr, 2021 1 commit
-
-
David Monniaux authored
-
- 29 Apr, 2021 1 commit
-
-
Xavier Leroy authored
-