From: "Andrew Savchenko" <bircoph@gmail.com>
To: gentoo-commits@lists.gentoo.org
Subject: [gentoo-commits] proj/sci:master commit in: sci-mathematics/frama-c/files/, sci-mathematics/frama-c/
Date: Mon, 24 Feb 2014 17:56:01 +0000 (UTC) [thread overview]
Message-ID: <1393264475.6fea4eb8b6cccd829f23b3f377d84e0aceadf8da.bircoph@gentoo> (raw)
commit: 6fea4eb8b6cccd829f23b3f377d84e0aceadf8da
Author: Andrew Savchenko <bircoph <AT> gmail <DOT> com>
AuthorDate: Mon Feb 24 17:54:35 2014 +0000
Commit: Andrew Savchenko <bircoph <AT> gmail <DOT> com>
CommitDate: Mon Feb 24 17:54:35 2014 +0000
URL: http://git.overlays.gentoo.org/gitweb/?p=proj/sci.git;a=commit;h=6fea4eb8
sci-mathematics/frama-c: version bump
Upgrade to EAPI 5.
Fix build with make >= 4.0.
Support build with recent ocaml-4.01.
---
sci-mathematics/frama-c/ChangeLog | 8 +-
sci-mathematics/frama-c/files/frama-c-make.patch | 12 ++
.../frama-c/files/frama-c-ocaml-4.01.patch | 145 +++++++++++++++++++++
sci-mathematics/frama-c/frama-c-20130601.ebuild | 65 +++++++++
4 files changed, 229 insertions(+), 1 deletion(-)
diff --git a/sci-mathematics/frama-c/ChangeLog b/sci-mathematics/frama-c/ChangeLog
index 6ae7f62..6ece894 100644
--- a/sci-mathematics/frama-c/ChangeLog
+++ b/sci-mathematics/frama-c/ChangeLog
@@ -1,7 +1,13 @@
# ChangeLog for sci-mathematics/frama-c
-# Copyright 1999-2013 Gentoo Foundation; Distributed under the GPL v2
+# Copyright 1999-2014 Gentoo Foundation; Distributed under the GPL v2
# $Header: $
+*frama-c-20130601 (24 Feb 2014)
+
+ 24 Feb 2014; Andrew Savchenko <bircoph@gmail.com> +frama-c-20130601.ebuild,
+ +files/frama-c-ocaml-4.01.patch, +files/frama-c-make.patch:
+ Version bump. Fix build with make >= 4.x, add ocaml-4.01 support.
+
14 Jan 2013; J.-C. Demay <jcdemay@gmail.com>
+frama-c-20120901.ebuild, -frama-c-20111001.ebuild:
version bump
diff --git a/sci-mathematics/frama-c/files/frama-c-make.patch b/sci-mathematics/frama-c/files/frama-c-make.patch
new file mode 100644
index 0000000..7e0b1d9
--- /dev/null
+++ b/sci-mathematics/frama-c/files/frama-c-make.patch
@@ -0,0 +1,12 @@
+--- frama-c-Oxygen-20120901/configure.in.orig 2012-09-19 15:56:17.000000000 +0400
++++ frama-c-Oxygen-20120901/configure.in 2014-02-24 19:02:44.616467203 +0400
+@@ -61,7 +61,8 @@
+ MAKE_MAJOR=`$MAKE -v | sed -n -f bin/sed_get_make_major `
+ MAKE_MINOR=`$MAKE -v | sed -n -f bin/sed_get_make_minor `
+ echo $ECHO_N "make version is $MAKE_DISTRIB Make $MAKE_MAJOR.$MAKE_MINOR: $ECHO_C"
+-if test "$MAKE_DISTRIB" != GNU -o "$MAKE_MAJOR" -lt 3 -o "$MAKE_MINOR" -lt 81;
++if test "$MAKE_DISTRIB" != GNU -o \( "$MAKE_MAJOR" -eq 3 -a "$MAKE_MINOR" -lt 81 \)
++ -o "$MAKE_MAJOR" -lt 3;
+ then
+ echo "${ECHO_T}"
+ AC_MSG_ERROR([unsupported version; GNU Make version 3.81
diff --git a/sci-mathematics/frama-c/files/frama-c-ocaml-4.01.patch b/sci-mathematics/frama-c/files/frama-c-ocaml-4.01.patch
new file mode 100644
index 0000000..44b86b3
--- /dev/null
+++ b/sci-mathematics/frama-c/files/frama-c-ocaml-4.01.patch
@@ -0,0 +1,145 @@
+https://raw.github.com/vprevosto/opam-repository/2e0db18a822eb1818cd39a02e2ca8dde071e5d51/packages/frama-c.20130601/files/4.01-compat.patch
+diff -Naur frama-c-Fluorine-20130601/external/hptmap.ml frama-c-Fluorine-20130601.new/external/hptmap.ml
+--- frama-c-Fluorine-20130601/external/hptmap.ml 2013-06-11 18:15:19.000000000 +0400
++++ frama-c-Fluorine-20130601.new/external/hptmap.ml 2014-02-24 20:17:10.749247061 +0400
+@@ -357,6 +357,21 @@
+ find htr
+
+
++ let find_key key htr =
++ let id = Key.id key in
++ let rec find htr =
++ match htr with
++ | Empty ->
++ raise Not_found
++ | Leaf (key', _, _) ->
++ if Key.equal key key' then
++ key'
++ else
++ raise Not_found
++ | Branch (_, mask, tree0, tree1, _) ->
++ find (if (id land mask) = 0 then tree0 else tree1)
++ in
++ find htr
+
+
+ let mem key htr =
+diff -Naur frama-c-Fluorine-20130601/external/hptmap.mli frama-c-Fluorine-20130601.new/external/hptmap.mli
+--- frama-c-Fluorine-20130601/external/hptmap.mli 2013-06-11 18:15:19.000000000 +0400
++++ frama-c-Fluorine-20130601.new/external/hptmap.mli 2014-02-24 20:17:10.769246098 +0400
+@@ -84,6 +84,9 @@
+ for [k], it is overridden. *)
+
+ val find : key -> t -> V.t
++
++ val find_key: key -> t -> key
++
+ val remove : key -> t -> t
+ (** [remove k m] returns the map [m] deprived from any binding involving
+ [k]. *)
+diff -Naur frama-c-Fluorine-20130601/src/kernel/file.ml frama-c-Fluorine-20130601.new/src/kernel/file.ml
+--- frama-c-Fluorine-20130601/src/kernel/file.ml 2013-06-11 18:13:13.000000000 +0400
++++ frama-c-Fluorine-20130601.new/src/kernel/file.ml 2014-02-24 20:17:10.773245905 +0400
+@@ -322,6 +322,7 @@
+ Printer.pp_logic_var lv Printer.pp_varinfo v
+
+ method vlogic_info_decl li =
++ Logic_var.Hashtbl.add known_logic_info li.l_var_info li;
+ List.iter
+ (fun lv ->
+ if lv.lv_kind <> LVFormal then
+@@ -769,10 +770,6 @@
+ DoChildren
+ | _ -> DoChildren
+
+- method vlogic_info_decl li =
+- Logic_var.Hashtbl.add known_logic_info li.l_var_info li;
+- DoChildren
+-
+ method vlogic_info_use li =
+ let unknown () =
+ check_abort "logic function %s has no information" li.l_var_info.lv_name
+diff -Naur frama-c-Fluorine-20130601/src/lib/hptset.ml frama-c-Fluorine-20130601.new/src/lib/hptset.ml
+--- frama-c-Fluorine-20130601/src/lib/hptset.ml 2013-06-11 18:13:42.000000000 +0400
++++ frama-c-Fluorine-20130601.new/src/lib/hptset.ml 2014-02-24 20:17:10.773245905 +0400
+@@ -26,6 +26,7 @@
+ val empty: t
+ val is_empty: t -> bool
+ val mem: elt -> t -> bool
++ val find: elt -> t -> elt
+ val add: elt -> t -> t
+ val singleton: elt -> t
+ val remove: elt -> t -> t
+@@ -71,6 +72,7 @@
+ type elt = X.t
+
+ let add k = add k ()
++ let find = find_key
+ let iter f = iter (fun x () -> f x)
+ let fold f = fold (fun x () -> f x)
+
+diff -Naur frama-c-Fluorine-20130601/src/lib/hptset.mli frama-c-Fluorine-20130601.new/src/lib/hptset.mli
+--- frama-c-Fluorine-20130601/src/lib/hptset.mli 2013-06-11 18:13:42.000000000 +0400
++++ frama-c-Fluorine-20130601.new/src/lib/hptset.mli 2014-02-24 20:17:10.777245712 +0400
+@@ -50,6 +50,8 @@
+ val mem: elt -> t -> bool
+ (** [mem x s] tests whether [x] belongs to the set [s]. *)
+
++ val find: elt -> t -> elt
++
+ val add: elt -> t -> t
+ (** [add x s] returns a set containing all elements of [s],
+ plus [x]. If [x] was already in [s], [s] is returned unchanged. *)
+diff -Naur frama-c-Fluorine-20130601/src/lib/setWithNearest.ml frama-c-Fluorine-20130601.new/src/lib/setWithNearest.ml
+--- frama-c-Fluorine-20130601/src/lib/setWithNearest.ml 2013-06-11 18:13:42.000000000 +0400
++++ frama-c-Fluorine-20130601.new/src/lib/setWithNearest.ml 2014-02-24 20:17:10.781245519 +0400
+@@ -165,6 +165,14 @@
+ let c = Ord.compare x v in
+ c = 0 || mem x (if c < 0 then l else r)
+
++ let rec find x = function
++ | Empty -> raise Not_found
++ | Node(l, v, r, _) ->
++ match Ord.compare x v with
++ | c when c < 0 -> find x l
++ | 0 -> v
++ | _ -> find x r
++
+ let singleton x = Node(Empty, x, Empty, 1)
+
+ let rec remove x = function
+diff -Naur frama-c-Fluorine-20130601/src/memory_state/cvalue.mli frama-c-Fluorine-20130601.new/src/memory_state/cvalue.mli
+--- frama-c-Fluorine-20130601/src/memory_state/cvalue.mli 2013-06-11 18:13:51.000000000 +0400
++++ frama-c-Fluorine-20130601.new/src/memory_state/cvalue.mli 2014-02-24 20:17:10.781245519 +0400
+@@ -35,8 +35,8 @@
+ include module type of Location_Bytes
+ (* Too many aliases, and OCaml module system is not able to keep track
+ of all of them. Use some shortcuts *)
+- with type z = Location_Bytes.z
+- and type M.t = Location_Bytes.M.t
++ with type M.t = Location_Bytes.M.t
++ and type z = Location_Bytes.z
+
+ include Lattice_With_Isotropy.S
+ with type t := t
+diff -Naur frama-c-Fluorine-20130601/src/wp/qed/src/idxset.ml frama-c-Fluorine-20130601.new/src/wp/qed/src/idxset.ml
+--- frama-c-Fluorine-20130601/src/wp/qed/src/idxset.ml 2013-06-11 18:13:23.000000000 +0400
++++ frama-c-Fluorine-20130601.new/src/wp/qed/src/idxset.ml 2014-02-24 20:17:10.785245326 +0400
+@@ -59,6 +59,8 @@
+
+ let mem e s = mem_k (E.id e) s
+
++ let find e s = if mem e s then e else raise Not_found
++
+ let lowest_bit x = x land (-x)
+
+ let branching_bit p0 p1 = lowest_bit (p0 lxor p1)
+@@ -360,6 +362,8 @@
+
+ let mem e s = mem_k (index e) s
+
++ let find e s = if mem e s then e else raise Not_found
++
+ let mask k m = (k lor (m-1)) land (lnot m)
+
+ (* we first write a naive implementation of [highest_bit]
diff --git a/sci-mathematics/frama-c/frama-c-20130601.ebuild b/sci-mathematics/frama-c/frama-c-20130601.ebuild
new file mode 100644
index 0000000..09cfe96
--- /dev/null
+++ b/sci-mathematics/frama-c/frama-c-20130601.ebuild
@@ -0,0 +1,65 @@
+# Copyright 1999-2014 Gentoo Foundation
+# Distributed under the terms of the GNU General Public License v2
+# $Header: $
+
+EAPI="5"
+
+inherit autotools eutils
+
+DESCRIPTION="Framework for analysis of source codes written in C"
+HOMEPAGE="http://frama-c.com"
+NAME="Fluorine"
+SRC_URI="http://frama-c.com/download/${PN/-c/-c-$NAME}-${PV/_/-}.tar.gz"
+
+LICENSE="LGPL-2"
+SLOT="0"
+KEYWORDS="~amd64 ~ppc ~x86"
+IUSE="doc gtk +ocamlopt"
+RESTRICT="strip"
+
+DEPEND=">=dev-lang/ocaml-3.10.2[ocamlopt?]
+ >=dev-ml/ocamlgraph-1.8.2[gtk?,ocamlopt?]
+ dev-ml/zarith
+ sci-mathematics/ltl2ba
+ sci-mathematics/alt-ergo
+ gtk? ( >=x11-libs/gtksourceview-2.8
+ >=gnome-base/libgnomecanvas-2.26
+ >=dev-ml/lablgtk-2.14[sourceview,gnomecanvas,ocamlopt?] )"
+RDEPEND="${DEPEND}"
+
+S="${WORKDIR}/${PN/-c/-c-$NAME}-${PV/_/-}"
+
+src_prepare(){
+ rm share/libc/test.c
+ touch config_file
+ epatch "${FILESDIR}/${PN}-make.patch" \
+ "${FILESDIR}/${PN}-ocaml-4.01.patch"
+
+ eautoreconf
+}
+
+src_configure(){
+ if use gtk; then
+ myconf="--enable-gui"
+ else
+ myconf="--disable-gui"
+ fi
+
+ econf ${myconf}
+}
+
+src_compile(){
+ # dependencies can not be processed in parallel,
+ # this is the intended behavior.
+ emake -j1 depend
+ emake all top DESTDIR="/"
+}
+
+src_install(){
+ emake install DESTDIR="${D}"
+ dodoc Changelog doc/README
+
+ if use doc; then
+ dodoc doc/manuals/*.pdf
+ fi
+}
next reply other threads:[~2014-02-24 17:56 UTC|newest]
Thread overview: 6+ messages / expand[flat|nested] mbox.gz Atom feed top
2014-02-24 17:56 Andrew Savchenko [this message]
-- strict thread matches above, loose matches on Subject: below --
2011-05-11 23:50 [gentoo-commits] proj/sci:master commit in: sci-mathematics/frama-c/files/, sci-mathematics/frama-c/ Jonathan-Christofer Demay
2011-02-28 10:47 Jonathan-Christofer Demay
2011-02-23 14:17 Jonathan-Christofer Demay
2011-02-23 13:23 Jonathan-Christofer Demay
2011-02-14 0:33 Jonathan-Christofer Demay
Reply instructions:
You may reply publicly to this message via plain-text email
using any one of the following methods:
* Save the following mbox file, import it into your mail client,
and reply-to-all from there: mbox
Avoid top-posting and favor interleaved quoting:
https://en.wikipedia.org/wiki/Posting_style#Interleaved_style
* Reply using the --to, --cc, and --in-reply-to
switches of git-send-email(1):
git send-email \
--in-reply-to=1393264475.6fea4eb8b6cccd829f23b3f377d84e0aceadf8da.bircoph@gentoo \
--to=bircoph@gmail.com \
--cc=gentoo-commits@lists.gentoo.org \
--cc=gentoo-dev@lists.gentoo.org \
/path/to/YOUR_REPLY
https://kernel.org/pub/software/scm/git/docs/git-send-email.html
* If your mail client supports setting the In-Reply-To header
via mailto: links, try the mailto: link
Be sure your reply has a Subject: header at the top and a blank line
before the message body.
This is a public inbox, see mirroring instructions
for how to clone and mirror all data and code used for this inbox