compcert-3.17
high assurance C compiler
Back to search · Project homepage
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.
Package information
- Ports path
- lang/compcert
- Package architecture
- amd64
- Maintainer
- Daniel Dickman <daniel@openbsd.org>
- Categories
- lang
- Available flavors
- None listed
- Only for architectures
- amd64
These are ports metadata. Binary availability depends on the release, architecture and mirror. Build and test dependencies are not an installation checklist.
Direct dependencies
Build
- lang/ocaml STEM->=4.05
- math/rocq STEM->=8.15.0
- sysutils/findlib
- devel/ocaml-menhir STEM->=20200624
- devel/gmake