[Pkg-ocaml-maint-commits] [frama-c] 08/20: Refresh patches
Mehdi Dogguy
mehdi at moszumanska.debian.org
Wed Dec 21 10:15:20 UTC 2016
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 <mehdi at 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 <mehdi at 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 <mehdi at 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
More information about the Pkg-ocaml-maint-commits
mailing list