CVSROOT: /cvs
Module name: ports
Changes by: [email protected] 2015/09/04 18:20:08
Log message:
import lang/compcert. ok sthen@
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.
Status:
Vendor Tag: daniel
Release Tags: daniel_20150904
N ports/lang/compcert/Makefile
N ports/lang/compcert/distinfo
N ports/lang/compcert/pkg/DESCR
N ports/lang/compcert/pkg/PLIST
N ports/lang/compcert/patches/patch-driver_Configuration_ml
N ports/lang/compcert/patches/patch-Makefile
N ports/lang/compcert/patches/patch-configure
No conflicts created by this import
