3c4bfcc3d7
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.
43 lines
932 B
Makefile
43 lines
932 B
Makefile
# $OpenBSD: Makefile,v 1.1.1.1 2015/09/05 00:20:08 daniel Exp $
|
|
|
|
ONLY_FOR_ARCHS = i386
|
|
|
|
COMMENT = high assurance C compiler
|
|
|
|
V= 2.5
|
|
GH_ACCOUNT = AbsInt
|
|
GH_PROJECT = CompCert
|
|
GH_TAGNAME = v${V}
|
|
DISTNAME = ${GH_PROJECT}-${V}
|
|
PKGNAME = ${DISTNAME:L}
|
|
|
|
HOMEPAGE = http://compcert.inria.fr/
|
|
|
|
CATEGORIES = lang
|
|
|
|
MAINTAINER = Daniel Dickman <daniel@openbsd.org>
|
|
|
|
# INRIA Non-Commercial License Agreement.
|
|
PERMIT_PACKAGE_CDROM = no commercial use
|
|
PERMIT_PACKAGE_FTP = Yes
|
|
|
|
WANTLIB += c m
|
|
|
|
USE_GMAKE = Yes
|
|
|
|
CONFIGURE_STYLE = simple
|
|
CONFIGURE_ARGS = -prefix ${WRKINST}${PREFIX} \
|
|
-no-standard-headers \
|
|
${MACHINE_ARCH:S/i386/ia32/}-bsd
|
|
|
|
BUILD_DEPENDS = lang/ocaml \
|
|
math/coq \
|
|
devel/ocaml-menhir
|
|
|
|
post-install:
|
|
${INSTALL_DATA} ${WRKSRC}/LICENSE ${PREFIX}/share/compcert
|
|
sed -i -e "s,^stdlib_path=.*,stdlib_path=${TRUEPREFIX}/lib/compcert," \
|
|
${PREFIX}/share/compcert/compcert.ini
|
|
|
|
.include <bsd.port.mk>
|