The lang/compcert port
compcert-3.13.1p1 – high assurance C compiler
Description
The CompCert C verified compiler is a compiler for a large subset
of the C programming language that generates code for the PowerPC,
ARM and x86 processors.
The distinguishing feature of CompCert is that it has been formally
verified using the Coq proof assistant: the generated assembly code
is formally guaranteed to behave as prescribed by the semantics of
the source C code.
CompCert is not free software. This non-commercial release can only
be used for evaluation, research, educational and personal purposes.
A commercial version of CompCert, without this restriction and with
professional support, can be purchased from AbsInt. See the file
LICENSE for more information.
WWW: https://compcert.org/
- Only for arches
-
aarch64
amd64
i386
powerpc
- Broken
-
on i386:
linker/relocation errors following update to ocaml 4.14.2
- Categories:
-
lang
Library dependencies
Build dependencies
Run dependencies