CompCert
CompCert copied to clipboard
AbsInt
The CompCert formally-verified C compiler
If compcert does not install `.v` and `.glob` files, the bug minimizer cannot minimize any bugs in projects that are built on top of compcert. Note that `coq_makefile`-made makefiles install...
See #526 for motivations. - Build `.glob` files in the same directory as the source `.v` file (Coq default) - Install `.glob` files along with `.vo` and `.v` files Fixes:...
This will allow https://github.com/coq/opam/tree/master/extra-dev/packages/coq-compcert/coq-compcert.dev to drop the patch that makes `./configure` compatible with unreleased / dev versions of menhir.
Appendix H of ISO C 2023 makes provisions for built-in binary floating-point types `_Float`_N_, where _N_ is the bit size of the type. Some C compilers and math libraries already...
Currently if an unrecognized warning is passed to CompCert, the compiler will error out. Clang will print a warning (they have a -Wunknown-warning-option) and continue compilation. I’d like to request...
Currently, unrecognized warning options `-Wsome-unknown-warning` are fatal errors. As suggested in #552, this PR makes sure that `-Wsome-unknown-warning` is a warning (by default), and that `-Wno-some-unknown-warning` is ignored. This is...
This PR adds support for generating position-independent executables (PIE), Position-independent code (PIC) and shared libraries for AArch64, RISC-V and x86-64 (Linux and macOS; no Cygwin at this point). For AArch64...
This is built upon the development of #345 to support building (most of) Compcert with the Dune build system. It resolves the issues mentioned in the original draft, especially building...
I've been [trying out using `offsetof` to calculate the size of structures with flexible array members](https://stackoverflow.com/questions/79606596/using-offsetof-to-get-allocation-size), and CompCert appears to be the only compiler that fails this test case (where...
Apparently, certain compilers define `__ILP32__`, `__LP64__`, `__LLP64__` (and the same without trailing `__`) to imply certain sizes of integers and pointers. ``` #if defined(__LLP64__) if (sizeof(short) == 2 && sizeof(int)...
