This is an automated email from the git hooks/post-receive script.
mehdi pushed a commit to branch master
in repository frama-c.
commit dee89fab5a40e2c272f52be83d074c69cd65008a
Author: Mehdi Dogguy <me...@debian.org>
Date: Thu Dec 8 00:20:39 2016 +0100
Refresh patches
---
.../0001-Fix-spelling-error-in-binary.patch | 163 +++++++++++++++++----
...002-Use-bin-cp-instead-of-usr-bin-install.patch | 11 +-
.../0003-Disable-CHMOD_RO-invocations.patch | 5 +-
...during-the-configure-on-bytecode-architec.patch | 5 +-
4 files changed, 149 insertions(+), 35 deletions(-)
diff --git a/debian/patches/0001-Fix-spelling-error-in-binary.patch
b/debian/patches/0001-Fix-spelling-error-in-binary.patch
index 7eae1f0..851ebd1 100644
--- a/debian/patches/0001-Fix-spelling-error-in-binary.patch
+++ b/debian/patches/0001-Fix-spelling-error-in-binary.patch
@@ -3,17 +3,64 @@ Date: Thu, 21 Jan 2016 23:48:35 +0100
Subject: Fix spelling-error-in-binary
---
- 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(-)
+ 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/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
+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 bb69f4d..7775eda 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
+ (** 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 1aa2562..e232a50 100644
+--- a/src/kernel_services/analysis/exn_flow.ml
++++ b/src/kernel_services/analysis/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_services/analysis/logic_interp.ml
b/src/kernel_services/analysis/logic_interp.ml
-index aa44d65..6ce27ab 100644
+index a130786..11e3cf5 100644
--- a/src/kernel_services/analysis/logic_interp.ml
+++ b/src/kernel_services/analysis/logic_interp.ml
-@@ -637,7 +637,7 @@ struct
+@@ -635,7 +635,7 @@ struct
match ki_opt,before_opt with
(* function contract *)
| None,Some true ->
@@ -22,7 +69,7 @@ index aa44d65..6ce27ab 100644
related the pre-state of function contracts."
| None,None
| None,Some false ->
-@@ -645,7 +645,7 @@ struct
+@@ -643,7 +643,7 @@ struct
self#change_label AbsLabel_pre x
(* statement contract *)
| Some (_ki,false),Some true ->
@@ -31,7 +78,7 @@ index aa44d65..6ce27ab 100644
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."
+@@ -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 \
@@ -55,7 +102,7 @@ index aa44d65..6ce27ab 100644
annotations."
method private change_label_to_pre: 'a.'a -> 'a visitAction =
-@@ -685,7 +685,7 @@ annotations."
+@@ -683,7 +683,7 @@ annotations."
match ki_opt with
(* function contract *)
| None ->
@@ -64,7 +111,7 @@ index aa44d65..6ce27ab 100644
contracts."
(* statement contract *)
(* code annotation *)
-@@ -698,7 +698,7 @@ contracts."
+@@ -696,7 +696,7 @@ contracts."
match ki_opt with
(* function contract *)
| None ->
@@ -74,10 +121,10 @@ index aa44d65..6ce27ab 100644
(* 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
+index 1ddde67..4a5cdbf 100644
--- a/src/kernel_services/ast_queries/file.ml
+++ b/src/kernel_services/ast_queries/file.ml
-@@ -396,7 +396,7 @@ let parse = function
+@@ -411,7 +411,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. \
@@ -86,8 +133,34 @@ index a021321..5b9daf6 100644
-cpp-gnu-like option."
opt;
opt
+diff --git a/src/libraries/utils/bitvector.ml
b/src/libraries/utils/bitvector.ml
+index bbb1915..a1db387 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 cfd69c8..691bda1 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 13a1289..c175615 100644
+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 =
@@ -99,16 +172,54 @@ index 13a1289..c175615 100644
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/src/plugins/value_types/cvalue.ml
b/src/plugins/value_types/cvalue.ml
+index 767da7a..bf43c94 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
+ (* 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 3980084..c6cce64 100644
+--- a/src/plugins/wp/qed/src/logic.mli
++++ b/src/plugins/wp/qed/src/logic.mli
+@@ -421,7 +421,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
- let has_dkey k =
+ (** 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 a29118c..6732838 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,15 +7,16 @@ 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 2c27a92..d9fd57c 100644
+index fcce208..fcc3006 100644
--- a/share/Makefile.common
+++ b/share/Makefile.common
-@@ -156,7 +156,7 @@ CHMOD_RW= sh -c \
+@@ -134,7 +134,7 @@ CHMOD_RW= sh -c \
'for f in "$$@"; do \
if test -e $$f; then chmod u+w $$f; fi \
done' chmod_rw
-CP = install
+CP = cp
- #follow symbolic link
- CP_L = cp -fL
- ECHO = echo
+ CP_IF_DIFF = sh -c \
+ 'if cmp -s $$1 $$2; \
+ then touch -r $$2 $$1; \
+--
diff --git a/debian/patches/0003-Disable-CHMOD_RO-invocations.patch
b/debian/patches/0003-Disable-CHMOD_RO-invocations.patch
index 8a5fd97..863d429 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 d9fd57c..5d8cda6 100644
+index fcc3006..0459380 100644
--- a/share/Makefile.common
+++ b/share/Makefile.common
-@@ -151,7 +151,7 @@ external_make = \
+@@ -129,7 +129,7 @@ endif
CAT = cat
CHMOD = chmod
@@ -19,3 +19,4 @@ index d9fd57c..5d8cda6 100644
CHMOD_RW= sh -c \
'for f in "$$@"; do \
if test -e $$f; then chmod u+w $$f; fi \
+--
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 cfcad29..c3366c3 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 6bbed59..8df8ebc 100644
+index fdc28a5..54a07b2 100644
--- a/configure.in
+++ b/configure.in
-@@ -343,7 +343,7 @@ if test "$ENABLE_LOCAL_OCAMLGRAPH" != "yes"; then
+@@ -353,7 +353,7 @@ if test "$ENABLE_LOCAL_OCAMLGRAPH" != "yes"; then
ocamlgraph_error
fi
else
@@ -19,3 +19,4 @@ index 6bbed59..8df8ebc 100644
fi
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
