BSD Portslang/compcert 3.18p0 OpenBSD
high assurance C compiler
- System
- OpenBSD
- Repository
- OpenBSD ports
- Maintainer
- The OpenBSD ports mailing-list <[email protected]>
- Last update
- Commit
b7bdb54ad4- Categories
- lang
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.
Install
Binary package:
pkg_add compcertFrom the ports tree:
cd /usr/ports/lang/compcert && make installDependencies
Build dependencies 5
No port depends on this one.