CompCert
CompCert copied to clipboard
AbsInt
The CompCert formally-verified C compiler
This is a small clean up that removes the already rare uses of the proof irrelevance axiom.
These changes introduce a more structured namespace for memory blocks: a block id can either be a global `ident` (new), or a dynamically allocated `positive` (as before). Using this approach,...
The main reason for the patches in this branch is to strengthen the `Locmap.gss_reg` lemma, which used to claim that any value can be written to and recovered from any...
Since `PrintCsyntax` is dual-licensed, I expected it could be used in a GPL project. But according to `tools/modorder .depend.extr cfrontend/PrintCsyntax.cmx` (using opam `coq-compcert` v3.8 package, in case it matters), it...
Certain targets (ARM…) are are available as several sub-targets with different instruction sets. CompCert, when calling gcc as preprocessor, should pass the appropriate `-march=` option (*). Maybe there should be...
C11 defines the `_Thread_local` keyword, and GCC has long had the `__thread` modifier. They define data to reside in the _thread-local storage_. Basically, if `x` is thread-local, then it behaves...
In the case of a struct passing using `SP_split_args`, this code of `cparser/StructPassing.ml` is actually misleading ```ocaml let classify_param env ty = if is_composite_type env ty then begin match !struct_passing_style...
I ran into an issue recently in which CompCert could not compile a `struct` with bit-field members of type `long`. It was straightforward to find where this restriction was enforced,...
Example code: ```c #include struct int_def { const char *s; const int ints[]; }; static const struct int_def my_ints = { .s = "my ints", .ints = {0, 3, 7,...
Bit-field initialization via `-fbitfields` emulation leads to undefined behavior in most cases. It would be nice to be able to do it without having to resort to a static-storage variable....
