This is an automated email from the git hooks/post-receive script.
mehdi pushed a commit to branch master
in repository frama-c.
commit 7f7d77f3d5b53eb4d81511d62c739f20d39433ee
Author: Mehdi Dogguy <me...@debian.org>
Date: Thu Jan 21 23:14:19 2016 +0100
Refresh patches
---
debian/changelog | 1 +
.../0001-Fix-spelling-error-in-binary.patch | 257 ++++++++-------------
...002-Use-bin-cp-instead-of-usr-bin-install.patch | 4 +-
.../0003-Disable-CHMOD_RO-invocations.patch | 4 +-
...during-the-configure-on-bytecode-architec.patch | 4 +-
5 files changed, 106 insertions(+), 164 deletions(-)
diff --git a/debian/changelog b/debian/changelog
index b5dece2..570e544 100644
--- a/debian/changelog
+++ b/debian/changelog
@@ -1,6 +1,7 @@
frama-c (20151002+magnesium+dfsg-1) UNRELEASED; urgency=medium
* New upstream release
+ - Refresh patches.
- Add ocaml-findlib and libfindlib-ocaml-dev to Build-Depends
since they became a hard requirement.
* Fix variable FRAMA_GUI_LIBS in debian/rules: "gui" directory
diff --git a/debian/patches/0001-Fix-spelling-error-in-binary.patch
b/debian/patches/0001-Fix-spelling-error-in-binary.patch
index 8782b83..7eae1f0 100644
--- a/debian/patches/0001-Fix-spelling-error-in-binary.patch
+++ b/debian/patches/0001-Fix-spelling-error-in-binary.patch
@@ -1,105 +1,83 @@
From: Mehdi Dogguy <me...@debian.org>
-Date: Mon, 2 Jan 2012 14:36:52 +0100
+Date: Thu, 21 Jan 2016 23:48:35 +0100
Subject: Fix spelling-error-in-binary
---
- cil/src/frontc/cparser.mly | 2 +-
- cil/src/logic/logic_typing.ml | 2 +-
- cil/src/logic/logic_utils.mli | 2 +-
- src/ai/trace.ml | 2 +-
- src/gui/filetree.ml | 2 +-
- src/kernel/exn_flow.ml | 2 +-
- src/kernel/file.ml | 2 +-
- src/lib/bitvector.ml | 2 +-
- src/memory_state/cvalue.mli | 2 +-
- src/memory_state/lmap_sig.mli | 2 +-
- src/value/eval_annots.ml | 2 +-
- tests/spec/oracle/preprocess_string.res.oracle | 2 +-
- 12 files changed, 12 insertions(+), 12 deletions(-)
+ src/kernel_services/analysis/logic_interp.ml | 14 +++++++-------
+ src/kernel_services/ast_queries/file.ml | 2 +-
+ src/plugins/occurrence/register.ml | 2 +-
+ src/plugins/wp/wp_parameters.ml | 2 +-
+ 4 files changed, 10 insertions(+), 10 deletions(-)
-diff --git a/cil/src/frontc/cparser.mly b/cil/src/frontc/cparser.mly
-index 784db05..9d75dde 100644
---- a/cil/src/frontc/cparser.mly
-+++ b/cil/src/frontc/cparser.mly
-@@ -614,7 +614,7 @@ unary_expression: /*(* 6.5.3 *)*/
- { make_expr (UNARY (NOT, $2)) }
- | TILDE cast_expression
- { make_expr (UNARY (BNOT, $2)) }
--/* (* GCC allows to take address of a label (see COMPGOTO statement) *) */
-+/* (* GCC allows one to take address of a label (see COMPGOTO statement) *) */
- | AND_AND id_or_typename_as_id { make_expr (LABELADDR $2) }
- ;
+diff --git a/src/kernel_services/analysis/logic_interp.ml
b/src/kernel_services/analysis/logic_interp.ml
+index aa44d65..6ce27ab 100644
+--- a/src/kernel_services/analysis/logic_interp.ml
++++ b/src/kernel_services/analysis/logic_interp.ml
+@@ -637,7 +637,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 ->
+@@ -645,7 +645,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 ->
+@@ -664,20 +664,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."
-diff --git a/cil/src/logic/logic_typing.ml b/cil/src/logic/logic_typing.ml
-index 7a4c2af..75294b0 100644
---- a/cil/src/logic/logic_typing.ml
-+++ b/cil/src/logic/logic_typing.ml
-@@ -447,7 +447,7 @@ let post_state_env kind typ =
- let env = append_init_label env in
- let env = append_here_label env in
- let env = append_old_and_post_labels env in
-- (* NB: this allows to have \result and Exits as termination kind *)
-+ (* NB: this allows one to have \result and Exits as termination kind *)
- let env = add_result env typ in
- let env = add_exit_status env in
- let env = enter_post_state env kind in
-diff --git a/cil/src/logic/logic_utils.mli b/cil/src/logic/logic_utils.mli
-index 0d7bf9e..cb31198 100644
---- a/cil/src/logic/logic_utils.mli
-+++ b/cil/src/logic/logic_utils.mli
-@@ -319,7 +319,7 @@ val merge_funspec :
- val clear_funspec: funspec -> unit
-
- (** {2 Discriminating code_annotations} *)
--(** Functions below allows to test a special kind of code_annotation.
-+(** Functions below allows one to test a special kind of code_annotation.
- Use them in conjunction with {!Annotations.get_filter} to retrieve
- a particular kind of annotations associated to a statement. *)
-
-diff --git a/src/ai/trace.ml b/src/ai/trace.ml
-index 86f609b..fb5e830 100644
---- a/src/ai/trace.ml
-+++ b/src/ai/trace.ml
-@@ -31,7 +31,7 @@ let empty_execution_count = (0,0);;
- (* Nodes in the intra-procedural trace graph. They are identified by
- the stmt that begin them, together with an approximation of the
- number of times the block has been executed. The execution count
-- allows to differentiate multiple executions of the same basic
-+ allows one to differentiate multiple executions of the same basic
- block, which helps maintaining precise traces.
-
- The start of the trace is identified with a special element
-diff --git a/src/gui/filetree.ml b/src/gui/filetree.ml
-index e5c2e78..8f6f4e1 100644
---- a/src/gui/filetree.ml
-+++ b/src/gui/filetree.ml
-@@ -337,7 +337,7 @@ end
-
- module MODEL=MAKE(MYTREE)
-
--(* Primitives to handle the filetree menu (which allows to hide some
-+(* Primitives to handle the filetree menu (which allows one to hide some
- entries) *)
- module MenusHide = struct
- let hide key () = Configuration.find_bool ~default:false key
-diff --git a/src/kernel/exn_flow.ml b/src/kernel/exn_flow.ml
-index 69c639d..f2968ff 100644
---- a/src/kernel/exn_flow.ml
-+++ b/src/kernel/exn_flow.ml
-@@ -632,7 +632,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/file.ml b/src/kernel/file.ml
-index 7970f82..cde0b06 100644
---- a/src/kernel/file.ml
-+++ b/src/kernel/file.ml
-@@ -1104,7 +1104,7 @@ let parse = function
+ method private change_label_to_pre: 'a.'a -> 'a visitAction =
+@@ -685,7 +685,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 *)
+@@ -698,7 +698,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 a021321..5b9daf6 100644
+--- a/src/kernel_services/ast_queries/file.ml
++++ b/src/kernel_services/ast_queries/file.ml
+@@ -396,7 +396,7 @@ let parse = 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. \
@@ -108,66 +86,29 @@ index 7970f82..cde0b06 100644
-cpp-gnu-like option."
opt;
opt
-diff --git a/src/lib/bitvector.ml b/src/lib/bitvector.ml
-index 66bf84f..8f0007e 100644
---- a/src/lib/bitvector.ml
-+++ b/src/lib/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/memory_state/cvalue.mli b/src/memory_state/cvalue.mli
-index d6aa362..170a5c6 100644
---- a/src/memory_state/cvalue.mli
-+++ b/src/memory_state/cvalue.mli
-@@ -237,7 +237,7 @@ module Model: sig
- [loc] in [state]. If [loc] is not writable, {!bottom} is returned.
- The returned boolean indicates that the location may be invalid.
- For this function, [v] is an initialized value; the function
-- {!add_binding_unspecified} allows to write a possibly unspecified
-+ {!add_binding_unspecified} allows one to write a possibly unspecified
- value to [state]. *)
- val add_binding :
- exact:bool -> t -> location -> V.t -> bool * t
-diff --git a/src/memory_state/lmap_sig.mli b/src/memory_state/lmap_sig.mli
-index 972a9e7..b6c6590 100644
---- a/src/memory_state/lmap_sig.mli
-+++ b/src/memory_state/lmap_sig.mli
-@@ -89,7 +89,7 @@ val find_base : Base.t -> t -> offsetmap_top_bottom
- val find_base_or_default : Base.t -> t -> offsetmap_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/value/eval_annots.ml b/src/value/eval_annots.ml
-index c57a00d..0b08287 100644
---- a/src/value/eval_annots.ml
-+++ b/src/value/eval_annots.ml
-@@ -324,7 +324,7 @@ let check_fct_assigns kf ab ~pre_state found_froms =
- let source = fst (asgn.it_content.term_loc) in
- let ip = Property.ip_of_from kf Kglobal bol from in
- (* Note: narrowing the stated assigns (in [assigns_zone])
-- with the ones really found (in [outputs]) allows to
-+ with the ones really found (in [outputs]) allows one to
- have less dependencies. But this is sound only if the
- assigns from express a weak update.
+diff --git a/src/plugins/occurrence/register.ml
b/src/plugins/occurrence/register.ml
+index 13a1289..c175615 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/wp/wp_parameters.ml b/src/plugins/wp/wp_parameters.ml
+index a0a02ae..6c229b7 100644
+--- a/src/plugins/wp/wp_parameters.ml
++++ b/src/plugins/wp/wp_parameters.ml
+@@ -46,7 +46,7 @@ module Log =
+ (struct
+ let option_name = "-wp-log"
+ let arg_name = "..."
+- let help = "Log Specific informations"
++ let help = "Log Specific information"
+ end)
-diff --git a/tests/spec/oracle/preprocess_string.res.oracle
b/tests/spec/oracle/preprocess_string.res.oracle
-index 064fa94..b2ec6eb 100644
---- a/tests/spec/oracle/preprocess_string.res.oracle
-+++ b/tests/spec/oracle/preprocess_string.res.oracle
-@@ -1,5 +1,5 @@
- [kernel] Parsing share/libc/__fc_builtin_for_normalization.i (no
preprocessing)
--[kernel] warning: your preprocessor is not known to handle option `
-nostdinc'. 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 -cpp-gnu-like option.
-+[kernel] warning: your preprocessor is not known to handle option `
-nostdinc'. 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 explicitly -cpp-gnu-like option.
- [kernel] Parsing tests/spec/preprocess_string.c (with preprocessing)
- /* Generated by Frama-C */
- /*@ ensures *("/*"+0) ≡ '/'; */
+ let has_dkey k =
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 a2771e2..a29118c 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 583a23a..8c91ef6 100644
+index 2c27a92..d9fd57c 100644
--- a/share/Makefile.common
+++ b/share/Makefile.common
-@@ -148,7 +148,7 @@ CHMOD_RW= sh -c \
+@@ -156,7 +156,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 f1a0f1f..8a5fd97 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 8c91ef6..f7654a3 100644
+index d9fd57c..5d8cda6 100644
--- a/share/Makefile.common
+++ b/share/Makefile.common
-@@ -143,7 +143,7 @@ external_make = \
+@@ -151,7 +151,7 @@ external_make = \
CAT = cat
CHMOD = chmod
diff --git
a/debian/patches/0004-Don-t-fail-during-the-configure-on-bytecode-architec.patch
b/debian/patches/0004-Don-t-fail-during-the-configure-on-bytecode-architec.patch
index 2043f2e..cfcad29 100644
---
a/debian/patches/0004-Don-t-fail-during-the-configure-on-bytecode-architec.patch
+++
b/debian/patches/0004-Don-t-fail-during-the-configure-on-bytecode-architec.patch
@@ -7,10 +7,10 @@ Subject: Don't fail during the configure on bytecode
architectures
1 file changed, 1 insertion(+), 1 deletion(-)
diff --git a/configure.in b/configure.in
-index 9f5f9d8..164f1bc 100644
+index 6bbed59..8df8ebc 100644
--- a/configure.in
+++ b/configure.in
-@@ -376,7 +376,7 @@ if test "$ENABLE_LOCAL_OCAMLGRAPH" != "yes"; then
+@@ -343,7 +343,7 @@ if test "$ENABLE_LOCAL_OCAMLGRAPH" != "yes"; then
ocamlgraph_error
fi
else
--
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
