aboutsummaryrefslogtreecommitdiffstats
path: root/devel/frama-c/Makefile
blob: 24aac81c88ecc283e0f405003b86c71c76f4db0c (plain) (blame)
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
# Created by: b.f. <bf@FreeBSD.org>
# $FreeBSD$

PORTNAME=       frama-c
DISTVERSIONPREFIX=  Oxygen-
DISTVERSION=        20120901
CATEGORIES=     devel
MASTER_SITES=       http://frama-c.com/download/ LOCAL/bf

MAINTAINER= bf@FreeBSD.org
COMMENT=    Extensible platform for source-code analysis of C

LICENSE=    LGPL21

BUILD_DEPENDS=  ${LOCALBASE}/lib/ocaml/ocamlgraph/graph.a:${PORTSDIR}/math/ocaml-ocamlgraph
RUN_DEPENDS=    ${LOCALBASE}/lib/ocaml/ocamlgraph/graph.a:${PORTSDIR}/math/ocaml-ocamlgraph

GNU_CONFIGURE=  yes
CONFIGURE_ARGS+=    --with-cpp="${FRAMAC_DEFAULT_CPP}"
MAKE_ENV+=  FRAMAC_LIBDIR="${PREFIX}/lib/frama-c"
MAN1=       frama-c.1 frama-c-gui.1

OPTIONS_DEFINE=     ALTERGO COQ GUI PLUGINS
OPTIONS_DEFAULT=    ALTERGO GUI PLUGINS
ALTERGO_DESC=   Alt-Ergo plugin (requires PLUGINS)
COQ_DESC=   Coq plugin (requires PLUGINS)
GUI_DESC=   Graphical User Interface (requires PLUGINS)

USE_GMAKE=  yes
USE_OCAML=  yes

NO_STAGE=   yes
.include <bsd.port.options.mk>

FRAMAC_DEFAULT_CPP?=    ${CPP} -C -I${DATADIR}/libc -I.

.if ${PORT_OPTIONS:MALTERGO}
.if !${PORT_OPTIONS:MPLUGINS}
IGNORE= the Alt-Ergo plugin requires the PLUGINS option to be enabled
.endif
BUILD_DEPENDS +=    alt-ergo:${PORTSDIR}/math/alt-ergo
RUN_DEPENDS+=       alt-ergo:${PORTSDIR}/math/alt-ergo
.else
CONFIGURE_ENV +=    HAS_ALTERGO=no
.endif

.if ${PORT_OPTIONS:MCOQ}
.if !${PORT_OPTIONS:MPLUGINS}
IGNORE= the Coq plugin requires the PLUGINS option to be enabled
.endif
BUILD_DEPENDS +=    coqc:${PORTSDIR}/math/coq
RUN_DEPENDS+=       coqc:${PORTSDIR}/math/coq
.else
CONFIGURE_ENV +=    HAS_COQ=no
.endif

.if ${PORT_OPTIONS:MGUI}
.if !${PORT_OPTIONS:MPLUGINS}
IGNORE= the GUI requires the PLUGINS option to be enabled
.endif
BUILD_DEPENDS +=    lablgtk2:${PORTSDIR}/x11-toolkits/ocaml-lablgtk2
RUN_DEPENDS+=       lablgtk2:${PORTSDIR}/x11-toolkits/ocaml-lablgtk2
CONFIGURE_ARGS+=    --enable-gui
PLIST_SUB+=     GUI=""
.else
CONFIGURE_ARGS+=    --disable-gui
PLIST_SUB+=     GUI="@comment "
.endif

.if ${PORT_OPTIONS:MPLUGINS}
BUILD_DEPENDS +=    dot:${PORTSDIR}/graphics/graphviz \
            ltl2ba:${PORTSDIR}/math/ltl2ba
RUN_DEPENDS+=       dot:${PORTSDIR}/graphics/graphviz \
            ltl2ba:${PORTSDIR}/math/ltl2ba
PLIST_SUB+=     PLUGINS=""
.else
CONFIGURE_ARGS+=    --with-no-plugin
PLIST_SUB+=     PLUGINS="@comment "
.endif

post-patch:
    @cd ${WRKSRC}/tests; ${MKDIR} aorai report wp wp_acsl wp_bts \
    wp_engine wp_hoare wp_plugin wp_runtime wp_store wp_typed
    @${REINPLACE_CMD} -e 's|@make |@${GMAKE} |' \
            ${WRKSRC}/src/aorai/Makefile.in
    @${REINPLACE_CMD} \
        -e 's|$$(CP)|${INSTALL_DATA}|' \
        -e 's|add_prefix|addprefix|' \
            ${WRKSRC}/share/Makefile.plugin
    @${REINPLACE_CMD} \
        -e '\|$$(CP) $$(TARGETS|s|$$(CP)|${INSTALL_DATA}|' \
        -e '\|$$(CP) frama-c|s|$$(CP)|${INSTALL_SCRIPT}|' \
            ${WRKSRC}/share/Makefile.dynamic
    @${REINPLACE_CMD} -e '\|^# Installation|,\|^# File headers|{ \
        \|$$(CP).*bin|s|$$(CP)|${INSTALL_SCRIPT}|; \
        \|$$(CP).*man/|s|$$(CP)|${INSTALL_MAN}|; \
        s|$$(CP)|${INSTALL_DATA}|; }' \
            ${WRKSRC}/Makefile
    @${REINPLACE_CMD} -e 's|HAS_ALTERGO=$$||' \
        -e '\|case $$ALTERGO_VERSION in|{N; s|0\.92\.2|0.94*|;}' \
        -e 's|HAS_COQ=$$||' \
            ${WRKSRC}/configure
    @${REINPLACE_CMD} -Ee 's@(\+|/)(lablgtk2)@\1site-lib/\2@' \
        ${WRKSRC}/src/kernel/dynamic.ml

.if ${PORT_OPTIONS:MGUI}
pre-configure:
    @(if [ ! -e ${LOCALBASE}/${OCAML_SITELIBDIR}/lablgtk2/gtkSourceView2.cmi -o \
    ! -e ${LOCALBASE}/${OCAML_SITELIBDIR}/lablgtk2/gnomeCanvas.cmi ] ; then \
    ${ECHO_MSG} "==> The WITH_GUI option for ${PKGNAME} requires" ; \
    ${ECHO_MSG} "==> x11-toolkits/ocaml-lablgtk2 to be built" ; \
    ${ECHO_MSG} "==> WITH_GNOMECANVAS and WITH_GTKSOURCEVIEW2" ; \
    exit 1; fi)
    @(if [ ! -e ${LOCALBASE}/lib/ocaml/ocamlgraph/dgraph.cmi ] ; then \
    ${ECHO_MSG} "==> The WITH_GUI option for ${PKGNAME} requires" ; \
    ${ECHO_MSG} "==> math/ocaml-ocamlgraph to be built WITH_GUI" ; \
    exit 1; fi)

.endif

post-install:
    @${TOUCH} ${PREFIX}/lib/frama-c/plugins/.keep_me \
    ${PREFIX}/lib/frama-c/plugins/gui/.keep_me

check regression-test test: build
    @cd ${WRKSRC}; ${SETENV} ${MAKE_ENV:NCPP=*} \
    CPP="${CPP} -C -I${WRKSRC}/share/libc -I." \
    ${GMAKE} ${MAKE_ARGS} oracles fulltests

.include <bsd.port.mk>