[Pkg-ocaml-maint-commits] [frama-c] 04/09: Refrech patches.
Mehdi Dogguy
mehdi at moszumanska.debian.org
Mon Aug 31 20:29:29 UTC 2015
This is an automated email from the git hooks/post-receive script.
mehdi pushed a commit to branch master
in repository frama-c.
commit a6109448645dbabaa351c832e8d11e1842ba49de
Author: Mehdi Dogguy <mehdi at debian.org>
Date: Mon Aug 31 13:12:33 2015 +0000
Refrech patches.
---
debian/changelog | 2 +
.../0001-Fix-spelling-error-in-binary.patch | 225 +++++++++++++-----
...002-Use-bin-cp-instead-of-usr-bin-install.patch | 7 +-
.../0003-Disable-CHMOD_RO-invocations.patch | 7 +-
...during-the-configure-on-bytecode-architec.patch | 21 ++
debian/patches/0004-Port-to-OCamlgraph-1.8.5.patch | 254 ---------------------
...during-the-configure-on-bytecode-architec.patch | 22 --
debian/patches/series | 3 +-
8 files changed, 195 insertions(+), 346 deletions(-)
diff --git a/debian/changelog b/debian/changelog
index 8cfab46..d03a1b9 100644
--- a/debian/changelog
+++ b/debian/changelog
@@ -1,6 +1,8 @@
frama-c (20150201+sodium+dfsg-1) UNRELEASED; urgency=medium
* New upstream release (Closes: #797473).
+ - Refrech patches.
+ - Drop 0004-Port-to-OCamlgraph-1.8.5.patch: Integrated upstream.
-- Mehdi Dogguy <mehdi at debian.org> Mon, 31 Aug 2015 12:56:01 +0000
diff --git a/debian/patches/0001-Fix-spelling-error-in-binary.patch b/debian/patches/0001-Fix-spelling-error-in-binary.patch
index a42f6f5..8782b83 100644
--- a/debian/patches/0001-Fix-spelling-error-in-binary.patch
+++ b/debian/patches/0001-Fix-spelling-error-in-binary.patch
@@ -3,66 +3,171 @@ Date: Mon, 2 Jan 2012 14:36:52 +0100
Subject: Fix spelling-error-in-binary
---
- Changelog | 4 ++--
- cil/src/frontc/cabs2cil.ml | 4 ++--
- man/frama-c.1 | 2 +-
- 3 files changed, 5 insertions(+), 5 deletions(-)
+ 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(-)
-diff --git a/Changelog b/Changelog
-index b551baf..849fd3c 100644
---- a/Changelog
-+++ b/Changelog
-@@ -589,7 +589,7 @@ o! Kernel [2012/11/24] Various types whose names started by t_ in
- o Rte [2012/11/23] Export function "exp_annotations" to get RTEs of a C
- expression as annotations.
- o*!Kernel [2012/11/23] Added TLogic_coerce constructor to mark
-- explicitely a conversion from a C type to a logical one
-+ explicitly a conversion from a C type to a logical one
- (in particular floating point -> real and integral -> integer).
- Fixes issue #1309.
- o! Kernel [2012/11/22] Remove unintuitive ?prj argument from Cil visitors,
-@@ -1607,7 +1607,7 @@ o* Cil [2010/12/20] Fixed bug #645. Ast_info.constant_expr,
- mkAddrOrStartOf,mkString,parseInt,sizeOf] no longer use
- an optional argument ?loc. It is now a non optional labeled
- argument. Previous default value of loc was
-- ~loc:Cil_datatype.Location.unkown which is most of the time
-+ ~loc:Cil_datatype.Location.unknown which is most of the time
- not accurate.
+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/cil/src/frontc/cabs2cil.ml b/cil/src/frontc/cabs2cil.ml
-index e803678..2699ae8 100644
---- a/cil/src/frontc/cabs2cil.ml
-+++ b/cil/src/frontc/cabs2cil.ml
-@@ -2318,7 +2318,7 @@ let makeGlobalVarinfo (isadef: bool) (vi: varinfo) : varinfo * bool =
- * local. This can happen when we declare an extern variable with
- * global scope but we are in a local scope. *)
+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
-- (* We lookup in the environement. If this is extern inline then the name
-+ (* We lookup in the environment. If this is extern inline then the name
- * was already changed to foo__extinline. We lookup with the old name *)
- let lookupname =
- if vi.vstorage = Static then
-@@ -3517,7 +3517,7 @@ let default_argument_promotion idx exp =
- "implicit prototype cannot have variadic arguments"
- | TNamed _ -> assert false (* unrollType *)
- in
-- (* if we make a promotion, take it explicitely
-+ (* if we make a promotion, take it explicitly
- into account in the argument itself *)
- let (_,e) = castTo arg_type typ exp in
- (name,typ,[]), e
-diff --git a/man/frama-c.1 b/man/frama-c.1
-index 6e46d24..ae537d7 100644
---- a/man/frama-c.1
-+++ b/man/frama-c.1
-@@ -395,7 +395,7 @@ removes break, continue and switch statement before analyses. Defaults to
- no.
- .TP
- .B -then
--allows to compose analyzes: a first run of Frama-C will occur with the
-+allows one to compose analyzes: a first run of Frama-C will occur with the
- options before
- .B -then
- and a second run will be done with the options after
---
+ (** {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
+ "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. \
+- If you do not want to see this warning again, use explicitely \
++ If you do not want to see this warning again, use explicitly \
+ -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/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 a6bcb1b..a2771e2 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
@@ -3,14 +3,14 @@ Date: Mon, 2 Jan 2012 17:28:56 +0100
Subject: Use /bin/cp instead of /usr/bin/install
---
- share/Makefile.common | 2 +-
+ share/Makefile.common | 2 +-
1 file changed, 1 insertion(+), 1 deletion(-)
diff --git a/share/Makefile.common b/share/Makefile.common
-index 8580d75..f4cc748 100644
+index 583a23a..8c91ef6 100644
--- a/share/Makefile.common
+++ b/share/Makefile.common
-@@ -138,7 +138,7 @@ CHMOD_RW= sh -c \
+@@ -148,7 +148,7 @@ CHMOD_RW= sh -c \
'for f in "$$@"; do \
if test -e $$f; then chmod u+w $$f; fi \
done' chmod_rw
@@ -19,4 +19,3 @@ index 8580d75..f4cc748 100644
#follow symbolic link
CP_L = cp -fL
ECHO = echo
---
diff --git a/debian/patches/0003-Disable-CHMOD_RO-invocations.patch b/debian/patches/0003-Disable-CHMOD_RO-invocations.patch
index fd6c9ce..f1a0f1f 100644
--- a/debian/patches/0003-Disable-CHMOD_RO-invocations.patch
+++ b/debian/patches/0003-Disable-CHMOD_RO-invocations.patch
@@ -3,14 +3,14 @@ Date: Tue, 3 Jan 2012 15:24:27 +0100
Subject: Disable CHMOD_RO invocations
---
- share/Makefile.common | 2 +-
+ share/Makefile.common | 2 +-
1 file changed, 1 insertion(+), 1 deletion(-)
diff --git a/share/Makefile.common b/share/Makefile.common
-index f4cc748..eb169e4 100644
+index 8c91ef6..f7654a3 100644
--- a/share/Makefile.common
+++ b/share/Makefile.common
-@@ -133,7 +133,7 @@ external_make = \
+@@ -143,7 +143,7 @@ external_make = \
CAT = cat
CHMOD = chmod
@@ -19,4 +19,3 @@ index f4cc748..eb169e4 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
new file mode 100644
index 0000000..2043f2e
--- /dev/null
+++ b/debian/patches/0004-Don-t-fail-during-the-configure-on-bytecode-architec.patch
@@ -0,0 +1,21 @@
+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 9f5f9d8..164f1bc 100644
+--- a/configure.in
++++ b/configure.in
+@@ -376,7 +376,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/0004-Port-to-OCamlgraph-1.8.5.patch b/debian/patches/0004-Port-to-OCamlgraph-1.8.5.patch
deleted file mode 100644
index 798d17f..0000000
--- a/debian/patches/0004-Port-to-OCamlgraph-1.8.5.patch
+++ /dev/null
@@ -1,254 +0,0 @@
-From: Mehdi Dogguy <mehdi at debian.org>
-Date: Sun, 27 Apr 2014 13:46:16 +0200
-Subject: Port to OCamlgraph 1.8.5
-
----
- src/impact/reason_graph.ml | 2 +-
- src/kernel/stmts_graph.ml | 10 +++++-----
- src/logic/property_status.ml | 8 ++++----
- src/misc/service_graph.ml | 4 ++--
- src/pdg_types/pdgTypes.ml | 6 +++---
- src/postdominators/print.ml | 2 +-
- src/semantic_callgraph/register.ml | 4 ++--
- src/slicing/printSlice.ml | 10 +++++-----
- src/syntactic_callgraph/register.ml | 4 ++--
- src/wp/cil2cfg.ml | 12 ++++++------
- 10 files changed, 31 insertions(+), 31 deletions(-)
-
-diff --git a/src/impact/reason_graph.ml b/src/impact/reason_graph.ml
-index eabacb0..ce19b4a 100644
---- a/src/impact/reason_graph.ml
-+++ b/src/impact/reason_graph.ml
-@@ -139,7 +139,7 @@ module Printer (X: AdditionalInfo) = struct
-
- let graph_attributes _ = [`Label "Impact graph"]
-
-- let default_vertex_attributes _g = [`Style [`Filled]; `Shape `Box]
-+ let default_vertex_attributes _g = [`Style `Filled; `Shape `Box]
- let default_edge_attributes _g = []
-
- let vertex_attributes v =
-diff --git a/src/kernel/stmts_graph.ml b/src/kernel/stmts_graph.ml
-index a8fe121..16059c3 100644
---- a/src/kernel/stmts_graph.ml
-+++ b/src/kernel/stmts_graph.ml
-@@ -157,12 +157,12 @@ module TP = struct
-
- let vertex_attributes s =
- match s.skind with
-- | Loop _ -> [`Color 0xFF0000; `Style [`Filled]]
-- | If _ -> [`Color 0x00FF00; `Style [`Filled]; `Shape `Diamond]
-- | Return _ -> [`Color 0x0000FF; `Style [`Filled]]
-+ | Loop _ -> [`Color 0xFF0000; `Style `Filled]
-+ | If _ -> [`Color 0x00FF00; `Style `Filled; `Shape `Diamond]
-+ | Return _ -> [`Color 0x0000FF; `Style `Filled]
- | Block _ -> [`Shape `Box; `Fontsize 8]
-- | Goto _ -> [`Shape `Diamond; `Color 0x00FFFF ; `Style [`Filled]]
-- | Instr (Skip _) -> [`Color 0x00FFFF ; `Style [`Filled]]
-+ | Goto _ -> [`Shape `Diamond; `Color 0x00FFFF ; `Style `Filled]
-+ | Instr (Skip _) -> [`Color 0x00FFFF ; `Style `Filled]
- | _ -> []
- let default_vertex_attributes _ = []
-
-diff --git a/src/logic/property_status.ml b/src/logic/property_status.ml
-index f7c278d..47485f6 100644
---- a/src/logic/property_status.ml
-+++ b/src/logic/property_status.ml
-@@ -1481,12 +1481,12 @@ module Consolidation_graph = struct
- let s = get_status p in
- let color = status_color p s in
- let style = match s with
-- | Never_tried -> [`Style [`Bold]; `Width 0.8 ]
-- | _ -> [`Style [`Filled]]
-+ | Never_tried -> [`Style `Bold; `Width 0.8 ]
-+ | _ -> [`Style `Filled]
- in
- style @ [ label v; `Color color; `Shape `Box ]
- | Emitter _ as v ->
-- [ label v; `Shape `Diamond; `Color 0xb0c4de; `Style [`Filled] ]
-+ [ label v; `Shape `Diamond; `Color 0xb0c4de; `Style `Filled ]
- | Tuning_parameter _ as v ->
- [ label v; (*`Style `Dotted;*) `Color 0xb0c4de; ]
- (*| Correctness_parameter _ (*as v*) -> assert false (*[ label v; `Color 0xb0c4de ]*)*)
-@@ -1495,7 +1495,7 @@ module Consolidation_graph = struct
- | None -> []
- | Some s ->
- let c = emitted_status_color s in
-- [ `Color c; `Fontcolor c; `Style [`Bold] ]
-+ [ `Color c; `Fontcolor c; `Style `Bold ]
-
- let default_vertex_attributes _ = []
- let default_edge_attributes _ = []
-diff --git a/src/misc/service_graph.ml b/src/misc/service_graph.ml
-index 4f866c5..d158028 100644
---- a/src/misc/service_graph.ml
-+++ b/src/misc/service_graph.ml
-@@ -289,7 +289,7 @@ Src root:%s in %s (is_root:%b) Dst:%s in %s (is_root:%b) [2d case]"
- color e
- else
- match CallG.E.label e with
-- | Inter_services -> [ `Style [`Invis] ]
-+ | Inter_services -> [ `Style `Invis ]
- | Inter_functions | Both -> color e
-
- let default_edge_attributes _ = []
-@@ -303,7 +303,7 @@ Src root:%s in %s (is_root:%b) Dst:%s in %s (is_root:%b) [2d case]"
- sg_attributes =
- [ `Label ("S " ^ cs);
- `Color (Extlib.number_to_color id);
-- `Style [`Bold] ] }
-+ `Style `Bold ] }
-
- end
-
-diff --git a/src/pdg_types/pdgTypes.ml b/src/pdg_types/pdgTypes.ml
-index 05754e4..74cdebf 100644
---- a/src/pdg_types/pdgTypes.ml
-+++ b/src/pdg_types/pdgTypes.ml
-@@ -626,7 +626,7 @@ module Pdg = struct
-
- let graph_attributes _ = [`Rankdir `TopToBottom ]
-
-- let default_vertex_attributes _ = [`Style [`Filled]]
-+ let default_vertex_attributes _ = [`Style `Filled]
- let vertex_name v = string_of_int (Node.id v)
-
- let vertex_attributes v =
-@@ -711,13 +711,13 @@ module Pdg = struct
- if Dpd.is_ctrl d then (`Arrowtail `Odot)::attrib else attrib
- in
- let attrib =
-- if Dpd.is_addr d then (`Style [`Dotted])::attrib else attrib
-+ if Dpd.is_addr d then (`Style `Dotted)::attrib else attrib
- in
- attrib
-
- let get_subgraph v =
- let mk_subgraph name attrib =
-- let attrib = (`Style [`Filled]) :: attrib in
-+ let attrib = (`Style `Filled) :: attrib in
- Some { Graph.Graphviz.DotAttributes.sg_name= name;
- sg_parent = None;
- sg_attributes = attrib }
-diff --git a/src/postdominators/print.ml b/src/postdominators/print.ml
-index f2e3a25..15f4ff2 100644
---- a/src/postdominators/print.ml
-+++ b/src/postdominators/print.ml
-@@ -63,7 +63,7 @@ module Printer = struct
-
- let graph_attributes (title, _) = [`Label title]
-
-- let default_vertex_attributes _g = [`Style [`Filled]]
-+ let default_vertex_attributes _g = [`Style `Filled]
- let default_edge_attributes _g = []
-
- let vertex_attributes (s, has_postdom) =
-diff --git a/src/semantic_callgraph/register.ml b/src/semantic_callgraph/register.ml
-index 1c79dcc..071f061 100644
---- a/src/semantic_callgraph/register.ml
-+++ b/src/semantic_callgraph/register.ml
-@@ -102,8 +102,8 @@ module Service =
- let name = Kernel_function.get_name
- let attributes v =
- [ `Style
-- [if Kernel_function.is_definition v then `Bold
-- else `Dotted] ]
-+ (if Kernel_function.is_definition v then `Bold
-+ else `Dotted) ]
- let entry_point () =
- try Some (fst (Globals.entry_point ()))
- with Globals.No_such_entry_point _ -> None
-diff --git a/src/slicing/printSlice.ml b/src/slicing/printSlice.ml
-index c5363f9..211e0bb 100644
---- a/src/slicing/printSlice.ml
-+++ b/src/slicing/printSlice.ml
-@@ -227,7 +227,7 @@ module PrintProject = struct
-
- let graph_attributes (name, _) = [`Label name]
-
-- let default_vertex_attributes _ = [`Style [`Filled]]
-+ let default_vertex_attributes _ = [`Style `Filled]
-
- let vertex_name v = match v with
- | Src fi -> SlicingMacros.fi_name fi
-@@ -280,16 +280,16 @@ module PrintProject = struct
-
- let edge_attributes (e, call) =
- let attrib = match e with
-- | (Src _, Src _) -> [`Style [`Invis]]
-- | (OptSliceCallers _, _) -> [`Style [`Invis]]
-- | (_, OptSliceCallers _) -> [`Style [`Invis]]
-+ | (Src _, Src _) -> [`Style `Invis]
-+ | (OptSliceCallers _, _) -> [`Style `Invis]
-+ | (_, OptSliceCallers _) -> [`Style `Invis]
- | _ -> []
- in match call with None -> attrib
- | Some call -> (`Label (string_of_int call.sid)):: attrib
-
- let get_subgraph v =
- let mk_subgraph name attrib =
-- let attrib = (*(`Label name) ::*) (`Style [`Filled]) :: attrib in
-+ let attrib = (*(`Label name) ::*) (`Style `Filled) :: attrib in
- Some { Graph.Graphviz.DotAttributes.sg_name= name;
- sg_parent = None;
- sg_attributes = attrib }
-diff --git a/src/syntactic_callgraph/register.ml b/src/syntactic_callgraph/register.ml
-index d4669c4..d41980e 100644
---- a/src/syntactic_callgraph/register.ml
-+++ b/src/syntactic_callgraph/register.ml
-@@ -37,8 +37,8 @@ module Service =
- let name v = nodeName v.cnInfo
- let attributes v =
- [ match v.cnInfo with
-- | NIVar (_,b) when not !b -> `Style [`Dotted]
-- | _ -> `Style [`Bold] ]
-+ | NIVar (_,b) when not !b -> `Style `Dotted
-+ | _ -> `Style `Bold ]
- let equal v1 v2 = id v1 = id v2
- let compare v1 v2 =
- let i1 = id v1 in
-diff --git a/src/wp/cil2cfg.ml b/src/wp/cil2cfg.ml
-index 6d8cf09..ba5f410 100644
---- a/src/wp/cil2cfg.ml
-+++ b/src/wp/cil2cfg.ml
-@@ -1278,9 +1278,9 @@ module Printer (PE : sig val edge_txt : edge -> string end) = struct
- | Vstart | Vend | Vexit -> [`Color 0x0000FF; `Shape `Doublecircle]
- | VfctIn | VfctOut -> [`Color 0x0000FF; `Shape `Box]
- | VblkIn _ | VblkOut _ -> [`Shape `Box]
-- | Vloop _ | Vloop2 _ -> [`Color 0xFF0000; `Style [`Filled]]
-+ | Vloop _ | Vloop2 _ -> [`Color 0xFF0000; `Style `Filled]
- | Vtest _ | Vswitch _ ->
-- [`Color 0x00FF00; `Style [`Filled]; `Shape `Diamond]
-+ [`Color 0x00FF00; `Style `Filled; `Shape `Diamond]
- | Vcall _ | Vstmt _ -> []
- in (`Label (String.escaped label))::attr
-
-@@ -1290,15 +1290,15 @@ module Printer (PE : sig val edge_txt : edge -> string end) = struct
- let attr = [] in
- let attr = (`Label (String.escaped (PE.edge_txt e)))::attr in
- let attr =
-- if is_back_edge e then (`Constraint false)::(`Style [`Bold])::attr
-+ if is_back_edge e then (`Constraint false)::(`Style `Bold)::attr
- else attr
- in
- let attr = match (edge_type e) with
- | Ethen | EbackThen -> (`Color 0x00FF00)::attr
- | Eelse | EbackElse -> (`Color 0xFF0000)::attr
-- | Ecase [] -> (`Color 0x0000FF)::(`Style [`Dashed])::attr
-+ | Ecase [] -> (`Color 0x0000FF)::(`Style `Dashed)::attr
- | Ecase _ -> (`Color 0x0000FF)::attr
-- | Enext -> (`Style [`Dotted])::attr
-+ | Enext -> (`Style `Dotted)::attr
- | Eback -> attr (* see is_back_edge above *)
- | Enone -> attr
- in
-@@ -1308,7 +1308,7 @@ module Printer (PE : sig val edge_txt : edge -> string end) = struct
-
- let get_subgraph v =
- let mk_subgraph name attrib =
-- let attrib = (`Style [`Filled]) :: attrib in
-+ let attrib = (`Style `Filled) :: attrib in
- Some { Graph.Graphviz.DotAttributes.sg_name= name;
- sg_parent = None;
- sg_attributes = attrib }
---
diff --git a/debian/patches/0005-Don-t-fail-during-the-configure-on-bytecode-architec.patch b/debian/patches/0005-Don-t-fail-during-the-configure-on-bytecode-architec.patch
deleted file mode 100644
index 475bb87..0000000
--- a/debian/patches/0005-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, 28 Apr 2014 21:25:50 +0200
-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 81acf76..4d047d4 100644
---- a/configure.in
-+++ b/configure.in
-@@ -357,7 +357,7 @@ if test "$OCAMLGRAPH_EXISTS" = "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 58b17e5..16f228a 100644
--- a/debian/patches/series
+++ b/debian/patches/series
@@ -1,5 +1,4 @@
0001-Fix-spelling-error-in-binary.patch
0002-Use-bin-cp-instead-of-usr-bin-install.patch
0003-Disable-CHMOD_RO-invocations.patch
-0004-Port-to-OCamlgraph-1.8.5.patch
-0005-Don-t-fail-during-the-configure-on-bytecode-architec.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