compcert

high assurance C compiler

WWW CVSWeb GITHub
  1. Package version
    compcert-3.13.1p0
  2. Maintainer
    The OpenBSD ports mailing-list

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.

  • STEM->=4.05:lang/ocaml
  • STEM->=8.12.0:math/coq
  • sysutils/findlib
  • STEM->=20190626:devel/ocaml-menhir
  • STEM->=8,<9:lang/gcc/8
  • STEM->=8,<9:lang/gcc/8,-c++
  • devel/gmake

  • lang/gcc/8