[Pkg-ocaml-maint-commits] [frama-c] 02/03: Fix compilation with OCaml 4.01.0 (Closes: #731637)
Stéphane Glondu
glondu at moszumanska.debian.org
Sun Dec 8 11:37:26 UTC 2013
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 <steph at 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 <steph at 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
More information about the Pkg-ocaml-maint-commits
mailing list