CompCert
CompCert copied to clipboard
AbsInt
The CompCert formally-verified C compiler
Could you please detail what parts of multi-byte characters are supported by CompCert? Or, inversely, if there are specific multi-byte-related features which are not supported? In particular, some compilers accept...
This is a follow-up to ed89275cb. With the Clang/LLVM linker and loader, "const" variables initialized with symbol addresses which may need relocation cannot go in a readonly section and must...
Hello, In general, ARM32 uses IR11 as the frame pointer register (i.e. FP) [1], but CompCert currently is using IR12 as FP. Considering the [following implementation](https://github.com/AbsInt/CompCert/blob/master/arm/Asm.v#L760), ```coq | Pallocframe sz...
``` static int toto; int *const p = &toto; int main() { return 0; } ``` fails to link under OpenBSD x86_64 with LLVM 13.0.0 (but I suspect this may...
In revision 108d60c0 on x86-64 ``` #include void a() { uint64_t b = 0 & 0 ? 0 * 0 && 0 : b; } ``` produces ``` error: In...
CompCert 3.11 Clang / LLD 13.0.0 OpenBSD/riscv64 -current When trying to build CompCert 3.11 on RISC-V 64-bit the compiler builds Ok. When building the tests the build has an error...
It would be really great to support the +r constraint in extended asm. For example to support this code: https://github.com/openbsd/src/blob/b3424f948f9275685df5315a2922aad768594479/sys/arch/amd64/include/endian.h#L44 If support is not possible then this type of code...
The condition `Ptrofs.unsigned sz > 0` in the semantics of `free` makes it difficult to prove that a program cannot block when calling `free`. So, this commit removes it, at...
Certain operating systems set the text segment execute-only as a security measure. This is most notably the case by default with OpenBSD on x86-64, AArch64, MIPS64, PowerPC32, PowerPC64, RISC-V, and...