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 <me...@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 <me...@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 <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 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 <me...@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 <me...@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 _______________________________________________ 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