CompCert
CompCert copied to clipboard
AbsInt
The CompCert formally-verified C compiler
CompCert implements ASM-to-JSON conversion for the ARM and PowerPC architectures, but this functionality is missing for RISC-V. This patch implements this functionality. The implementation is based on the existing ARM/PowerPC...
…mb2 mode, but whether the processor supports Thumb2 mode. These instructions are also available in ARM mode on such processors.
OpenBSD ports recently updated CompCert to 3.13, but does not work for ocaml-non-native architectures. The problem comes from Makefile.menhir expecting either menhirLib.cmxa or .cmx is available. It assumes ocaml native...
Hi, I noticed that CompCert does not yet support `-ffunction-sections` and `-fdata-sections`, which are typically used to purge unused functions / data in gcc / clang: https://gcc.gnu.org/onlinedocs/gnat_ugn/Compilation-options.html So one question...
When I use `ccomp -interp ` , i encounter a UB problem about bitfield. I also notice https://github.com/AbsInt/CompCert/issues/22, it should be fixed, but not. ```c // test.c typedef struct S1...
Maybe `list_forall2` could be replaced by `List.Forall2` from the standard library.
The linker complains ``` ld: warning: can't parse dwarf compilation unit info ``` about programs compiled with `-g`
Please adapt CompCert to work with https://github.com/coq/coq/pull/17022. A suggested strategy is to add `Require Btauto` to files that `Require ZArith` and then fix up the cases where `auto` is now...
The current definition of `Val.of_bool` is: Definition of_bool (b: bool): val := if b then Vtrue else Vfalse. While this definition is perfectly natural, it inhibits partial evaluation that could...
Should be useful to identify changes more precisely in the Coq benchmarking.
