# Copyright 1999-2008 Gentoo Foundation
# Distributed under the terms of the GNU General Public License v2
# $Header: Exp $

inherit eutils

DESCRIPTION="Frama-C is a suite of tools dedicated to the analysis of the source code of software written in C."
HOMEPAGE="http://www.frama-c.cea.fr/"
SRC_URI="http://www.frama-c.cea.fr/download/${PN/-c/-c-Lithium}-${PV/_/+}.tar.gz"

LICENSE="LGPL-2"
SLOT="0"
KEYWORDS="~alpha ~amd64 ~hppa ~ia64 ~ppc ~sparc ~x86 ~x86-fbsd"

IUSE="gtk coq pvs apron stateshook"
RESTRICT="strip"

RDEPEND="!sci-mathematics/why"

DEPEND="${RDEPEND}
	>=dev-lang/ocaml-3.09
	gtk? ( >=dev-ml/lablgtk-2.6 )
	sci-mathematics/ltl2ba
	coq? ( sci-mathematics/coq )
        pvs? ( sci-mathematics/pvs )
        apron? ( dev-libs/apron )"

S="${WORKDIR}/${PN/-c/-c-Lithium}-${PV/_/+}"

src_compile() {
        cd "${S}"

        if use stateshook; then
                einfo "moving state_set.ml* from value/ to memory_state/ ..."
                mv src/value/state_set.ml* src/memory_state/ || die
                epatch "${FILESDIR}/${P}-states_hook.patch"
        fi

	if use gtk; then
		myconf="--enable-gui"
	else
		myconf="--disable-gui"
	fi

	sed -i -e "s/\$(COQLIB)/\$(DESTDIR)\/\$(COQLIB)/g" why/Makefile.in
	sed -i -e "s/-w \$(DESTDIR)\/\$(COQLIB)/-w \$(COQLIB)/g" why/Makefile.in
	sed -i -e "s/\$(PVSLIB)\/why/\$(DESTDIR)\$(PVSLIB)\/why/g" why/Makefile.in
	sed -i -e "s/--mandir=\$mandir --enable-apron=\$HAS_APRON/--mandir=\$mandir --enable-apron=\$HAS_APRON --host=\$host --build=\$build/g" configure

	econf ${myconf} || die "econf failed"
	emake -j1 depend DESTDIR="/" || die "emake depend failed"
	emake -j1 DESTDIR="/" || die "emake failed"
}

src_install(){
	emake install DESTDIR="${D}" || die "emake install failed"

	if use stateshook; then
		ewarn "USE flag 'stateshook' is enabled, it is not officially supported so do not report any bug upstream !"
		ewarn "The value analysis does not keep all the several states attached to a statement but just their union."
		ewarn "With this patch you can access all these states through a hook while the analysis is taking place."
        fi
}