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