public inbox for gentoo-commits@lists.gentoo.org
 help / color / mirror / Atom feed
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
+}


             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