This is an automated email from the git hooks/post-receive script.
mehdi pushed a commit to branch master
in repository frama-c.
commit 809c57f198d8ab8de7c352a7eefb08d957bbb755
Author: Mehdi Dogguy <me...@debian.org>
Date: Fri Aug 11 12:06:53 2017 -0400
Refresh patches
---
.../0001-Fix-spelling-error-in-binary.patch | 422 ++-------------------
...002-Use-bin-cp-instead-of-usr-bin-install.patch | 4 +-
.../0003-Disable-CHMOD_RO-invocations.patch | 4 +-
...mlfind-package-lablgtk2-gnome.gnomecanvas.patch | 4 +-
.../0005-Value.cmo-needs-LoopAnalysis.cmo.patch | 4 +-
...0006-gui.byte-needs-TARGETS_GUI_BYTE-only.patch | 6 +-
.../patches/0007-Fix-FTBFS-with-OCaml-4.05.0.patch | 39 +-
7 files changed, 59 insertions(+), 424 deletions(-)
diff --git a/debian/patches/0001-Fix-spelling-error-in-binary.patch
b/debian/patches/0001-Fix-spelling-error-in-binary.patch
index 8177c60..a164401 100644
--- a/debian/patches/0001-Fix-spelling-error-in-binary.patch
+++ b/debian/patches/0001-Fix-spelling-error-in-binary.patch
@@ -3,36 +3,16 @@ Date: Thu, 21 Jan 2016 23:48:35 +0100
Subject: Fix spelling-error-in-binary
---
- man/frama-c.1 | 4 ++--
- src/kernel_internals/typing/asm_contracts.ml | 2 +-
- src/kernel_services/abstract_interp/lmap_sig.mli | 2 +-
- src/kernel_services/analysis/exn_flow.ml | 2 +-
- src/kernel_services/analysis/logic_interp.ml | 14 +++++++-------
- src/kernel_services/ast_queries/file.ml | 2 +-
- src/kernel_services/ast_queries/logic_const.mli | 2 +-
- src/kernel_services/ast_queries/logic_env.ml | 4 ++--
- src/kernel_services/ast_queries/logic_typing.ml | 2 +-
- src/kernel_services/plugin_entry_points/kernel.ml | 2 +-
- src/libraries/utils/bitvector.ml | 2 +-
- src/plugins/aorai/aorai_utils.ml | 2 +-
- src/plugins/occurrence/register.ml | 2 +-
- src/plugins/scope/dpds_gui.ml | 2 +-
- .../security_slicing/security_slicing_parameters.ml | 2 +-
- src/plugins/slicing/fct_slice.ml | 4 ++--
- src/plugins/value/gui_files/register_gui.ml | 2 +-
- src/plugins/value/value_parameters.ml | 2 +-
- src/plugins/value_types/cvalue.ml | 2 +-
- src/plugins/wp/VC.mli | 2 +-
- src/plugins/wp/qed/src/logic.mli | 2 +-
- src/plugins/wp/wpAnnot.ml | 2 +-
- src/plugins/wp/wp_parameters.ml | 2 +-
- 23 files changed, 32 insertions(+), 32 deletions(-)
+ man/frama-c.1 | 4 ++--
+ src/kernel_services/ast_data/cil_types.mli | 2 +-
+ src/plugins/e-acsl/typing.ml | 4 ++--
+ 3 files changed, 5 insertions(+), 5 deletions(-)
diff --git a/man/frama-c.1 b/man/frama-c.1
-index 67f47d2..9eccab8 100644
+index fac74bc..5801d7b 100644
--- a/man/frama-c.1
+++ b/man/frama-c.1
-@@ -389,14 +389,14 @@ alias of
+@@ -404,14 +404,14 @@ alias of
.TP
.B -print-plugin-path
outputs the directory where Frama-C searches its plugins
@@ -49,358 +29,38 @@ index 67f47d2..9eccab8 100644
.B FRAMAC_SHARE
variable)
.TP
-diff --git a/src/kernel_internals/typing/asm_contracts.ml
b/src/kernel_internals/typing/asm_contracts.ml
-index 3496d74..c30fa22 100644
---- a/src/kernel_internals/typing/asm_contracts.ml
-+++ b/src/kernel_internals/typing/asm_contracts.ml
-@@ -91,7 +91,7 @@ object(self)
- (* the only interesting information for clobbers is the
- presence of the "memory" keyword, which indicates that
- memory may have been accessed (read or write) outside of
-- the locations explicitely referred to as output or
-+ the locations explicitly referred to as output or
- input. We can't do much more than emitting a warning and
- considering that nothing is touched beyond normally
- specified outputs and inputs. *)
-diff --git a/src/kernel_services/abstract_interp/lmap_sig.mli
b/src/kernel_services/abstract_interp/lmap_sig.mli
-index 5e5aff3..ce2d244 100644
---- a/src/kernel_services/abstract_interp/lmap_sig.mli
-+++ b/src/kernel_services/abstract_interp/lmap_sig.mli
-@@ -103,7 +103,7 @@ val find_base : Base.t -> t -> offsetmap
Bottom.Top.or_top_bottom
- val find_base_or_default : Base.t -> t -> offsetmap Bottom.Top.or_top_bottom
- (** Same as [find_base], but return the default values for bases
- that are not currently present in the map. Prefer the use of this function
-- to [find_base], unless you explicitely want to see if the base is bound.
*)
-+ to [find_base], unless you explicitly want to see if the base is bound. *)
-
-
- (** {2 Binding variables} *)
-diff --git a/src/kernel_services/analysis/exn_flow.ml
b/src/kernel_services/analysis/exn_flow.ml
-index 7f10d0a..a32c483 100644
---- a/src/kernel_services/analysis/exn_flow.ml
-+++ b/src/kernel_services/analysis/exn_flow.ml
-@@ -638,7 +638,7 @@ object(self)
-
- method private guard_post_cond (kind,pred as orig) =
- match kind with
-- (* If we exit explicitely with exit,
-+ (* If we exit explicitly with exit,
- we haven't seen an uncaught exception anyway. *)
- | Exits | Breaks | Continues -> orig
- | Returns | Normal ->
-diff --git a/src/kernel_services/analysis/logic_interp.ml
b/src/kernel_services/analysis/logic_interp.ml
-index ec565ce..fff7627 100644
---- a/src/kernel_services/analysis/logic_interp.ml
-+++ b/src/kernel_services/analysis/logic_interp.ml
-@@ -635,7 +635,7 @@ struct
- match ki_opt,before_opt with
- (* function contract *)
- | None,Some true ->
-- failwith "The use of the label Old is forbiden inside clauses \
-+ failwith "The use of the label Old is forbidden inside clauses \
- related the pre-state of function contracts."
- | None,None
- | None,Some false ->
-@@ -643,7 +643,7 @@ struct
- self#change_label AbsLabel_pre x
- (* statement contract *)
- | Some (_ki,false),Some true ->
-- failwith "The use of the label Old is forbiden inside clauses \
-+ failwith "The use of the label Old is forbidden inside clauses \
- related the pre-state of statement contracts."
- | Some (ki,false),None
- | Some (ki,false),Some false ->
-@@ -662,20 +662,20 @@ related the pre-state of statement contracts."
- (* function contract *)
- | None,Some _ ->
- failwith "Function contract where the use of the label Post is \
-- forbiden."
-+ forbidden."
- | None,None ->
- (* refers to the post-state of the contract. *)
- self#change_label AbsLabel_post x
- (* statement contract *)
- | Some (_ki,false),Some _ ->
- failwith "Statement contract where the use of the label Post is \
--forbiden."
-+forbidden."
- | Some (_ki,false),None ->
- (* refers to the pre-state of the contract. *)
- self#change_label AbsLabel_post x
- (* code annotation *)
- | Some (_ki,true), _ ->
-- failwith "The use of the label Post is forbiden inside code \
-+ failwith "The use of the label Post is forbidden inside code \
- annotations."
-
- method private change_label_to_pre: 'a.'a -> 'a visitAction =
-@@ -683,7 +683,7 @@ annotations."
- match ki_opt with
- (* function contract *)
- | None ->
-- failwith "The use of the label Pre is forbiden inside function \
-+ failwith "The use of the label Pre is forbidden inside function \
- contracts."
- (* statement contract *)
- (* code annotation *)
-@@ -696,7 +696,7 @@ contracts."
- match ki_opt with
- (* function contract *)
- | None ->
-- failwith "the use of C labels is forbiden inside clauses related \
-+ failwith "the use of C labels is forbidden inside clauses related \
- function contracts."
- (* statement contract *)
- (* code annotation *)
-diff --git a/src/kernel_services/ast_queries/file.ml
b/src/kernel_services/ast_queries/file.ml
-index af53fad..e5a3a7c 100644
---- a/src/kernel_services/ast_queries/file.ml
-+++ b/src/kernel_services/ast_queries/file.ml
-@@ -413,7 +413,7 @@ let parse_cabs = function
- "your preprocessor is not known to handle option `%s'. \
- If pre-processing fails because of it, please add \
- -no-cpp-gnu-like option to Frama-C's command-line. \
-- If you do not want to see this warning again, use
explicitely \
-+ If you do not want to see this warning again, use explicitly
\
- -cpp-gnu-like option."
- opt;
- opt
-diff --git a/src/kernel_services/ast_queries/logic_const.mli
b/src/kernel_services/ast_queries/logic_const.mli
-index 72d8f3e..64604fd 100644
---- a/src/kernel_services/ast_queries/logic_const.mli
-+++ b/src/kernel_services/ast_queries/logic_const.mli
-@@ -22,7 +22,7 @@
- (* *)
- (**************************************************************************)
-
--(** Smart contructors for logic annotations.
-+(** Smart constructors for logic annotations.
- @plugin development guide *)
-
- open Cil_types
-diff --git a/src/kernel_services/ast_queries/logic_env.ml
b/src/kernel_services/ast_queries/logic_env.ml
-index 6475cf4..8750429 100644
---- a/src/kernel_services/ast_queries/logic_env.ml
-+++ b/src/kernel_services/ast_queries/logic_env.ml
-@@ -92,7 +92,7 @@ module Logic_ctor_builtin =
- (Datatype.String.Hashtbl)
- (Cil_datatype.Logic_ctor_info)
- (struct
-- let name = "built-in logic contructors table"
-+ let name = "built-in logic constructors table"
- let dependencies = []
- let size = 17
- end)
-@@ -102,7 +102,7 @@ module Logic_ctor_info =
- (Datatype.String.Hashtbl)
- (Cil_datatype.Logic_ctor_info)
- (struct
-- let name = "logic contructors table"
-+ let name = "logic constructors table"
- let dependencies = [ Logic_ctor_builtin.self ]
- let size = 17
- end)
-diff --git a/src/kernel_services/ast_queries/logic_typing.ml
b/src/kernel_services/ast_queries/logic_typing.ml
-index 9694a9f..e20b73c 100644
---- a/src/kernel_services/ast_queries/logic_typing.ml
-+++ b/src/kernel_services/ast_queries/logic_typing.ml
-@@ -2090,7 +2090,7 @@ let add_label info lab =
- res
- | _ -> ind
- (* We do not have a context allowing to update the predicate.
-- Implies that any recursive call is already explicitely guarded
-+ Implies that any recursive call is already explicitly guarded
- *)
-
- method! vlogic_info_decl info =
-diff --git a/src/kernel_services/plugin_entry_points/kernel.ml
b/src/kernel_services/plugin_entry_points/kernel.ml
-index 0112fac..83d7dd6 100644
---- a/src/kernel_services/plugin_entry_points/kernel.ml
-+++ b/src/kernel_services/plugin_entry_points/kernel.ml
-@@ -1068,7 +1068,7 @@ module UnspecifiedAccess =
- False(struct
- let module_name = "UnspecifiedAccess"
- let option_name = "-unspecified-access"
-- let help = "do not assume that read/write accesses occuring \
-+ let help = "do not assume that read/write accesses occurring \
- between sequence points are separated"
- end)
-
-diff --git a/src/libraries/utils/bitvector.ml
b/src/libraries/utils/bitvector.ml
-index b2d786b..3ebf43d 100644
---- a/src/libraries/utils/bitvector.ml
-+++ b/src/libraries/utils/bitvector.ml
-@@ -34,7 +34,7 @@
- bitvector, which has to be provided in some informations (such as
- concat). We rely on the invariant that the extra bits are set to
- 0 (this is important e.g. for equality testing). An alternative
-- design could have been not to explicitely ignore these extra bits
-+ design could have been not to explicitly ignore these extra bits
- in operations that are sensitive to them, but this seems more
- error-prone. *)
-
-diff --git a/src/plugins/aorai/aorai_utils.ml
b/src/plugins/aorai/aorai_utils.ml
-index b9df7f2..778f9cc 100644
---- a/src/plugins/aorai/aorai_utils.ml
-+++ b/src/plugins/aorai/aorai_utils.ml
-@@ -736,7 +736,7 @@ let is_out_of_state_pred state =
-
- (* In the deterministic case, we only assign the unique state variable
- to a specific enumerated constant. Non-determistic automata on the other
-- hand, need to have the corresponding state variable explicitely set to 0.
*)
-+ hand, need to have the corresponding state variable explicitly set to 0. *)
- let is_out_of_state_stmt (_,copy) loc =
- if Aorai_option.Deterministic.get ()
- then
-diff --git a/src/plugins/occurrence/register.ml
b/src/plugins/occurrence/register.ml
-index 9318acb..51ca7df 100644
---- a/src/plugins/occurrence/register.ml
-+++ b/src/plugins/occurrence/register.ml
-@@ -216,7 +216,7 @@ let print_one fmt v l =
- | (Some kf, _, _) :: _ -> Kernel_function.get_name kf
- | (None,Kstmt _,_)::_ -> assert false
- | (None,Kglobal,_)::_ ->
-- fatal "inconsistent context for occurence of variable %s"
v.vname
-+ fatal "inconsistent context for occurrence of variable %s"
v.vname
- in
- if v.vformal then "parameter of " ^ kf_name
- else "local of " ^ kf_name);
-diff --git a/src/plugins/scope/dpds_gui.ml b/src/plugins/scope/dpds_gui.ml
-index b0052bb..019566d 100644
---- a/src/plugins/scope/dpds_gui.ml
-+++ b/src/plugins/scope/dpds_gui.ml
-@@ -379,7 +379,7 @@ let help (main_ui:Design.main_window_extension_points) =
- ^"and the data is the one that is selected if any, "
- ^"or it can be given via a popup.\n"
- ^"\tIf the text given in the popup is empty, or 'Cancel' is chosen, "
-- ^"the selection of the command is reseted.");
-+ ^"the selection of the command is reset.");
- add (ShowDef.help);
- add (Zones.help);
- add (DataScope.help);
-diff --git a/src/plugins/security_slicing/security_slicing_parameters.ml
b/src/plugins/security_slicing/security_slicing_parameters.ml
-index 6a7e58c..7b40173 100644
---- a/src/plugins/security_slicing/security_slicing_parameters.ml
-+++ b/src/plugins/security_slicing/security_slicing_parameters.ml
-@@ -31,7 +31,7 @@ module Slicing =
- False
- (struct
- let option_name = "-security-slicing"
-- let help = "perfom the security slicing analysis"
-+ let help = "perform the security slicing analysis"
- end)
-
- (*
-diff --git a/src/plugins/slicing/fct_slice.ml
b/src/plugins/slicing/fct_slice.ml
-index 7416760..8631141 100644
---- a/src/plugins/slicing/fct_slice.ml
-+++ b/src/plugins/slicing/fct_slice.ml
-@@ -1035,7 +1035,7 @@ let choose_precise_slice fi_to_call call_info =
- if more_outputs
- then (* not enough outputs in [ff] *)
- begin
-- SlicingParameters.debug ~level:2
"[Fct_Slice.choose_precise_slice] %s ? not enought outputs"
-+ SlicingParameters.debug ~level:2
"[Fct_Slice.choose_precise_slice] %s ? not enough outputs"
- (SlicingMacros.ff_name ff);
- find slices
- end
-@@ -1258,7 +1258,7 @@ let apply_missing_outputs proj ff call output_marks
more_outputs =
- (** check if [f_to_call] is ok for this call, and if so,
- * change the function call and propagate missing marks in the inputs
- * if needed.
--* @raise ChangeCallErr if [f_to_call] doesn't compute enought outputs.
-+* @raise ChangeCallErr if [f_to_call] doesn't compute enough outputs.
- *)
- let apply_change_call proj ff call f_to_call =
- SlicingParameters.debug ~level:1 "[Fct_Slice.apply_change_call]";
-diff --git a/src/plugins/value/gui_files/register_gui.ml
b/src/plugins/value/gui_files/register_gui.ml
-index 7d1e2c9..f45ff94 100644
---- a/src/plugins/value/gui_files/register_gui.ml
-+++ b/src/plugins/value/gui_files/register_gui.ml
-@@ -794,7 +794,7 @@ module Callstacks_manager = struct
- statement" ()
- in
- let chk_consolidated = new Widget.checkbox ~label:"Consolidated value"
-- ~tooltip:"Show values consolidated accross all callstacks" ()
-+ ~tooltip:"Show values consolidated across all callstacks" ()
- in
- let chk_callstacks = new Widget.checkbox ~label:"Per callstack"
- ~tooltip:"Show values per callstack" ()
-diff --git a/src/plugins/value/value_parameters.ml
b/src/plugins/value/value_parameters.ml
-index 3dc6b8f..beb79cd 100644
---- a/src/plugins/value/value_parameters.ml
-+++ b/src/plugins/value/value_parameters.ml
-@@ -441,7 +441,7 @@ module WarnCopyIndeterminate =
- let option_name = "-val-warn-copy-indeterminate"
- let arg_name = "f | @all"
- let help = "warn when a statement of the specified functions copies a \
--value that may be indeterminate (uninitalized or containing escaping
address). \
-+value that may be indeterminate (uninitialized or containing escaping
address). \
- Set by default; can be deactivated for function 'f' by '=-f', or for all \
- functions by '=-@all'."
- end)
-diff --git a/src/plugins/value_types/cvalue.ml
b/src/plugins/value_types/cvalue.ml
-index 947a05b..b743720 100644
---- a/src/plugins/value_types/cvalue.ml
-+++ b/src/plugins/value_types/cvalue.ml
-@@ -1072,7 +1072,7 @@ module Default_offsetmap = struct
- let default_contents = Lmap.Bottom
- (* this works because, currently:
- - during the analysis, we merge maps with the same variables (all locals
-- are explicitely present)
-+ are explicitly present)
- - after the analysis, for synthetic results, we merge maps with different
- sets of locals, but is is ok to have missing ones considered as being
- bound to Bottom.
-diff --git a/src/plugins/wp/VC.mli b/src/plugins/wp/VC.mli
-index 0f90d67..75de324 100644
---- a/src/plugins/wp/VC.mli
-+++ b/src/plugins/wp/VC.mli
-@@ -43,7 +43,7 @@ val get_formula: t -> Lang.F.pred
-
- (** {2 Database}
- Notice that a property or a function have no proof obligation until you
-- explicitely generate them {i via} the [generate_xxx] functions below.
-+ explicitly generate them {i via} the [generate_xxx] functions below.
- *)
-
- val clear : unit -> unit
-diff --git a/src/plugins/wp/qed/src/logic.mli
b/src/plugins/wp/qed/src/logic.mli
-index dc316d0..54c3437 100644
---- a/src/plugins/wp/qed/src/logic.mli
-+++ b/src/plugins/wp/qed/src/logic.mli
-@@ -423,7 +423,7 @@ sig
- (** Mark a term to be printed *)
- val mark : marks -> term -> unit
-
-- (** Mark a term to be explicitely shared *)
-+ (** Mark a term to be explicitly shared *)
- val share : marks -> term -> unit
-
- (** Returns a list of terms to be shared among all {i shared} or {i
-diff --git a/src/plugins/wp/wpAnnot.ml b/src/plugins/wp/wpAnnot.ml
-index d1d0952..cea0dd8 100644
---- a/src/plugins/wp/wpAnnot.ml
-+++ b/src/plugins/wp/wpAnnot.ml
-@@ -1274,7 +1274,7 @@ let build_configs assigns kf model behaviors ki property
=
- | None -> ()
- | Some Kglobal ->
- debug
-- "[get_strategies] select in function properies@."
-+ "[get_strategies] select in function properties@."
- | Some (Kstmt s) ->
- debug
- "[get_strategies] select stmt %d properties@." s.sid
-diff --git a/src/plugins/wp/wp_parameters.ml b/src/plugins/wp/wp_parameters.ml
-index 9ad708a..861dbda 100644
---- a/src/plugins/wp/wp_parameters.ml
-+++ b/src/plugins/wp/wp_parameters.ml
-@@ -372,7 +372,7 @@ let () = Parameter_customize.set_group wp_simplifier
- module BoundForallUnfolding =
- Int(struct
- let option_name = "-wp-bound-forall-unfolding"
-- let help = "Instanciate up to <n> forall-integers hypotheses."
-+ let help = "Instantiate up to <n> forall-integers hypotheses."
- let arg_name="n"
- let default = 1000
- end)
+diff --git a/src/kernel_services/ast_data/cil_types.mli
b/src/kernel_services/ast_data/cil_types.mli
+index c23460a..1c78913 100644
+--- a/src/kernel_services/ast_data/cil_types.mli
++++ b/src/kernel_services/ast_data/cil_types.mli
+@@ -543,7 +543,7 @@ and varinfo = {
+ (**
+ - For global variables, true iff the variable or function
+ is defined in the file.
+- - For local variables, true iff the variable is explicitely initialized
++ - For local variables, true iff the variable is explicitly initialized
+ at declaration time.
+ - Unused for formals variables and logic variables.
+ *)
+diff --git a/src/plugins/e-acsl/typing.ml b/src/plugins/e-acsl/typing.ml
+index 9f9130f..7d7fb03 100644
+--- a/src/plugins/e-acsl/typing.ml
++++ b/src/plugins/e-acsl/typing.ml
+@@ -203,7 +203,7 @@ let coerce ~arith_operand ~ctx ~op ty =
+ end else
+ (* only add an explicit cast if the context is [Gmp] and [ty] is not;
+ or if the term corresponding to [ty] is an operand of an arithmetic
+- operation which must be explicitely coerced in order to force the
++ operation which must be explicitly coerced in order to force the
+ operation to be of the expected type. *)
+ if (ctx = Gmp && ty <> Gmp) || arith_operand
+ then { ty; op; cast = Some ctx }
+@@ -329,7 +329,7 @@ let rec type_term ~use_gmp_opt ?(arith_operand=false) ?ctx
t =
+ with Interval.Not_an_integer ->
+ dup Other (* real *)
+ in
+- (* it is enough to explicitely coerce when required one operand to [ctx]
++ (* it is enough to explicitly coerce when required one operand to [ctx]
+ (through [arith_operand]) in order to force the type of the
operation.
+ Heuristic: coerce the operand which is not a lval in order to lower
+ the number of explicit casts *)
diff --git a/debian/patches/0002-Use-bin-cp-instead-of-usr-bin-install.patch
b/debian/patches/0002-Use-bin-cp-instead-of-usr-bin-install.patch
index 0f57547..8e86159 100644
--- a/debian/patches/0002-Use-bin-cp-instead-of-usr-bin-install.patch
+++ b/debian/patches/0002-Use-bin-cp-instead-of-usr-bin-install.patch
@@ -7,10 +7,10 @@ Subject: Use /bin/cp instead of /usr/bin/install
1 file changed, 1 insertion(+), 1 deletion(-)
diff --git a/share/Makefile.common b/share/Makefile.common
-index 4c88e5c..0d9c74a 100644
+index e768789..bb9f1db 100644
--- a/share/Makefile.common
+++ b/share/Makefile.common
-@@ -133,7 +133,7 @@ CHMOD_RW= sh -c \
+@@ -164,7 +164,7 @@ CHMOD_RW= sh -c \
'for f in "$$@"; do \
if test -e $$f; then chmod u+w $$f; fi \
done' chmod_rw
diff --git a/debian/patches/0003-Disable-CHMOD_RO-invocations.patch
b/debian/patches/0003-Disable-CHMOD_RO-invocations.patch
index b5086f4..3f6f6ec 100644
--- a/debian/patches/0003-Disable-CHMOD_RO-invocations.patch
+++ b/debian/patches/0003-Disable-CHMOD_RO-invocations.patch
@@ -7,10 +7,10 @@ Subject: Disable CHMOD_RO invocations
1 file changed, 1 insertion(+), 1 deletion(-)
diff --git a/share/Makefile.common b/share/Makefile.common
-index 0d9c74a..7d36c93 100644
+index bb9f1db..919fdc9 100644
--- a/share/Makefile.common
+++ b/share/Makefile.common
-@@ -128,7 +128,7 @@ endif
+@@ -159,7 +159,7 @@ endif
CAT = cat
CHMOD = chmod
diff --git
a/debian/patches/0004-Use-ocamlfind-package-lablgtk2-gnome.gnomecanvas.patch
b/debian/patches/0004-Use-ocamlfind-package-lablgtk2-gnome.gnomecanvas.patch
index 988c934..fef3132 100644
--- a/debian/patches/0004-Use-ocamlfind-package-lablgtk2-gnome.gnomecanvas.patch
+++ b/debian/patches/0004-Use-ocamlfind-package-lablgtk2-gnome.gnomecanvas.patch
@@ -7,10 +7,10 @@ Subject: Use ocamlfind package lablgtk2-gnome.gnomecanvas
1 file changed, 1 insertion(+), 1 deletion(-)
diff --git a/share/Makefile.config.in b/share/Makefile.config.in
-index e254ddc..8068024 100644
+index 31a8a9b..353a60b 100644
--- a/share/Makefile.config.in
+++ b/share/Makefile.config.in
-@@ -178,7 +178,7 @@ LIBRARY_NAMES += zarith
+@@ -176,7 +176,7 @@ LIBRARY_NAMES += landmarks landmarks.ppx
endif
ifneq ($(ENABLE_GUI),no)
diff --git a/debian/patches/0005-Value.cmo-needs-LoopAnalysis.cmo.patch
b/debian/patches/0005-Value.cmo-needs-LoopAnalysis.cmo.patch
index 2c200ea..99b0493 100644
--- a/debian/patches/0005-Value.cmo-needs-LoopAnalysis.cmo.patch
+++ b/debian/patches/0005-Value.cmo-needs-LoopAnalysis.cmo.patch
@@ -10,10 +10,10 @@ PLUGIN_CMO_LIST variable.
1 file changed, 4 insertions(+)
diff --git a/Makefile b/Makefile
-index abbc893..e844de3 100644
+index 0d83496..1fdf715 100644
--- a/Makefile
+++ b/Makefile
-@@ -1095,6 +1095,10 @@ $(foreach p,$(EXTERNAL_PLUGINS),$(eval $(call
INCLUDE_PLUGIN,$p)))
+@@ -1027,6 +1027,10 @@ $(foreach p,$(EXTERNAL_PLUGINS),$(eval $(call
INCLUDE_PLUGIN,$p)))
CMX = $(CMO:.cmo=.cmx)
CMI = $(CMO:.cmo=.cmi)
diff --git a/debian/patches/0006-gui.byte-needs-TARGETS_GUI_BYTE-only.patch
b/debian/patches/0006-gui.byte-needs-TARGETS_GUI_BYTE-only.patch
index c8b5a85..8e7fa8f 100644
--- a/debian/patches/0006-gui.byte-needs-TARGETS_GUI_BYTE-only.patch
+++ b/debian/patches/0006-gui.byte-needs-TARGETS_GUI_BYTE-only.patch
@@ -7,10 +7,10 @@ Subject: gui.byte needs TARGETS_GUI_BYTE only
1 file changed, 6 insertions(+), 2 deletions(-)
diff --git a/share/Makefile.dynamic b/share/Makefile.dynamic
-index 9655220..0b60162 100644
+index fbdd26a..ac4ee23 100644
--- a/share/Makefile.dynamic
+++ b/share/Makefile.dynamic
-@@ -197,8 +197,8 @@ $(eval $(call
include_generic_plugin_Makefile,$(PLUGIN_NAME)))
+@@ -188,14 +188,18 @@ $(eval $(call
include_generic_plugin_Makefile,$(PLUGIN_NAME)))
TARGETS := $(TARGET_META) $(TARGET_CMI)
TARGETS_TOP := $(TARGET_TOP_CMO) $(TARGET_TOP_CMX) \
$(TARGET_TOP_CMA) $(TARGET_TOP_CMXS)
@@ -21,8 +21,6 @@ index 9655220..0b60162 100644
TARGETS_BYTE:= $(TARGET_META) $(TARGET_CMI) $(TARGET_TOP_CMO)
$(TARGET_TOP_CMA)
TARGETS_OPT:= $(TARGET_META) $(TARGET_CMI) $(TARGET_TOP_CMX)
$(TARGET_TOP_CMXS)
-@@ -206,7 +206,11 @@ include $(MAKECONFIG_DIR)/Makefile.kernel
-
byte:: $(TARGETS_BYTE)
opt:: $(TARGETS_OPT)
+ifeq ($(OCAMLBEST),byte)
diff --git a/debian/patches/0007-Fix-FTBFS-with-OCaml-4.05.0.patch
b/debian/patches/0007-Fix-FTBFS-with-OCaml-4.05.0.patch
index 62792b3..777daf1 100644
--- a/debian/patches/0007-Fix-FTBFS-with-OCaml-4.05.0.patch
+++ b/debian/patches/0007-Fix-FTBFS-with-OCaml-4.05.0.patch
@@ -6,12 +6,11 @@ Subject: Fix FTBFS with OCaml 4.05.0
src/kernel_services/analysis/dataflow.ml | 2 +-
src/kernel_services/analysis/dataflow2.ml | 2 +-
src/libraries/project/state_builder.ml | 1 +
- src/libraries/utils/hook.ml | 4 ++--
src/plugins/wp/qed/src/idxset.ml | 2 +-
- 5 files changed, 6 insertions(+), 5 deletions(-)
+ 4 files changed, 4 insertions(+), 3 deletions(-)
diff --git a/src/kernel_services/analysis/dataflow.ml
b/src/kernel_services/analysis/dataflow.ml
-index 0f32f24..137dd2c 100644
+index 516cd3f..9c5deb6 100644
--- a/src/kernel_services/analysis/dataflow.ml
+++ b/src/kernel_services/analysis/dataflow.ml
@@ -80,7 +80,7 @@ module type StmtStartData = sig
@@ -22,9 +21,9 @@ index 0f32f24..137dd2c 100644
+module StartData(X: sig type t val size: int end) : StmtStartData with type
data = X.t = struct
type data = X.t
open Cil_datatype.Stmt.Hashtbl
- let stmtStartData = create X.size
+ let stmtStartData: data Cil_datatype.Stmt.Hashtbl.t = create X.size
diff --git a/src/kernel_services/analysis/dataflow2.ml
b/src/kernel_services/analysis/dataflow2.ml
-index 0d6eb24..55c108e 100644
+index f56ee4e..c3db409 100644
--- a/src/kernel_services/analysis/dataflow2.ml
+++ b/src/kernel_services/analysis/dataflow2.ml
@@ -57,7 +57,7 @@ module type StmtStartData = sig
@@ -35,12 +34,12 @@ index 0d6eb24..55c108e 100644
+module StartData(X: sig type t val size: int end) : StmtStartData with type
data = X.t = struct
type data = X.t
open Cil_datatype.Stmt.Hashtbl
- let stmtStartData = create X.size
+ let stmtStartData: data Cil_datatype.Stmt.Hashtbl.t = create X.size
diff --git a/src/libraries/project/state_builder.ml
b/src/libraries/project/state_builder.ml
-index 8d07c0d..2f65b81 100644
+index c9cb0db..abbd28a 100644
--- a/src/libraries/project/state_builder.ml
+++ b/src/libraries/project/state_builder.ml
-@@ -746,6 +746,7 @@ struct
+@@ -763,6 +763,7 @@ struct
let mem = HW.mem
let find_all = HW.find_all
let find = HW.find
@@ -48,30 +47,8 @@ index 8d07c0d..2f65b81 100644
let remove = HW.remove
let add h v = HW.replace h v v
-diff --git a/src/libraries/utils/hook.ml b/src/libraries/utils/hook.ml
-index 7c4e762..7db08ae 100644
---- a/src/libraries/utils/hook.ml
-+++ b/src/libraries/utils/hook.ml
-@@ -54,7 +54,7 @@ let add_once v queue =
- let already = Queue.fold (fun b v' -> b || v' == v) false queue in
- if not already then Queue.add v queue
-
--module Build(P:sig type t end) = struct
-+module Build(P:sig type t end) : Iter_hook with type param = P.t = struct
- type param = P.t
- type result = unit
- let hooks = Queue.create ()
-@@ -74,7 +74,7 @@ module Build(P:sig type t end) = struct
- let length () = Queue.length hooks
- end
-
--module Fold(P:sig type t end) = struct
-+module Fold(P:sig type t end) : S with type param = P.t and type result = P.t
= struct
- type param = P.t
- type result = P.t
- let hooks = Queue.create ()
diff --git a/src/plugins/wp/qed/src/idxset.ml
b/src/plugins/wp/qed/src/idxset.ml
-index 941384b..037d0b4 100644
+index fb9355a..489463c 100644
--- a/src/plugins/wp/qed/src/idxset.ml
+++ b/src/plugins/wp/qed/src/idxset.ml
@@ -56,7 +56,7 @@ sig
--
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
