ports

lang/compcert

compcert-3.3 – 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: http://compcert.inria.fr/

Distribution forbidden on cdroms
no commercial use
Only for arches
amd64 i386
Broken
An update of coq >= 8.6.1 is required to unbreak
Categories:
lang

Library dependencies

None

Build dependencies

Run dependencies

None