./lang/compcert [high assurance C compiler]
[+] Add this package to your ports tracker

[ CVSweb ] [ Homepage ] [ RSS feed ]

Version: 2.5, Package name: compcert-2.5
Maintained by: Daniel Dickman
Master sites:
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.


Filesize: 2285.298 KB
Version History (View Complete History)
  • (2015-09-05) Package added to openports.se, version compcert-2.5 (created)
[show/hide] View available PLISTS (Can be a lot of data)