[Pkg-ocaml-maint-commits] [why] 12/14: add patch hashtabl to fix type error

[Ralf Treinen]

This is an automated email from the git hooks/post-receive script.

treinen pushed a commit to branch master
in repository why.

commit 631c48c3ec05817867587bd2a2ac573be9dce771
Author: Ralf Treinen <treinen at free.fr>
Date:   Fri Jan 17 21:42:58 2014 +0100

    add patch hashtabl to fix type error
---
 debian/changelog       |  1 +
 debian/patches/hashtbl | 56 ++++++++++++++++++++++++++++++++++++++++++++++++++
 debian/patches/series  |  1 +
 3 files changed, 58 insertions(+)

diff --git a/debian/changelog b/debian/changelog
index af853e0..3483da4 100644
--- a/debian/changelog
+++ b/debian/changelog
@@ -11,6 +11,7 @@ why (2.33-1) unstable; urgency=low
     - 0007-Replace-caduceus-invocation-by-Frama-C.patch
   * New patch deprecated-or to replace "or" by "||", needed for more strict
     checks in ocaml 4
+  * New patch hashtbl to fix compilation with ocaml 4.01, taken from fedora.
 
  -- Ralf Treinen <treinen at debian.org>  Fri, 17 Jan 2014 20:36:07 +0100
 
diff --git a/debian/patches/hashtbl b/debian/patches/hashtbl
new file mode 100644
index 0000000..d430202
--- /dev/null
+++ b/debian/patches/hashtbl
@@ -0,0 +1,56 @@
+Author: Jerry James <loganjerry at gmail.com >
+Description: fix type error with ocaml 4.01
+
+Index: why/jc/jc_annot_inference.ml
+===================================================================
+--- why.orig/jc/jc_annot_inference.ml	2014-01-17 21:43:53.332548129 +0100
++++ why/jc/jc_annot_inference.ml	2014-01-17 21:45:18.672822708 +0100
+@@ -84,7 +84,7 @@
+ let unfolding_of_app app =
+   let f = app.jc_app_fun in
+   let _, term_or_assertion =
+-    try Hashtbl.find Jc_typing.logic_functions_table f.jc_logic_info_tag
++   try IntHashtblIter.find Jc_typing.logic_functions_table f.jc_logic_info_tag
+     with Not_found -> assert false
+   in
+   match term_or_assertion with
+@@ -2528,7 +2528,7 @@
+ 	  in
+ 	  let els = call.jc_call_args in
+ 	  let _,_,fs,_ =
+-            Hashtbl.find Jc_typing.functions_table fi.jc_fun_info_tag
++            IntHashtblIter.find Jc_typing.functions_table fi.jc_fun_info_tag
+           in
+           (* Collect preconditions of functions called. *)
+           let reqa = fs.jc_fun_requires in
+@@ -3543,7 +3543,7 @@
+   (* Compute abstract value at function call *)
+   let curinvs = List.fold_left (ai_expr iaio abs) curinvs args in
+   let _f, _pos, spec, _body =
+-    Hashtbl.find Jc_typing.functions_table f.jc_fun_info_tag
++    IntHashtblIter.find Jc_typing.functions_table f.jc_fun_info_tag
+   in
+ (*   begin match body with None -> () | Some body -> *)
+ (*     if Jc_options.interprocedural then *)
+@@ -3732,9 +3732,9 @@
+ 
+     (* Add global variables as abstract variables in [env]. *)
+     let globvars =
+-      Hashtbl.fold (fun _tag (vi,_e) acc ->
+-		      Vai.all_variables (new term_var vi) @ acc
+-		   ) Jc_typing.variables_table []
++      IntHashtblIter.fold (fun _tag (vi,_e) acc ->
++			   Vai.all_variables (new term_var vi) @ acc
++			  ) Jc_typing.variables_table []
+     in
+     let env = Environment.add env (Array.of_list globvars) [||] in
+ 
+@@ -4164,7 +4164,7 @@
+     (fun fi ->
+        let fi, _, fs, slo =
+ 	 try
+-	   Hashtbl.find Jc_typing.functions_table fi.jc_fun_info_tag
++	   IntHashtblIter.find Jc_typing.functions_table fi.jc_fun_info_tag
+ 	 with Not_found -> assert false (* should never happen *)
+        in
+        match slo with
diff --git a/debian/patches/series b/debian/patches/series
index ad50418..5da5075 100644
--- a/debian/patches/series
+++ b/debian/patches/series
@@ -1 +1,2 @@
 deprecated-or
+hashtbl

-- 
Alioth's /usr/local/bin/git-commit-notice on /srv/git.debian.org/git/pkg-ocaml-maint/packages/why.git