Various updates related to Frama-C.

17 files changed, 603 insertions, 20 deletions

diff --git a/dev-ml/mlgmpidl/Manifest b/dev-ml/mlgmpidl/Manifest
new file mode 100644
index 000000000..1f3a46d51
--- /dev/null
+++ b/dev-ml/mlgmpidl/Manifest
@@ -0,0 +1,2 @@
+DIST mlgmpidl-1.1.tgz 194002 RMD160 752c865e5355b40f9b3c9babf0c9c378cb3b4009 SHA1 ef26eaa215ccedbfc20c00614f702a06d3a70420 SHA256 8990a56f4c1ff701bb922bacf7f23b40539d123216ac5f9fe0f35967735d6fc9
+EBUILD mlgmpidl-1.1.ebuild 1347 RMD160 5eff2fd937a758d0ac8df13473465551a6b35f73 SHA1 a3135dfdb622b46b1fc086ff8d88901219cbd0a3 SHA256 98f8d303dafc13b7ca0aaa41bd284da84e7d6117adf9d7856238e0d962a38c24
diff --git a/dev-ml/mlgmpidl/mlgmpidl-1.1.ebuild b/dev-ml/mlgmpidl/mlgmpidl-1.1.ebuild
new file mode 100644
index 000000000..4bc14d0d1
--- /dev/null
+++ b/dev-ml/mlgmpidl/mlgmpidl-1.1.ebuild
@@ -0,0 +1,57 @@
+# Copyright 1999-2009 Gentoo Foundation
+# Distributed under the terms of the GNU General Public License v2
+# $Header: Exp $
+
+inherit eutils toolchain-funcs
+
+DESCRIPTION="MLGMPIDL is a package offering an interface to the GMP and MPFR libraries for OCaml version 3.07 or higher."
+HOMEPAGE="http://www.inrialpes.fr/pop-art/people/bjeannet/mlxxxidl-forge/mlgmpidl/"
+SRC_URI="http://gforge.inria.fr/frs/download.php/20228/${PN}-${PV}.tgz"
+
+LICENSE="LGPL-2"
+SLOT="0"
+KEYWORDS="~amd64 ~ppc ~sparc ~x86"
+IUSE="doc +mpfr"
+
+RDEPEND="dev-libs/gmp
+		mpfr? ( dev-libs/mpfr )
+		>=dev-lang/ocaml-3.09
+		dev-ml/camlidl"
+DEPEND="${RDEPEND}
+		doc? ( app-text/texlive
+				app-text/ghostscript-gpl )"
+
+src_unpack() {
+	unpack ${A}
+	mv ${PN} ${PN}-${PV}
+	cd ${S}
+
+	rm -R html mlgmpidl.pdf
+	mv Makefile.config.model Makefile.config
+	sed -i Makefile.config \
+		-e "s/FLAGS = \\\/FLAGS += \\\/g" \
+		-e "s/-O3 -UNDEBUG/-DUDEBUG/g" \
+		-e "s/MLGMPIDL_PREFIX = /MLGMPIDL_PREFIX = \${DESTDIR}\/usr/g"
+
+	if use !mpfr; then
+		sed -i -e "s/HAS_MPFR=1/#HAS_MPFR=0/g" Makefile.config
+	fi
+}
+
+src_compile() {
+	emake all gmprun gmptop -j1 || die "emake failed"
+
+	if use doc; then
+		make html mlgmpidl.pdf || die "emake doc failed"
+	fi
+}
+
+src_install(){
+	emake install DESTDIR="${D}" || die "emake install failed"
+	dodoc COPYING README
+
+	if use doc; then
+		dodoc mlgmpidl.pdf
+	fi
+}
+
diff --git a/dev-ml/ocamlgraph/Manifest b/dev-ml/ocamlgraph/Manifest
index f62c106c2..00d24f7ef 100644
--- a/dev-ml/ocamlgraph/Manifest
+++ b/dev-ml/ocamlgraph/Manifest
@@ -1,3 +1,3 @@
-AUX ocamlgraph-1.1-makefile.patch 5379 RMD160 e97ef8d3b70bd470f419ea5fd0d18a77c8f1df8a SHA1 f9b1236890d7372b19f17489ced2ccf86c5397d9 SHA256 53efa9874769339eca9adefc09ad40ea0abc28a8fe248d7443df71c50f18d054
-DIST ocamlgraph-1.1.tar.gz 195045 RMD160 f48af8e9c1c681bf6ee42ea22267ce022777db57 SHA1 70152127fd05aa97006434614441425182e87471 SHA256 955e0bfbfda83e055b0cf0527af0b706c8f4a14f680d3a77be1e1e725e1cfb3f
-EBUILD ocamlgraph-1.1.ebuild 1005 RMD160 31ce50aa3fdf5c98986ceae5b2e5684a956df22f SHA1 575d1b50fc6c1f6aed30f4ad2eae1d86fee7ff47 SHA256 e98c0a4509a55bf95cc2fddd0f8549e8197213774745ed10049fe6cfb4d287cf
+AUX ocamlgraph-1.2-makefile.patch 3980 RMD160 fda851982c979d4c4d667bdd803bb9a570f8e3f8 SHA1 74eec2569ad39f35fd784fc13fa16f7d37cbe3f8 SHA256 fa5ce23b1561555c07d51a75b7e2850fdb1b6abe41bc902b9d4f8f99a1473e0c
+DIST ocamlgraph-1.2.tar.gz 213426 RMD160 c5ef73069a912ba179adbad3c4e0d629cc91cd54 SHA1 087cd2720c1a3df3f6543db4ad8d81983fcddba0 SHA256 0695a91a3f2abc0f47eafdae4af8a6022154727aec00784a12362d3719ff51f2
+EBUILD ocamlgraph-1.2.ebuild 1027 RMD160 27095298c445a12f3a8d3bead261336141f7d1e8 SHA1 6f6d8036141f1425f3feef777229185b2b705da1 SHA256 ec26bf47e8acdc1e89ace4f685e59192b6bae62c046d623ccab0742826988fd7
diff --git a/dev-ml/ocamlgraph/files/ocamlgraph-1.2-makefile.patch b/dev-ml/ocamlgraph/files/ocamlgraph-1.2-makefile.patch
new file mode 100644
index 000000000..fd7b8de5c
--- /dev/null
+++ b/dev-ml/ocamlgraph/files/ocamlgraph-1.2-makefile.patch
@@ -0,0 +1,102 @@
+diff -Naurd ocamlgraph-1.2-orign/Makefile.in ocamlgraph-1.2-patch/Makefile.in
+--- ocamlgraph-1.2-orign/Makefile.in	2009-08-31 05:57:53.000000000 +0000
++++ ocamlgraph-1.2-patch/Makefile.in	2009-09-11 13:23:51.000000000 +0000
+@@ -31,7 +31,7 @@
+ OCAMLDOC = @OCAMLDOC@
+ OCAMLLEX = @OCAMLLEX@
+ OCAMLYACC= @OCAMLYACC@
+-OCAMLLIB = @OCAMLLIB@
++OCAMLLIB = @OCAMLLIB@/ocamlgraph/
+ OCAMLBEST= @OCAMLBEST@
+ OCAMLVERSION = @OCAMLVERSION@
+ OCAMLWEB = @OCAMLWEB@
+@@ -147,6 +147,7 @@
+ VIEWER_CMO:=$(patsubst %,$(VIEWER_DIR)/%.cmo, $(VIEWER_CMO))
+ VIEWER_CMX=$(VIEWER_CMO:.cmo=.cmx)
+ VIEWER_CMI=$(VIEWER_CMO:.cmo=.cmi)
++VIEWER_OBJ=$(VIEWER_CMO:.cmo=.o)
+ 
+ VIEWER_INCLUDES= @INCLUDEGTK2@ -I $(VIEWER_DIR) $(INCLUDES) -I .
+ 
+@@ -175,6 +176,7 @@
+ DGRAPH_CMO:=$(patsubst %,$(DGRAPH_DIR)/%.cmo, $(DGRAPH_CMO))
+ DGRAPH_CMX=$(DGRAPH_CMO:.cmo=.cmx)
+ DGRAPH_CMI=$(DGRAPH_CMO:.cmo=.cmi)
++DGRAPH_OBJ=$(DGRAPH_CMO:.cmo=.o)
+ 
+ DGRAPH_INCLUDES= @INCLUDEGTK2@ -I $(DGRAPH_DIR) $(INCLUDES) -I .
+ 
+@@ -270,42 +272,48 @@
+ 
+ install: install-$(OCAMLBEST) install-byte
+ ifeq (@LABLGNOMECANVAS@,yes)
++	mkdir -p $(DESTDIR)$(BINDIR)
+ ifeq ($(OCAMLBEST),byte)
+-	cp -f $(BINDIR)/graph-editor.byte $(BINDIR)/graph-editor$(EXE)
+-	cp -f $(BINDIR)/graph-viewer.byte $(BINDIR)/graph-viewer$(EXE)
++	ln -s $(BINDIR)/ocamlgraph-editor.byte $(DESTDIR)$(BINDIR)/ocamlgraph-editor$(EXE)
++	ln -s $(BINDIR)/ocamlgraph-viewer.byte $(DESTDIR)$(BINDIR)/ocamlgraph-viewer$(EXE)
+ else
+-	cp -f $(BINDIR)/graph-editor.opt $(BINDIR)/graph-editor$(EXE)
+-	cp -f $(BINDIR)/graph-viewer.opt $(BINDIR)/graph-viewer$(EXE)
++	mv $(DESTDIR)$(BINDIR)/ocamlgraph-editor.opt $(DESTDIR)$(BINDIR)/ocamlgraph-editor$(EXE)
++	mv $(DESTDIR)$(BINDIR)/ocamlgraph-viewer.opt $(DESTDIR)$(BINDIR)/ocamlgraph-viewer$(EXE)
+ endif
+ endif
+ 
+ install-byte: 
++	mkdir -p "$(DESTDIR)$(OCAMLLIB)"
+ 	cp -f graph.cmo graph.cmi $(CMA) "$(DESTDIR)$(OCAMLLIB)"
+ ifeq (@LABLGNOMECANVAS@,yes)
+-	cp -f $(ED_DIR)/editor.byte $(BINDIR)/graph-editor.byte
+-	cp -f $(VIEWER_CMO) "$(DESTDIR)$(OCAMLLIB)"
+-	cp -f $(DGRAPH_CMO) "$(DESTDIR)$(OCAMLLIB)"
+-	cp -f $(DGRAPH_DIR)/dgraph.byte $(BINDIR)/graph-viewer.byte
++	mkdir -p $(DESTDIR)$(BINDIR)
++	cp -f $(ED_DIR)/editor.byte $(DESTDIR)$(BINDIR)/ocamlgraph-editor.byte
++	cp -f $(VIEWER_CMO) $(VIEWER_CMI) "$(DESTDIR)$(OCAMLLIB)"
++	cp -f $(DGRAPH_CMO) $(DGRAPH_CMI) "$(DESTDIR)$(OCAMLLIB)"
++	cp -f $(DGRAPH_DIR)/dgraph.byte $(DESTDIR)$(BINDIR)/ocamlgraph-viewer.byte
+ endif
+ 
+ install-opt: install-byte
++	mkdir -p "$(DESTDIR)$(OCAMLLIB)"
+ 	cp -f graph$(LIBEXT) graph.cmx $(CMXA) "$(DESTDIR)$(OCAMLLIB)"
+ ifeq (@LABLGNOMECANVAS@,yes)
+-	cp -f $(ED_DIR)/editor.opt $(BINDIR)/graph-editor.opt
+-	cp -f $(VIEWER_CMX) "$(DESTDIR)$(OCAMLLIB)"
+-	cp -f $(DGRAPH_CMX) "$(DESTDIR)$(OCAMLLIB)"
+-	cp -f $(DGRAPH_DIR)/dgraph.opt $(BINDIR)/graph-viewer.opt
++	mkdir -p $(DESTDIR)$(BINDIR)
++	cp -f $(ED_DIR)/editor.opt $(DESTDIR)$(BINDIR)/ocamlgraph-editor.opt
++	cp -f $(VIEWER_CMX) $(VIEWER_OBJ) "$(DESTDIR)$(OCAMLLIB)"
++	cp -f $(DGRAPH_CMX) $(DGRAPH_OBJ) "$(DESTDIR)$(OCAMLLIB)"
++	cp -f $(DGRAPH_DIR)/dgraph.opt $(DESTDIR)$(BINDIR)/ocamlgraph-viewer.opt
+ endif
+ 
+ install-findlib: META
+ ifdef OCAMLFIND
++	mkdir -p $(DESTDIR)/$(OCAMLLIB)
+ ifeq (@LABLGNOMECANVAS@,yes)
+-	$(OCAMLFIND) install ocamlgraph META $(SRCDIR)/*.mli \
+-		graph$(LIBEXT) graph.cmx graph.cmo graph.cmi $(CMA) $(CMXA) \
+-		$(VIEWER_CMX) $(VIEWER_CMO) $(DGRAPH_CMX) $(DGRAPH_CMO)
++	$(OCAMLFIND) install -destdir $(DESTDIR)/$(OCAMLLIB) \
++		ocamlgraph META $(SRCDIR)/*.mli dgraph/*.mli dgraph/viewer.ml \
++		dgraph/dGraphViewer.ml view_graph/*.mli view_graph/viewGraph_test.ml
+ else
+-	$(OCAMLFIND) install ocamlgraph META $(SRCDIR)/*.mli \
+-		graph$(LIBEXT) graph.cmx graph.cmo graph.cmi $(CMA) $(CMXA)
++	$(OCAMLFIND) install -destdir $(DESTDIR)/$(OCAMLLIB) \
++		ocamlgraph META $(SRCDIR)/*.mli
+ endif
+ endif
+ 
+@@ -328,7 +336,6 @@
+ 	mkdir -p doc
+ 	rm -f doc/*
+ 	$(OCAMLDOC) -d doc -html $(INCLUDES) $(DOC_SRC)
+-	$(MAKE) -C $(VIEWER_DIR) doc
+ 
+ # literate programming
+ $(NAME).tex: $(DOC_SRC)
diff --git a/dev-ml/ocamlgraph/ocamlgraph-1.2.ebuild b/dev-ml/ocamlgraph/ocamlgraph-1.2.ebuild
new file mode 100644
index 000000000..9ee425cd8
--- /dev/null
+++ b/dev-ml/ocamlgraph/ocamlgraph-1.2.ebuild
@@ -0,0 +1,52 @@
+# Copyright 1999-2009 Gentoo Foundation
+# Distributed under the terms of the GNU General Public License v2
+# $Header: Exp $
+
+inherit eutils autotools
+
+DESCRIPTION="A graph library for Objective Caml"
+HOMEPAGE="http://ocamlgraph.lri.fr/"
+SRC_URI="http://ocamlgraph.lri.fr/download/${P}.tar.gz"
+
+LICENSE="LGPL-2"
+SLOT="0"
+KEYWORDS="~amd64 ~ppc ~sparc ~x86"
+
+RDEPEND=">=dev-lang/ocaml-3.10.2"
+
+DEPEND="${RDEPEND}
+    gtk? ( >=dev-ml/lablgtk-2.6 )
+    ocamlopt? ( dev-lang/ocaml[ocamlopt] )"
+
+IUSE="doc examples gtk +ocamlopt"
+
+src_unpack() {
+	unpack ${A}
+	cd ${S}
+	epatch "${FILESDIR}/${P}-makefile.patch"
+	eautoreconf
+}
+
+src_compile() {
+	econf || die "econf failed"
+	emake DESTDIR="/" -j1 || die "emake failed"
+
+	if use doc; then
+		emake doc || die "emake doc failed"
+	fi
+}
+
+src_install() {
+	emake install install-findlib DESTDIR="${D}" || die "emake install failed"
+	dodoc CHANGES COPYING CREDITS FAQ README
+
+	if use doc; then
+		dohtml doc/*
+	fi
+
+	if use examples; then
+		insinto /usr/share/doc/${PF}
+		doins -r examples
+	fi
+}
+
diff --git a/sci-mathematics/apron/Manifest b/sci-mathematics/apron/Manifest
index 7d897767f..efefbc068 100644
--- a/sci-mathematics/apron/Manifest
+++ b/sci-mathematics/apron/Manifest
@@ -1,4 +1,3 @@
-AUX apron-0.9.9-doc.patch 64468 RMD160 caa0822b7a166120d4005aaffc306a2a87934829 SHA1 6ec06db79955cb75b9d136e8f3b837ce242c301c SHA256 0c837cc92f67c8ceb6421daae490113f0b6f4cda5b03839b06fd23b6504b1e20
-AUX apron-0.9.9-ppl.patch 10288 RMD160 f2863bd448859a6f32b8a0dec74c4aad28a7b241 SHA1 633d30d09f909c9745ac4b7a2511b313c7388fb2 SHA256 efbb85f5a4412f210becc7ecf91772996f4bbc938e3628ad29ed8f6d33d88819
-DIST apron-0.9.9.tgz 1442889 RMD160 9b9081b4e7b442198975baffc7febf45073381e9 SHA1 31a607622c325869006eff21c2708f37448a7290 SHA256 f016e0b6d24feb7f75c0a0af370bf9d4bd512b86733c7abf25a12f6350718680
-EBUILD apron-0.9.9.ebuild 2357 RMD160 6261a2d30cbe64fbc45dc63c5c24b8219f9a3b8e SHA1 23a99a9b94caba37dca7191676324a8e12fc6a36 SHA256 09fe90643ccebab980b4584b4300f065f2b222d77d588bc2498a4386224f859c
+AUX apron-0.9.10-pkgrid_manager.patch 543 RMD160 36b7ef40e2748781a21275af0e50bfbfd0a4253e SHA1 c636f4837643b3bfe6cc2f9ee7194d9b2a756fc6 SHA256 d62e05fac7f08d2b6ac62a8e8819ce00e55605155869a7d5ad814c399020d6bf
+DIST apron-0.9.10.tgz 845879 RMD160 ddd621617adfa158ecd1b8cc3371feca29a95538 SHA1 77ac01bad0d5a0dfc702c647e1290b4bd1ff6f11 SHA256 af1f113b455d16b41bba3c3e94274edacfa5a8d8ef12fde2adc26eaa01f900ef
+EBUILD apron-0.9.10.ebuild 2269 RMD160 6045101918918224f9bc758c8678a1d983e2dc55 SHA1 fdab347c7c75f910851a72b620eb1b424f3f90fa SHA256 940b28f76815e13a8b0c904154343dcece45498aa64cee33432c98de7f62df04
diff --git a/sci-mathematics/apron/apron-0.9.10.ebuild b/sci-mathematics/apron/apron-0.9.10.ebuild
new file mode 100644
index 000000000..7ad16f9e4
--- /dev/null
+++ b/sci-mathematics/apron/apron-0.9.10.ebuild
@@ -0,0 +1,87 @@
+# Copyright 1999-2009 Gentoo Foundation
+# Distributed under the terms of the GNU General Public License v2
+# $Header: Exp $
+
+inherit eutils toolchain-funcs
+
+DESCRIPTION="The APRON library is dedicated to the static analysis of the numerical variables of a program by Abstract Interpretation"
+HOMEPAGE="http://apron.cri.ensmp.fr/library/"
+SRC_URI="http://apron.cri.ensmp.fr/library/${P}.tgz"
+
+LICENSE="LGPL-2 GPL-2"
+SLOT="0"
+KEYWORDS="~amd64 ~ppc ~sparc ~x86"
+IUSE="cxx doc ocaml ppl"
+
+RDEPEND="dev-libs/gmp
+		dev-libs/mpfr
+		ocaml? ( >=dev-lang/ocaml-3.09
+				dev-ml/camlidl )
+		ppl? ( dev-libs/ppl )"
+DEPEND="${RDEPEND}
+		doc? ( app-text/texlive
+				app-text/ghostscript-gpl 
+				cxx? ( app-doc/doxygen ) )"
+
+src_unpack() {
+	unpack ${A}
+	cd ${S}
+
+	mv Makefile.config.model Makefile.config
+
+	#fix compile process
+	sed -i Makefile.config \
+		-e "s/FLAGS = \\\/FLAGS += \\\/g" \
+		-e "s/-O3 -DNDEBUG/-DNDEBUG/g" \
+		-e "s/APRON_PREFIX = \/usr/APRON_PREFIX = \${DESTDIR}\/usr/g" \
+		-e "s/MLGMPIDL_PREFIX = \/usr\/local/MLGMPIDL_PREFIX = \${DESTDIR}\/usr/g"
+	
+	#fix doc building process
+	sed -i Makefile -e "s/; make html/; make/g"
+	sed -i apronxx/doc/Doxyfile \
+		-e "s/OUTPUT_DIRECTORY       = \/.*/OUTPUT_DIRECTORY       = .\//g" \
+		-e "s/STRIP_FROM_PATH        = \/.*/STRIP_FROM_PATH        = .\//g"
+
+	if [[ "$(gcc-major-version)" == "4" ]]; then
+		sed -i -e "s/# HAS_LONG_DOUBLE = 1/HAS_LONG_DOUBLE = 1/g" Makefile.config
+	fi
+	if use !ocaml; then
+		sed -i -e "s/HAS_OCAML = 1/#HAS_OCAML = 0/g" Makefile.config
+	fi
+	if use ppl; then
+		sed -i -e "s/# HAS_PPL = 1/HAS_PPL = 1/g" Makefile.config
+	fi
+	if use cxx && use ppl; then
+		sed -i -e "s/# HAS_CPP = 1/HAS_CPP = 1/g" Makefile.config
+	else
+		die "USE flag 'cxx' needs USE flag 'ppl' set"
+	fi
+
+	epatch "${FILESDIR}/${P}-pkgrid_manager.patch"
+}
+
+src_compile() {
+	#damn crappy Makefile
+	emake || emake || die "emake failed"
+
+	if use doc; then
+		emake doc || "emake doc failed"
+	fi
+}
+
+src_install(){
+	emake install DESTDIR="${D}" || die "emake install failed"
+	dodoc AUTHORS Changes COPYING README
+
+	if use doc; then
+		dodoc apron/apron.pdf
+		if use ocaml; then
+			dodoc mlapronidl/mlapronidl.pdf
+		fi
+		if use cxx; then
+			mv apronxx/doc/latex/refman.pdf apronxx/apronxx.pdf
+			dodoc ./apronxx/apronxx.pdf
+		fi
+	fi
+}
+
diff --git a/sci-mathematics/apron/files/apron-0.9.10-pkgrid_manager.patch b/sci-mathematics/apron/files/apron-0.9.10-pkgrid_manager.patch
new file mode 100644
index 000000000..6fa5d3cab
--- /dev/null
+++ b/sci-mathematics/apron/files/apron-0.9.10-pkgrid_manager.patch
@@ -0,0 +1,12 @@
+diff -Naur apron-0.9.10-orig/apronxx/apxx_ppl_product_inline.hh apron-0.9.10-ptch/apronxx/apxx_ppl_product_inline.hh
+--- apron-0.9.10-orig/apronxx/apxx_ppl_product_inline.hh	2007-10-10 12:42:07.000000000 +0000
++++ apron-0.9.10-ptch/apronxx/apxx_ppl_product_inline.hh	2009-09-22 21:05:56.000000000 +0000
+@@ -14,7 +14,7 @@
+ */
+ 
+ inline pkgrid_manager::pkgrid_manager(bool strict) 
+-  : manager(ap_pkgrid_manager_alloc(strict))
++  : manager(ap_pkgrid_manager_alloc(NULL, NULL))
+ {}
+ 
+ inline manager& pkgrid_manager::operator=(const manager& m)
diff --git a/sci-mathematics/frama-c/Manifest b/sci-mathematics/frama-c/Manifest
index ee2ae8004..7da24b4a5 100644
--- a/sci-mathematics/frama-c/Manifest
+++ b/sci-mathematics/frama-c/Manifest
@@ -1,9 +1,6 @@
-AUX frama-c-20090601_beta1-accessors.patch 1277 RMD160 0158505b80d98477fa39f67c80b12e0414f26b41 SHA1 0a3427db59af94e7ca534cc44bedd0ca9742c7f3 SHA256 ee4a0ebf3702ad6d39ff7522ae53aabc0d907bf51bf177bf71d69ac6a760aa62
-AUX frama-c-20090601_beta1-configure.patch 11290 RMD160 500f61b8fba8288ec6f546d4ab8fd4267002457c SHA1 d95b00b7f5f5ee53450af0c2a14d63e99b14fa4f SHA256 eb4bc27a77db309f95c8030e2b4c93fcd430fca84af31ba2f8a73fb686b4d593
-AUX frama-c-20090601_beta1-install_files.patch 746 RMD160 19e8ff63018342b9e1917bdf80f786d7f8d4fdf7 SHA1 f99bbb80e2d3316a9fa4f204773bff95143159db SHA256 359676758f92ff385c5137f596a342233f09d741a724128ed8127228f58a718c
-AUX frama-c-20090601_beta1-ocamlgraph.patch 571 RMD160 40bb7627c3cca8a1a1a5b8309d12aeca4915067b SHA1 48b618a9ef22606964c873bbaa7817e7c3fd4018 SHA256 1bb63323d8a07e7d43adfe70a618a576d937c098f178790f18e6d404166dc85a
-AUX frama-c-20090601_beta1-printexc.patch 8717 RMD160 af10bb8a9869e5ab6d4b32b9d4a5f379686f6b5a SHA1 c7aabb6373b10b6e45167c1a4d0ea4c3a6213f58 SHA256 680a99a0a73d6b0eb6f2dcd41caae02b5cd5b4846de1af85b34b5092bab4e5cf
-AUX frama-c-20090601_beta1-states_hook.patch 3904 RMD160 8d859be8eb8917b415a3b6f9a7c30a62d1de2215 SHA1 e4e76ec1b83f2409d2b16f84db40f873ff8cb0ce SHA256 274d3b5a68d437b01186a7b6734059033b9750dd3de6c0c7b02a7e88672d6ba1
-AUX frama-c-20090601_beta1-stmt_deps.patch 4076 RMD160 8aca2d28f6c53de8d43455ab8216e43c16ed7dd3 SHA1 8ce7665ec28ca6b3d1021b5e6cc828bb8ecd18bd SHA256 349c897c45d2af21118bc0e1ce90de94a4c8906d38d3c562f8d729745f6f5d33
-DIST frama-c-Beryllium-20090601-beta1.tar.gz 17564297 RMD160 d24e815c850f2bb66816c316d31eaf7f015f2741 SHA1 7d2219f1753f32bfa0e3a950fbd05e059e88538a SHA256 349a984b15ee72381f851b5fe89115656e450f49eb98ce3f3c3969fa2031c42a
-EBUILD frama-c-20090601_beta1.ebuild 1827 RMD160 bfe59cf239e2a40b9a6f5103d0ee831b639fc407 SHA1 ef901f0ba51cd0dfeab9f52b862a837be8a4714f SHA256 d49e14131442f52e03a47a9bbfc729fa104667061a044cb9d70d80b64a4c7de3
+AUX frama-c-20090901-ocamlgraph_link.patch 721 RMD160 0b78639b9f31c62575a0552c93b48dd82faeb513 SHA1 ac84c82de12c8436973a97c2e62eceac8c0fd12d SHA256 5003ddacc4b90dfb6e61af643a0d22bf2135f1d7bdb10fe1f6e20d783da5207a
+AUX frama-c-20090901-varinfo_accessor.patch 1277 RMD160 0158505b80d98477fa39f67c80b12e0414f26b41 SHA1 0a3427db59af94e7ca534cc44bedd0ca9742c7f3 SHA256 ee4a0ebf3702ad6d39ff7522ae53aabc0d907bf51bf177bf71d69ac6a760aa62
+AUX frama-c-20090901-weak_dynlink.patch 836 RMD160 5af7b5a35a7d4548cb5adea1dc1481fe7869b161 SHA1 ac6cb265603818ecdb75a3946f44721775350f8c SHA256 48e350c5dad819ebb8dea19b6a441ae8141d29a80b32ae8f400fe46f951fcfcd
+AUX frama-c-20090901-why_link.patch 2172 RMD160 bc971e4d99a8a8b7570fd1da8e5f751b70b4a73f SHA1 6e8d3c337715af9d94f996aa2ca5a63dbae20ae9 SHA256 0f4020d2562cf32f85e1ee605464c2e48cffa0448245999fd063b70095640357
+DIST frama-c-Beryllium-20090901.tar.gz 18162700 RMD160 b29038e948b898196947cae636eef9adbea99ed6 SHA1 17b1516e9807a9a34ab20a3413efc372549e6fed SHA256 ac420d72b9d0062dd1213a6e595a01c32d0cd5a465c8736c65a42cc717742cc9
+EBUILD frama-c-20090901.ebuild 1681 RMD160 b8ec4529de77aaf117ddc8ce0cb42ff5ecb7ee8d SHA1 b11a5c3b1c9484ffce73df7401a3429041f56c60 SHA256 36e270862ac13f7aa8c75f26f6813beb8d9bd6a1f7af710250831cf4bc84a997
diff --git a/sci-mathematics/frama-c/files/frama-c-20090901-ocamlgraph_link.patch b/sci-mathematics/frama-c/files/frama-c-20090901-ocamlgraph_link.patch
new file mode 100644
index 000000000..518aada60
--- /dev/null
+++ b/sci-mathematics/frama-c/files/frama-c-20090901-ocamlgraph_link.patch
@@ -0,0 +1,22 @@
+From: Mehdi Dogguy <mehdi@debian.org>
+Date: Wed, 9 Sep 2009 17:25:18 +0200
+Subject: [PATCH] Add dGraphView.cmo when linking
+
+---
+ Makefile |    2 +-
+ 1 files changed, 1 insertions(+), 1 deletions(-)
+
+diff --git a/Makefile b/Makefile
+index 65d9f77..3a70533 100644
+--- a/Makefile
++++ b/Makefile
+@@ -357,7 +357,7 @@ OPT_LIBS+= graph.cmxa
+ ifeq ($(HAS_GNOMECANVAS),yes)
+ ifeq ($(ENABLE_SYNTACTIC_CALLGRAPH),yes)
+ GRAPH_GUICMO_BASE= xDotDraw.cmo dGraphModel.cmo xDot.cmo dGraphViewItem.cmo \
+-	concreteModel.cmo
++	dGraphView.cmo concreteModel.cmo
+ GRAPH_GUICMO_BASE+= viewGraph.cmo viewGraph_select.cmo viewGraph_utils.cmo
+ GRAPH_GUICMO=$(GRAPH_GUICMO_BASE:%=$(OCAMLGRAPH_HOME)/%)
+ GRAPH_GUICMX= $(GRAPH_GUICMO:.cmo=.cmx)
+-- 
diff --git a/sci-mathematics/frama-c/files/frama-c-20090901-varinfo_accessor.patch b/sci-mathematics/frama-c/files/frama-c-20090901-varinfo_accessor.patch
new file mode 100644
index 000000000..644aef7da
--- /dev/null
+++ b/sci-mathematics/frama-c/files/frama-c-20090901-varinfo_accessor.patch
@@ -0,0 +1,26 @@
+diff -Naur frama-c-Beryllium-20090601-beta1-orig/src/ai/base.ml frama-c-Beryllium-20090601-beta1-ptch/src/ai/base.ml
+--- frama-c-Beryllium-20090601-beta1-orig/src/ai/base.ml	2009-05-15 09:10:25.000000000 +0000
++++ frama-c-Beryllium-20090601-beta1-ptch/src/ai/base.ml	2009-07-12 17:10:54.000000000 +0000
+@@ -271,6 +271,11 @@
+   | Var (t,_) | Initialized_Var (t,_) -> t
+   | _ -> assert false
+ 
++let get_varinfo t =
++  match t with
++  | Var (t,_) | Initialized_Var (t,_) -> t
++  | _ -> assert false
++
+ let create_varinfo varinfo =
+   assert (not varinfo.vlogic);
+   Var (varinfo,validity_from_type varinfo)
+diff -Naur frama-c-Beryllium-20090601-beta1-orig/src/ai/base.mli frama-c-Beryllium-20090601-beta1-ptch/src/ai/base.mli
+--- frama-c-Beryllium-20090601-beta1-orig/src/ai/base.mli	2009-05-05 14:29:35.000000000 +0000
++++ frama-c-Beryllium-20090601-beta1-ptch/src/ai/base.mli	2009-07-12 17:09:54.000000000 +0000
+@@ -61,6 +61,7 @@
+ val is_block_local: t -> Cil_types.block -> bool
+ val is_hidden_variable : t -> bool
+ val validity_from_type : Cil_types.varinfo -> validity
++val get_varinfo : t -> Cil_types.varinfo
+ val create_varinfo : Cil_types.varinfo -> t
+ val create_logic :  Cil_types.varinfo -> validity -> t
+ val create_initialized :  Cil_types.varinfo -> validity -> t
diff --git a/sci-mathematics/frama-c/files/frama-c-20090901-weak_dynlink.patch b/sci-mathematics/frama-c/files/frama-c-20090901-weak_dynlink.patch
new file mode 100644
index 000000000..e3d2054e0
--- /dev/null
+++ b/sci-mathematics/frama-c/files/frama-c-20090901-weak_dynlink.patch
@@ -0,0 +1,21 @@
+From: Mehdi Dogguy <dogguy@pps.jussieu.fr>
+Date: Tue, 1 Sep 2009 10:17:52 +0200
+Subject: [PATCH] Fix weak pattern-matching in dynlink_lower_311_byte.ml
+
+---
+ src/lib/dynlink_lower_311_byte.ml |    1 +
+ 1 files changed, 1 insertions(+), 0 deletions(-)
+
+diff --git a/src/lib/dynlink_lower_311_byte.ml b/src/lib/dynlink_lower_311_byte.ml
+index 58e0ee5..fc2705e 100644
+--- a/src/lib/dynlink_lower_311_byte.ml
++++ b/src/lib/dynlink_lower_311_byte.ml
+@@ -84,6 +84,7 @@ let from_dynlink_error = function
+   | Dynlink.Corrupted_interface s -> Corrupted_interface s
+   | Dynlink.File_not_found s -> File_not_found s
+   | Dynlink.Cannot_open_dll s -> Cannot_open_dll s
++  | Dynlink.Inconsistent_implementation s -> Inconsistent_implementation s
+ 
+ let stub_error f x = 
+   try f x with Dynlink.Error e -> raise (Error (from_dynlink_error e))
+-- 
diff --git a/sci-mathematics/frama-c/files/frama-c-20090901-why_link.patch b/sci-mathematics/frama-c/files/frama-c-20090901-why_link.patch
new file mode 100644
index 000000000..66cbf7044
--- /dev/null
+++ b/sci-mathematics/frama-c/files/frama-c-20090901-why_link.patch
@@ -0,0 +1,55 @@
+From: Mehdi Dogguy <mehdi@debian.org>
+Date: Wed, 9 Sep 2009 16:51:55 +0200
+Subject: [PATCH] Make Jessie plugin use Jc from Why 2.19
+
+---
+ src/jessie/interp.ml |   14 ++++++--------
+ 1 files changed, 6 insertions(+), 8 deletions(-)
+
+diff --git a/src/jessie/interp.ml b/src/jessie/interp.ml
+index c3057db..84ae55d 100644
+--- a/src/jessie/interp.ml
++++ b/src/jessie/interp.ml
+@@ -2060,8 +2060,8 @@ let global vardefs g =
+     | GCompTag(compinfo,pos) when compinfo.cstruct -> (* struct type *)
+         let field fi =
+           let this =
+-            default_field_modifiers, 
+-            ctype ?bitsize:fi.fsize_in_bits fi.ftype,
++            false,
++            (ctype ?bitsize:fi.fsize_in_bits fi.ftype:Jc_ast.ptype),
+             fi.fname, fi.fsize_in_bits
+           in
+           let padding_size =
+@@ -2069,8 +2069,8 @@ let global vardefs g =
+           in
+           if padding_size = 0 then [this] else
+             let padding =
+-              default_field_modifiers, 
+-              type_of_padding, unique_name "padding", fi.fpadding_in_bits
++              false,
++              (type_of_padding:Jc_ast.ptype), unique_name "padding", fi.fpadding_in_bits
+             in
+             [this;padding]
+         in
+@@ -2131,8 +2131,8 @@ let global vardefs g =
+         in
+         let padding =
+           if union_size = 0 then [] else
+-            [default_field_modifiers, 
+-             type_of_padding, unique_name "padding", Some union_size]
++            [false, 
++             (type_of_padding:Jc_ast.ptype), unique_name "padding", Some union_size]
+         in
+         let union_tag = JCDtag(compinfo.cname,[],None,padding,[]) in
+         let fields = List.map field compinfo.cfields in
+@@ -2397,8 +2397,6 @@ let pragma = function
+ 		  [Jc_output.JCfloat_model Jc_env.FMstrict]
+               | "full" -> float_model := `Full;
+ 		  [Jc_output.JCfloat_model Jc_env.FMfull]
+-              | "multirounding" -> float_model := `Multirounding;
+-		  [Jc_output.JCfloat_model Jc_env.FMmultirounding]
+               | s ->
+                   Jessie_options.warning ~current:true
+                     "pragma %s: identifier %s is not a valid value (ignored)." 
+-- 
diff --git a/sci-mathematics/frama-c/frama-c-20090901.ebuild b/sci-mathematics/frama-c/frama-c-20090901.ebuild
new file mode 100644
index 000000000..678c0ad54
--- /dev/null
+++ b/sci-mathematics/frama-c/frama-c-20090901.ebuild
@@ -0,0 +1,70 @@
+# Copyright 1999-2009 Gentoo Foundation
+# Distributed under the terms of the GNU General Public License v2
+# $Header: Exp $
+
+inherit autotools 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/"
+NAME="Beryllium"
+SRC_URI="http://www.frama-c.cea.fr/download/${PN/-c/-c-$NAME}-${PV/_/-}.tar.gz"
+
+LICENSE="LGPL-2"
+SLOT="0"
+KEYWORDS="~amd64 ~ppc ~sparc ~x86"
+
+IUSE="apron coq doc gappa gtk pff pvs +why"
+RESTRICT="strip"
+
+RDEPEND="sci-mathematics/ltl2ba
+		apron? ( sci-mathematics/apron )
+        coq? ( sci-mathematics/coq )
+        gappa? ( sci-mathematics/gappalib-coq )
+        pff? ( sci-mathematics/pff )
+        pvs? ( sci-mathematics/pvs )
+		why? ( sci-mathematics/why )"
+
+DEPEND="${RDEPEND}
+		>=dev-lang/ocaml-3.10.2
+		>=dev-ml/ocamlgraph-1.1
+		gtk? ( >=dev-ml/lablgtk-2.12 )"
+
+S="${WORKDIR}/${PN/-c/-c-$NAME}-${PV/_/-}"
+
+src_unpack(){
+	unpack ${A}
+	cd "${S}"
+
+	touch config_file
+	epatch "${FILESDIR}/${P}-varinfo_accessor.patch"
+	epatch "${FILESDIR}/${P}-why_link.patch"
+	epatch "${FILESDIR}/${P}-ocamlgraph_link.patch"
+	epatch "${FILESDIR}/${P}-weak_dynlink.patch"
+
+	eautoreconf
+}
+
+src_compile() {
+	if use gtk; then
+		myconf="--enable-gui"
+	else
+		myconf="--disable-gui"
+	fi
+
+	econf ${myconf} --with-whydir=no || die "econf failed"
+
+	# dependencies can not be processed in parallel,
+	# this is the intended behavior.
+	emake -j1 depend || die "emake depend failed"
+	emake all top DESTDIR="/" || die "emake failed"
+}
+
+src_install(){
+	emake install DESTDIR="${D}" || die "emake install failed"
+	dodoc Changelog doc/README
+
+	if use doc; then
+		dodoc doc/manuals/* 
+	fi
+}
+
diff --git a/sci-mathematics/why/Manifest b/sci-mathematics/why/Manifest
index 1ffc5a70f..c87abb4a7 100644
--- a/sci-mathematics/why/Manifest
+++ b/sci-mathematics/why/Manifest
@@ -1,4 +1,4 @@
 AUX why-2.19-jessie_lib.patch 1631 RMD160 b3975a252f539a04b079b6e973332136fde464cb SHA1 2ba2c2956354c896904d0c9a2e1d6079fbb56027 SHA256 aaff9f7648438d54eec0b1e9f0ff4828aaa26558ee7d847190d7a3d6e0c4abbc
-AUX why-2.19-sandbox.patch 3025 RMD160 b8b1b178b09a7b6eda9c8aeac7f5013650fb6c84 SHA1 6bd5e80aa79a6a36d89a114696da716b92aa60df SHA256 121b67a2b46139b93be9af293615a6a04e06a00323096e8b2317a7116bbf5d84
+AUX why-2.19-makefile_sandbox.patch 3025 RMD160 b8b1b178b09a7b6eda9c8aeac7f5013650fb6c84 SHA1 6bd5e80aa79a6a36d89a114696da716b92aa60df SHA256 121b67a2b46139b93be9af293615a6a04e06a00323096e8b2317a7116bbf5d84
 DIST why-2.19.tar.gz 2622629 RMD160 d1e3a099226a42b039672161ada63270e6274b46 SHA1 6139699168c6aab76d42e02029ba4c51cf2a8130 SHA256 f5eef288c25744f1c7725c1c733b3129a74cde6cf08eaa57b9705115d75499a3
-EBUILD why-2.19.ebuild 1251 RMD160 06d27855255d3d9d6e64439e09ec07bd85f7f8f3 SHA1 e9a00f666946205726522a29545645e474660bd0 SHA256 ab65ace2cae729b5a739b81bd3190a7b3453d6848d9413cc2680537fe641566c
+EBUILD why-2.19.ebuild 1439 RMD160 721d1ac7ad18c127a5c2f62c235d43d761ce19ce SHA1 6816b7435f14dff7e22b9b20930fc56e598f7e95 SHA256 100229337d43f8bf6e931ee50494d7ebc0f565ac5382199cc8f74bde664830ad
diff --git a/sci-mathematics/why/files/why-2.19-makefile_sandbox.patch b/sci-mathematics/why/files/why-2.19-makefile_sandbox.patch
new file mode 100644
index 000000000..3ec92830a
--- /dev/null
+++ b/sci-mathematics/why/files/why-2.19-makefile_sandbox.patch
@@ -0,0 +1,75 @@
+diff -Naur why-2.19-orig/Makefile.in why-2.19-ptch/Makefile.in
+--- why-2.19-orig/Makefile.in	2009-06-23 12:09:43.000000000 +0000
++++ why-2.19-ptch/Makefile.in	2009-09-04 14:43:22.000000000 +0000
+@@ -777,9 +777,9 @@
+ 	cp -f $(VO7) $(LIBDIR)/why/coq7
+ install-coq-v8: 
+ 	if test -w $(COQLIB) ; then \
+-	 mkdir -p $(COQLIB)/user-contrib ; \
+-	 cp -f $(V8FILES) $(COQLIB)/user-contrib ; \
+-	 cp -f $(VO8) $(COQLIB)/user-contrib ; \
++	 mkdir -p $(DESTDIR)/$(COQLIB)/user-contrib ; \
++	 cp -f $(V8FILES) $(DESTDIR)/$(COQLIB)/user-contrib ; \
++	 cp -f $(VO8) $(DESTDIR)/$(COQLIB)/user-contrib ; \
+ 	else \
+ 	echo "Cannot copy to Coq standard library. Add $(LIBDIR)/why/coq to Coq include path." ;\
+ 	mkdir -p $(LIBDIR)/why/coq ;\
+@@ -788,18 +788,18 @@
+ 
+ install-pvs-no:
+ install-pvs-yes: $(PVSFILES)
+-	mkdir -p $(PVSLIB)/why
+-	cp $(PVSFILES) $(PVSFILES:.pvs=.prf) $(PVSLIB)/why
+-	cp lib/pvs/top.pvs lib/pvs/pvscontext.el $(PVSLIB)/why
++	mkdir -p $(DESTDIR)/$(PVSLIB)/why
++	cp $(PVSFILES) $(PVSFILES:.pvs=.prf) $(DESTDIR)/$(PVSLIB)/why
++	cp lib/pvs/top.pvs lib/pvs/pvscontext.el $(DESTDIR)/$(PVSLIB)/why
+ 	@echo "======  Compiling PVS theories, this may take some time ======"
+-	(cd $(PVSLIB)/why ; @PVSC@ -batch -l pvscontext.el -q -v 2 > top.out)
++	(cd $(DESTDIR)/$(PVSLIB)/why ; @PVSC@ -batch -l pvscontext.el -q -v 2 > top.out)
+ 	@echo "======  Done compiling PVS theories ======"
+ 
+ install-mizar-no:
+ install-mizar-yes:
+-	mkdir -p @MIZARLIB@/mml/dict
+-	cp lib/mizar/why.miz @MIZARLIB@/mml
+-	cp lib/mizar/dict/why.voc @MIZARLIB@/mml/dict
++	mkdir -p $(DESTDIR)/@MIZARLIB@/mml/dict
++	cp lib/mizar/why.miz $(DESTDIR)/@MIZARLIB@/mml
++	cp lib/mizar/dict/why.voc $(DESTDIR)/@MIZARLIB@/mml/dict
+ 
+ local-install: $(BINARY) $(WHYCONFIG) $(CADUCEUS) $(JESSIE) bin/gwhy.$(OCAMLBEST) byte bin/gwhy.byte 
+ 	cp $(BINARY) $$HOME/bin/why
+@@ -817,15 +817,15 @@
+ # 	cp -f $(WHY2HTML) $$HOME/bin/$$OSTYPE/why2html
+ # 	cp -f $(DP) $$HOME/bin/$$OSTYPE/dp
+ # 	cp -f $(RVMERGE) $$HOME/bin/$$OSTYPE/rv_merge
+-# #	mkdir -p $(COQLIB)/contrib7/why
+-# #	cp -f $(VO7) $(VFILES) $(COQLIB)/contrib7/why
+-# #	mkdir -p $(COQLIB)/contrib/why
+-# #	cp -f $(VO8) $(VFILES) $(COQLIB)/contrib/why
+-# 	mkdir -p $(PVSLIB)/why
+-# 	cp $(PVSFILES) $(PVSLIB)/why
+-# 	mkdir -p $(MIZFILES)/mml/dict
+-# 	cp lib/mizar/why.miz $(MIZFILES)/mml
+-# 	cp lib/mizar/dict/why.voc $(MIZFILES)/mml/dict
++# #	mkdir -p $(DESTDIR)/$(COQLIB)/contrib7/why
++# #	cp -f $(VO7) $(VFILES) $(DESTDIR)/$(COQLIB)/contrib7/why
++# #	mkdir -p $(DESTDIR)/$(COQLIB)/contrib/why
++# #	cp -f $(VO8) $(VFILES) $(DESTDIR)/$(COQLIB)/contrib/why
++# 	mkdir -p $(DESTDIR)/$(PVSLIB)/why
++# 	cp $(PVSFILES) $(DESTDIR)/$(PVSLIB)/why
++# 	mkdir -p $(DESTDIR)/$(MIZFILES)/mml/dict
++# 	cp lib/mizar/why.miz $(DESTDIR)/$(MIZFILES)/mml
++# 	cp lib/mizar/dict/why.voc $(DESTDIR)/$(MIZFILES)/mml/dict
+ # 	mkdir -p $$HOME/man/man1
+ # 	cp -f doc/*.1 $$HOME/man/man1
+ 
+@@ -1119,7 +1119,6 @@
+ 	rm -f $(GENERATED)
+ 	make -C atp clean
+ 	make -C doc clean
+-	make -C examples-v7 clean
+ 	make -C examples clean
+ 
+ dist-clean:: clean
diff --git a/sci-mathematics/why/why-2.19.ebuild b/sci-mathematics/why/why-2.19.ebuild
index 353650be8..60c0c6ffa 100644
--- a/sci-mathematics/why/why-2.19.ebuild
+++ b/sci-mathematics/why/why-2.19.ebuild
@@ -29,17 +29,23 @@ src_unpack() {
 	unpack ${A}
 	cd ${S}
 
-	epatch "${FILESDIR}/${P}-sandbox.patch"
+	epatch "${FILESDIR}/${P}-makefile_sandbox.patch"
 
 	mv jc/jc_ast.mli jc/jc_ast.ml
 	mv jc/jc_env.mli jc/jc_env.ml
 	epatch "${FILESDIR}/${P}-jessie_lib.patch"
 
+	#to build with apron-0.9.10
+	sed -i configure.in \
+		-e "s/oct_caml/octMPQ_caml/g" \
+		-e "s/box_caml/boxMPQ_caml/g" \
+		-e "s/polka_caml/polkaMPQ_caml/g"
+
 	eautoreconf
 }
 
 src_compile(){
-	econf $(use_enable apron) || die "econf failed"
+	econf $(use_enable apron) PATH="/usr/bin:$PATH" || die "econf failed"
 	emake DESTDIR="/" || die "emake failed"
 }