This is an automated email from the git hooks/post-receive script. mehdi pushed a commit to branch master in repository frama-c.
commit 3ada267ce919b2c0b4a46206f62ed1adf2da563c Author: Mehdi Dogguy <me...@debian.org> Date: Thu Dec 8 00:32:25 2016 +0100 Refresh patches --- debian/changelog | 3 ++ .../0001-Fix-spelling-error-in-binary.patch | 56 +++++++++++----------- ...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 | 22 --------- debian/patches/series | 1 - 6 files changed, 36 insertions(+), 54 deletions(-) diff --git a/debian/changelog b/debian/changelog index 03fb36c..4d3f2d1 100644 --- a/debian/changelog +++ b/debian/changelog @@ -1,6 +1,9 @@ frama-c (20161101+silicon+dfsg-1) UNRELEASED; urgency=medium * New upstream release. + * Refresh patches. + - Drop patch 0004-Don-t-fail-during-the-configure-on-bytecode-architec.patch + (not needed anymore) -- Mehdi Dogguy <me...@debian.org> Thu, 08 Dec 2016 00:24:00 +0100 diff --git a/debian/patches/0001-Fix-spelling-error-in-binary.patch b/debian/patches/0001-Fix-spelling-error-in-binary.patch index 851ebd1..83bec16 100644 --- a/debian/patches/0001-Fix-spelling-error-in-binary.patch +++ b/debian/patches/0001-Fix-spelling-error-in-binary.patch @@ -8,13 +8,13 @@ Subject: Fix spelling-error-in-binary 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_typing.ml | 2 +- src/libraries/utils/bitvector.ml | 2 +- src/plugins/aorai/aorai_utils.ml | 2 +- src/plugins/occurrence/register.ml | 2 +- src/plugins/value_types/cvalue.ml | 2 +- src/plugins/wp/VC.mli | 2 +- src/plugins/wp/qed/src/logic.mli | 2 +- - tests/spec/oracle/preprocess_string.res.oracle | 2 +- 12 files changed, 18 insertions(+), 18 deletions(-) diff --git a/src/kernel_internals/typing/asm_contracts.ml b/src/kernel_internals/typing/asm_contracts.ml @@ -31,11 +31,11 @@ index 3496d74..c30fa22 100644 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 bb69f4d..7775eda 100644 +index 5e5aff3..ce2d244 100644 --- a/src/kernel_services/abstract_interp/lmap_sig.mli +++ b/src/kernel_services/abstract_interp/lmap_sig.mli -@@ -92,7 +92,7 @@ val find_base : Base.t -> t -> offsetmap_top_bottom - val find_base_or_default : Base.t -> t -> offsetmap_top_bottom +@@ -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. *) @@ -44,10 +44,10 @@ index bb69f4d..7775eda 100644 (** {2 Binding variables} *) diff --git a/src/kernel_services/analysis/exn_flow.ml b/src/kernel_services/analysis/exn_flow.ml -index 1aa2562..e232a50 100644 +index 7f10d0a..a32c483 100644 --- a/src/kernel_services/analysis/exn_flow.ml +++ b/src/kernel_services/analysis/exn_flow.ml -@@ -632,7 +632,7 @@ object(self) +@@ -638,7 +638,7 @@ object(self) method private guard_post_cond (kind,pred as orig) = match kind with @@ -57,7 +57,7 @@ index 1aa2562..e232a50 100644 | 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 a130786..11e3cf5 100644 +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 @@ -121,10 +121,10 @@ index a130786..11e3cf5 100644 (* statement contract *) (* code annotation *) diff --git a/src/kernel_services/ast_queries/file.ml b/src/kernel_services/ast_queries/file.ml -index 1ddde67..4a5cdbf 100644 +index af53fad..e5a3a7c 100644 --- a/src/kernel_services/ast_queries/file.ml +++ b/src/kernel_services/ast_queries/file.ml -@@ -411,7 +411,7 @@ let parse_cabs = function +@@ -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. \ @@ -133,8 +133,21 @@ index 1ddde67..4a5cdbf 100644 -cpp-gnu-like option." opt; opt +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/libraries/utils/bitvector.ml b/src/libraries/utils/bitvector.ml -index bbb1915..a1db387 100644 +index b2d786b..3ebf43d 100644 --- a/src/libraries/utils/bitvector.ml +++ b/src/libraries/utils/bitvector.ml @@ -34,7 +34,7 @@ @@ -147,7 +160,7 @@ index bbb1915..a1db387 100644 error-prone. *) diff --git a/src/plugins/aorai/aorai_utils.ml b/src/plugins/aorai/aorai_utils.ml -index cfd69c8..691bda1 100644 +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 = @@ -173,11 +186,11 @@ index 9318acb..51ca7df 100644 if v.vformal then "parameter of " ^ kf_name else "local of " ^ kf_name); diff --git a/src/plugins/value_types/cvalue.ml b/src/plugins/value_types/cvalue.ml -index 767da7a..bf43c94 100644 +index 947a05b..b743720 100644 --- a/src/plugins/value_types/cvalue.ml +++ b/src/plugins/value_types/cvalue.ml -@@ -1058,7 +1058,7 @@ module Default_offsetmap = struct - let default_contents = `Bottom +@@ -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) @@ -199,10 +212,10 @@ index 0f90d67..75de324 100644 val clear : unit -> unit diff --git a/src/plugins/wp/qed/src/logic.mli b/src/plugins/wp/qed/src/logic.mli -index 3980084..c6cce64 100644 +index dc316d0..54c3437 100644 --- a/src/plugins/wp/qed/src/logic.mli +++ b/src/plugins/wp/qed/src/logic.mli -@@ -421,7 +421,7 @@ sig +@@ -423,7 +423,7 @@ sig (** Mark a term to be printed *) val mark : marks -> term -> unit @@ -211,15 +224,4 @@ index 3980084..c6cce64 100644 val share : marks -> term -> unit (** Returns a list of terms to be shared among all {i shared} or {i -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) ≡ '/'; */ -- 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 6732838..a18fd5a 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 fcce208..fcc3006 100644 +index 4c88e5c..0d9c74a 100644 --- a/share/Makefile.common +++ b/share/Makefile.common -@@ -134,7 +134,7 @@ CHMOD_RW= sh -c \ +@@ -133,7 +133,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 863d429..6b339f0 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 fcc3006..0459380 100644 +index 0d9c74a..7d36c93 100644 --- a/share/Makefile.common +++ b/share/Makefile.common -@@ -129,7 +129,7 @@ endif +@@ -128,7 +128,7 @@ endif 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 deleted file mode 100644 index c3366c3..0000000 --- a/debian/patches/0004-Don-t-fail-during-the-configure-on-bytecode-architec.patch +++ /dev/null @@ -1,22 +0,0 @@ -From: Mehdi Dogguy <me...@debian.org> -Date: Mon, 31 Aug 2015 13:20:47 +0000 -Subject: Don't fail during the configure on bytecode architectures - ---- - configure.in | 2 +- - 1 file changed, 1 insertion(+), 1 deletion(-) - -diff --git a/configure.in b/configure.in -index fdc28a5..54a07b2 100644 ---- a/configure.in -+++ b/configure.in -@@ -353,7 +353,7 @@ if test "$ENABLE_LOCAL_OCAMLGRAPH" != "yes"; then - ocamlgraph_error - fi - else -- ocamlgraph_error -+ echo "Upstream .oO(I'm too lazy to write a test for the pure bytecode case)" - fi - fi - else --- diff --git a/debian/patches/series b/debian/patches/series index 16f228a..06464b6 100644 --- a/debian/patches/series +++ b/debian/patches/series @@ -1,4 +1,3 @@ 0001-Fix-spelling-error-in-binary.patch 0002-Use-bin-cp-instead-of-usr-bin-install.patch 0003-Disable-CHMOD_RO-invocations.patch -0004-Don-t-fail-during-the-configure-on-bytecode-architec.patch -- 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