CompCert
CompCert copied to clipboard
AbsInt
The CompCert formally-verified C compiler
The Coq team released Coq `8.16+rc1` on June 01, 2022. The corresponding Coq Platform release `2022.09` should be released before **September 15, 2022**. It can be delayed in case of...
Improves robustness in case of stronger (e)auto (see [coq/#16293](https://github.com/coq/coq/pull/16293)).
ccomp v3.11, v3.10, aarch64, -g3 -gdwarf-3: ``` typedef struct tt{ int i1:8; int i2:8; int i3:8; int i4:8; }tt; tt t; ``` (gdb) p t $1 = {i1 = 0,...
`Declare Scope` makes it possible to declare a new notation scope before adding notations to it. This construct has been available since Coq 8.12, and is recommended, to the point...
Dear CompCert developers, this is a proof-of-concept highlighting a full build of x86 using the Dune build system. The PR is not meant to be merged yet, but as a...
`__builtin_unreachable` is currently accepted, but seems to be compiled as a no-operation. Wouldn't it be reasonable, at LTL level, to compile it as a self-loop (`Nop` onto the same control...
By popular demand. The tail call optimization pass performed later in CompCert will not turn a call into a tail call if the function has stack-allocated data, because this might...
Looking at Compcert I'm trying to clarify if this project absolutely requires GCC or if it should work with Clang?
In this paper: (https://www.trojansource.codes/trojan-source.pdf) researchers from the University of Cambridge describe an attack which uses special Unicode characters to inject invisible or modified code. As far as I can tell...
The C standard allows a compiler to "contract" compound floating-point expressions by removing intermediate rounding points. Concretely, an expression `a*b+c` may be rewritten into `fma(a, b, c)`. It has come...