This is an automated email from the git hooks/post-receive script. glondu pushed a commit to branch master in repository frama-c.
commit d5b8530de604649aadd6cb819e7674816861930c Author: Stephane Glondu <st...@glondu.net> Date: Sun Dec 8 12:24:51 2013 +0100 Fix compilation with OCaml 4.01.0 (Closes: #731637) --- .../0005-Fix-compilation-with-OCaml-4.01.0.patch | 171 +++++++++++++++++++++ debian/patches/series | 1 + 2 files changed, 172 insertions(+) diff --git a/debian/patches/0005-Fix-compilation-with-OCaml-4.01.0.patch b/debian/patches/0005-Fix-compilation-with-OCaml-4.01.0.patch new file mode 100644 index 0000000..add5050 --- /dev/null +++ b/debian/patches/0005-Fix-compilation-with-OCaml-4.01.0.patch @@ -0,0 +1,171 @@ +From: Stephane Glondu <st...@glondu.net> +Date: Sun, 8 Dec 2013 12:17:33 +0100 +Subject: Fix compilation with OCaml 4.01.0 + +Author: Virgile Prevosto +Origin: https://github.com/vprevosto/opam-repository/blob/master/packages/frama-c.20130601/files/4.01-compat.patch +Bug-Debian: http://bugs.debian.org/cgi-bin/bugreport.cgi?bug=731637 +--- + external/hptmap.ml | 15 +++++++++++++++ + external/hptmap.mli | 3 +++ + src/kernel/file.ml | 5 +---- + src/lib/hptset.ml | 2 ++ + src/lib/hptset.mli | 2 ++ + src/lib/setWithNearest.ml | 8 ++++++++ + src/memory_state/cvalue.mli | 4 ++-- + src/wp/qed/src/idxset.ml | 4 ++++ + 8 files changed, 37 insertions(+), 6 deletions(-) + +diff --git a/external/hptmap.ml b/external/hptmap.ml +index 39bacc4..4737d96 100644 +--- a/external/hptmap.ml ++++ b/external/hptmap.ml +@@ -357,6 +357,21 @@ struct + 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 --git a/external/hptmap.mli b/external/hptmap.mli +index 979e8e8..b3b5e8e 100644 +--- a/external/hptmap.mli ++++ b/external/hptmap.mli +@@ -84,6 +84,9 @@ this function will be renamed "hash" in the future *) + 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 --git a/src/kernel/file.ml b/src/kernel/file.ml +index 3258366..a34aee3 100644 +--- a/src/kernel/file.ml ++++ b/src/kernel/file.ml +@@ -322,6 +322,7 @@ object(self) + 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 @@ object(self) + 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 --git a/src/lib/hptset.ml b/src/lib/hptset.ml +index e5fe2db..5de7957 100644 +--- a/src/lib/hptset.ml ++++ b/src/lib/hptset.ml +@@ -26,6 +26,7 @@ module type S = sig + 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 @@ module Make(X: Id_Datatype) + 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 --git a/src/lib/hptset.mli b/src/lib/hptset.mli +index e1ae83d..2f1ef49 100644 +--- a/src/lib/hptset.mli ++++ b/src/lib/hptset.mli +@@ -50,6 +50,8 @@ module type S = sig + 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 --git a/src/lib/setWithNearest.ml b/src/lib/setWithNearest.ml +index 0123bd7..1408fa4 100644 +--- a/src/lib/setWithNearest.ml ++++ b/src/lib/setWithNearest.ml +@@ -165,6 +165,14 @@ module Make(Ord: Datatype.S) = struct + 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 --git a/src/memory_state/cvalue.mli b/src/memory_state/cvalue.mli +index 602bc4a..ac60f7b 100644 +--- a/src/memory_state/cvalue.mli ++++ b/src/memory_state/cvalue.mli +@@ -35,8 +35,8 @@ module V : sig + 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 --git a/src/wp/qed/src/idxset.ml b/src/wp/qed/src/idxset.ml +index 32dd645..7549515 100644 +--- a/src/wp/qed/src/idxset.ml ++++ b/src/wp/qed/src/idxset.ml +@@ -59,6 +59,8 @@ struct + + 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 @@ struct + + 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/debian/patches/series b/debian/patches/series index fff4336..cfa21fb 100644 --- a/debian/patches/series +++ b/debian/patches/series @@ -2,3 +2,4 @@ 0002-Use-bin-cp-instead-of-usr-bin-install.patch 0003-Disable-CHMOD_RO-invocations.patch 0004-Fix-auto-detection-of-ocaml-zarith.patch +0005-Fix-compilation-with-OCaml-4.01.0.patch -- Alioth's /usr/local/bin/git-commit-notice on /srv/git.debian.org/git/pkg-ocaml-maint/packages/frama-c.git _______________________________________________ Pkg-ocaml-maint-commits mailing list Pkg-ocaml-maint-commits@lists.alioth.debian.org http://lists.alioth.debian.org/cgi-bin/mailman/listinfo/pkg-ocaml-maint-commits