From mboxrd@z Thu Jan 1 00:00:00 1970 Return-Path: Received: from lists.gentoo.org (pigeon.gentoo.org [208.92.234.80]) by finch.gentoo.org (Postfix) with ESMTP id 05FE6138E66 for ; Mon, 24 Feb 2014 17:56:10 +0000 (UTC) Received: from pigeon.gentoo.org (localhost [127.0.0.1]) by pigeon.gentoo.org (Postfix) with SMTP id D81ACE0A9E; Mon, 24 Feb 2014 17:56:05 +0000 (UTC) Received: from smtp.gentoo.org (smtp.gentoo.org [140.211.166.183]) (using TLSv1.2 with cipher AECDH-AES256-SHA (256/256 bits)) (No client certificate requested) by pigeon.gentoo.org (Postfix) with ESMTPS id 62036E0A9E for ; Mon, 24 Feb 2014 17:56:05 +0000 (UTC) Received: from spoonbill.gentoo.org (spoonbill.gentoo.org [81.93.255.5]) (using TLSv1.2 with cipher AECDH-AES256-SHA (256/256 bits)) (No client certificate requested) by smtp.gentoo.org (Postfix) with ESMTPS id 7EE2E33F9C9 for ; Mon, 24 Feb 2014 17:56:03 +0000 (UTC) Received: from localhost.localdomain (localhost [127.0.0.1]) by spoonbill.gentoo.org (Postfix) with ESMTP id 6CC4318875 for ; Mon, 24 Feb 2014 17:56:01 +0000 (UTC) From: "Andrew Savchenko" To: gentoo-commits@lists.gentoo.org Content-Transfer-Encoding: 8bit Content-type: text/plain; charset=UTF-8 Reply-To: gentoo-dev@lists.gentoo.org, "Andrew Savchenko" Message-ID: <1393264475.6fea4eb8b6cccd829f23b3f377d84e0aceadf8da.bircoph@gentoo> Subject: [gentoo-commits] proj/sci:master commit in: sci-mathematics/frama-c/files/, sci-mathematics/frama-c/ X-VCS-Repository: proj/sci X-VCS-Files: sci-mathematics/frama-c/ChangeLog sci-mathematics/frama-c/files/frama-c-make.patch sci-mathematics/frama-c/files/frama-c-ocaml-4.01.patch sci-mathematics/frama-c/frama-c-20130601.ebuild X-VCS-Directories: sci-mathematics/frama-c/files/ sci-mathematics/frama-c/ X-VCS-Committer: bircoph X-VCS-Committer-Name: Andrew Savchenko X-VCS-Revision: 6fea4eb8b6cccd829f23b3f377d84e0aceadf8da X-VCS-Branch: master Date: Mon, 24 Feb 2014 17:56:01 +0000 (UTC) Precedence: bulk List-Post: List-Help: List-Unsubscribe: List-Subscribe: List-Id: Gentoo Linux mail X-BeenThere: gentoo-commits@lists.gentoo.org X-Archives-Salt: 930277f4-3359-4302-9668-9f3dbf3e25fa X-Archives-Hash: e6d95b0553dd5dad20fc705b4fdc70d7 commit: 6fea4eb8b6cccd829f23b3f377d84e0aceadf8da Author: Andrew Savchenko gmail com> AuthorDate: Mon Feb 24 17:54:35 2014 +0000 Commit: Andrew Savchenko gmail 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 +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 +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 +}