This is an automated email from the git hooks/post-receive script. mehdi pushed a commit to branch master in repository frama-c.
commit a6c1ee7ba453dea4c774142153978c9e40fa86a4 Author: Mehdi Dogguy <me...@debian.org> Date: Sun Apr 27 13:23:32 2014 +0200 Refresh patches. --- debian/changelog | 3 + .../0001-Fix-spelling-error-in-binary.patch | 20 +- ...002-Use-bin-cp-instead-of-usr-bin-install.patch | 10 +- .../0003-Disable-CHMOD_RO-invocations.patch | 6 +- .../0004-Fix-auto-detection-of-ocaml-zarith.patch | 16 +- .../0005-Fix-compilation-with-OCaml-4.01.0.patch | 171 -------------- debian/patches/0005-Port-to-OCamlgraph-1.8.5.patch | 254 +++++++++++++++++++++ debian/patches/series | 2 +- 8 files changed, 284 insertions(+), 198 deletions(-) diff --git a/debian/changelog b/debian/changelog index abffde2..9144df8 100644 --- a/debian/changelog +++ b/debian/changelog @@ -1,6 +1,9 @@ frama-c (20140301+neon+dfsg-1) UNRELEASED; urgency=low * New upstream release. + - Refresh patches + - Remove 0005-Fix-compilation-with-OCaml-4.01.0.patch + - Add 0005-Port-to-OCamlgraph-1.8.5.patch * Bump build-dependency of Ocamlgraph to 1.8.5~. -- Mehdi Dogguy <me...@debian.org> Sun, 27 Apr 2014 13:16:04 +0200 diff --git a/debian/patches/0001-Fix-spelling-error-in-binary.patch b/debian/patches/0001-Fix-spelling-error-in-binary.patch index 9770502..a42f6f5 100644 --- a/debian/patches/0001-Fix-spelling-error-in-binary.patch +++ b/debian/patches/0001-Fix-spelling-error-in-binary.patch @@ -3,16 +3,16 @@ 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 +- + Changelog | 4 ++-- + cil/src/frontc/cabs2cil.ml | 4 ++-- + man/frama-c.1 | 2 +- 3 files changed, 5 insertions(+), 5 deletions(-) diff --git a/Changelog b/Changelog -index aaae442..5f972ef 100644 +index b551baf..849fd3c 100644 --- a/Changelog +++ b/Changelog -@@ -219,7 +219,7 @@ o! Kernel [2012/11/24] Various types whose names started by t_ in +@@ -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 @@ -21,7 +21,7 @@ index aaae442..5f972ef 100644 (in particular floating point -> real and integral -> integer). Fixes issue #1309. o! Kernel [2012/11/22] Remove unintuitive ?prj argument from Cil visitors, -@@ -1237,7 +1237,7 @@ o* Cil [2010/12/20] Fixed bug #645. Ast_info.constant_expr, +@@ -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 @@ -31,10 +31,10 @@ index aaae442..5f972ef 100644 ################################### diff --git a/cil/src/frontc/cabs2cil.ml b/cil/src/frontc/cabs2cil.ml -index 8351fc2..23d7769 100644 +index e803678..2699ae8 100644 --- a/cil/src/frontc/cabs2cil.ml +++ b/cil/src/frontc/cabs2cil.ml -@@ -2233,7 +2233,7 @@ let makeGlobalVarinfo (isadef: bool) (vi: varinfo) : varinfo * bool = +@@ -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. *) @@ -43,7 +43,7 @@ index 8351fc2..23d7769 100644 * was already changed to foo__extinline. We lookup with the old name *) let lookupname = if vi.vstorage = Static then -@@ -3427,7 +3427,7 @@ let default_argument_promotion idx exp = +@@ -3517,7 +3517,7 @@ let default_argument_promotion idx exp = "implicit prototype cannot have variadic arguments" | TNamed _ -> assert false (* unrollType *) in @@ -53,7 +53,7 @@ index 8351fc2..23d7769 100644 let (_,e) = castTo arg_type typ exp in (name,typ,[]), e diff --git a/man/frama-c.1 b/man/frama-c.1 -index 667f6a3..e2a1a70 100644 +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 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 3b0a768..a6bcb1b 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,20 +3,20 @@ 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 90c877e..4441720 100644 +index 8580d75..f4cc748 100644 --- a/share/Makefile.common +++ b/share/Makefile.common -@@ -157,7 +157,7 @@ CHMOD_RW= sh -c \ +@@ -138,7 +138,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 - MKDIR = mkdir -p - MV = mv -- diff --git a/debian/patches/0003-Disable-CHMOD_RO-invocations.patch b/debian/patches/0003-Disable-CHMOD_RO-invocations.patch index 537146a..fd6c9ce 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 4441720..16a6f61 100644 +index f4cc748..eb169e4 100644 --- a/share/Makefile.common +++ b/share/Makefile.common -@@ -152,7 +152,7 @@ external_make = \ +@@ -133,7 +133,7 @@ external_make = \ CAT = cat CHMOD = chmod diff --git a/debian/patches/0004-Fix-auto-detection-of-ocaml-zarith.patch b/debian/patches/0004-Fix-auto-detection-of-ocaml-zarith.patch index 966c012..6eb2926 100644 --- a/debian/patches/0004-Fix-auto-detection-of-ocaml-zarith.patch +++ b/debian/patches/0004-Fix-auto-detection-of-ocaml-zarith.patch @@ -7,23 +7,23 @@ installation method (simple one or using ocamlfind). It is always: $(ocamlc -where)/zarith/* --- - configure.in | 4 +--- + configure.in | 4 +--- 1 file changed, 1 insertion(+), 3 deletions(-) diff --git a/configure.in b/configure.in -index 7af9655..58c9bb6 100644 +index 81acf76..a823905 100644 --- a/configure.in +++ b/configure.in -@@ -364,10 +364,8 @@ AC_ARG_ENABLE( +@@ -433,10 +433,8 @@ AC_ARG_ENABLE( ZARITH_PATH=$enableval,) if test -z "$ZARITH_PATH"; then -- # standard installation procedure of zarith diverges according to +- # standard installation procedure of zarith diverges according to - # ocamlfind installation (see zarith's README) if test "$OCAMLFIND" = no ; then -- ZARITH_PATH=$OCAMLLIB -+ ZARITH_PATH=$OCAMLLIB/zarith +- ZARITH_PATH=$OCAMLLIB ++ ZARITH_PATH=$OCAMLLIB/zarith + AC_CHECK_FILE($ZARITH_PATH/zarith.$LIB_SUFFIX,HAS_ZARITH=yes,HAS_ZARITH=no) else - ZARITH_PATH=`ocamlfind printconf destdir | tr -d '\\r\\n'`/zarith - fi + ZARITH_PATH=$($OCAMLFIND query zarith 2>/dev/null | tr -d '\r\n') -- diff --git a/debian/patches/0005-Fix-compilation-with-OCaml-4.01.0.patch b/debian/patches/0005-Fix-compilation-with-OCaml-4.01.0.patch deleted file mode 100644 index add5050..0000000 --- a/debian/patches/0005-Fix-compilation-with-OCaml-4.01.0.patch +++ /dev/null @@ -1,171 +0,0 @@ -From: Stephane Glondu <st...@glondu.net> -Date: Sun, 8 Dec 2013 12:17:33 +0100 -Subject: Fix compilation with OCaml 4.01.0 - -Author: Virgile Prevosto -Origin: https://github.com/vprevosto/opam-repository/blob/master/packages/frama-c.20130601/files/4.01-compat.patch -Bug-Debian: http://bugs.debian.org/cgi-bin/bugreport.cgi?bug=731637 ---- - external/hptmap.ml | 15 +++++++++++++++ - external/hptmap.mli | 3 +++ - src/kernel/file.ml | 5 +---- - src/lib/hptset.ml | 2 ++ - src/lib/hptset.mli | 2 ++ - src/lib/setWithNearest.ml | 8 ++++++++ - src/memory_state/cvalue.mli | 4 ++-- - src/wp/qed/src/idxset.ml | 4 ++++ - 8 files changed, 37 insertions(+), 6 deletions(-) - -diff --git a/external/hptmap.ml b/external/hptmap.ml -index 39bacc4..4737d96 100644 ---- a/external/hptmap.ml -+++ b/external/hptmap.ml -@@ -357,6 +357,21 @@ struct - find htr - - -+ let find_key key htr = -+ let id = Key.id key in -+ let rec find htr = -+ match htr with -+ | Empty -> -+ raise Not_found -+ | Leaf (key', _, _) -> -+ if Key.equal key key' then -+ key' -+ else -+ raise Not_found -+ | Branch (_, mask, tree0, tree1, _) -> -+ find (if (id land mask) = 0 then tree0 else tree1) -+ in -+ find htr - - - let mem key htr = -diff --git a/external/hptmap.mli b/external/hptmap.mli -index 979e8e8..b3b5e8e 100644 ---- a/external/hptmap.mli -+++ b/external/hptmap.mli -@@ -84,6 +84,9 @@ this function will be renamed "hash" in the future *) - for [k], it is overridden. *) - - val find : key -> t -> V.t -+ -+ val find_key: key -> t -> key -+ - val remove : key -> t -> t - (** [remove k m] returns the map [m] deprived from any binding involving - [k]. *) -diff --git a/src/kernel/file.ml b/src/kernel/file.ml -index 3258366..a34aee3 100644 ---- a/src/kernel/file.ml -+++ b/src/kernel/file.ml -@@ -322,6 +322,7 @@ object(self) - Printer.pp_logic_var lv Printer.pp_varinfo v - - method vlogic_info_decl li = -+ Logic_var.Hashtbl.add known_logic_info li.l_var_info li; - List.iter - (fun lv -> - if lv.lv_kind <> LVFormal then -@@ -769,10 +770,6 @@ object(self) - DoChildren - | _ -> DoChildren - -- method vlogic_info_decl li = -- Logic_var.Hashtbl.add known_logic_info li.l_var_info li; -- DoChildren -- - method vlogic_info_use li = - let unknown () = - check_abort "logic function %s has no information" li.l_var_info.lv_name -diff --git a/src/lib/hptset.ml b/src/lib/hptset.ml -index e5fe2db..5de7957 100644 ---- a/src/lib/hptset.ml -+++ b/src/lib/hptset.ml -@@ -26,6 +26,7 @@ module type S = sig - val empty: t - val is_empty: t -> bool - val mem: elt -> t -> bool -+ val find: elt -> t -> elt - val add: elt -> t -> t - val singleton: elt -> t - val remove: elt -> t -> t -@@ -71,6 +72,7 @@ module Make(X: Id_Datatype) - type elt = X.t - - let add k = add k () -+ let find = find_key - let iter f = iter (fun x () -> f x) - let fold f = fold (fun x () -> f x) - -diff --git a/src/lib/hptset.mli b/src/lib/hptset.mli -index e1ae83d..2f1ef49 100644 ---- a/src/lib/hptset.mli -+++ b/src/lib/hptset.mli -@@ -50,6 +50,8 @@ module type S = sig - val mem: elt -> t -> bool - (** [mem x s] tests whether [x] belongs to the set [s]. *) - -+ val find: elt -> t -> elt -+ - val add: elt -> t -> t - (** [add x s] returns a set containing all elements of [s], - plus [x]. If [x] was already in [s], [s] is returned unchanged. *) -diff --git a/src/lib/setWithNearest.ml b/src/lib/setWithNearest.ml -index 0123bd7..1408fa4 100644 ---- a/src/lib/setWithNearest.ml -+++ b/src/lib/setWithNearest.ml -@@ -165,6 +165,14 @@ module Make(Ord: Datatype.S) = struct - let c = Ord.compare x v in - c = 0 || mem x (if c < 0 then l else r) - -+ let rec find x = function -+ | Empty -> raise Not_found -+ | Node(l, v, r, _) -> -+ match Ord.compare x v with -+ | c when c < 0 -> find x l -+ | 0 -> v -+ | _ -> find x r -+ - let singleton x = Node(Empty, x, Empty, 1) - - let rec remove x = function -diff --git a/src/memory_state/cvalue.mli b/src/memory_state/cvalue.mli -index 602bc4a..ac60f7b 100644 ---- a/src/memory_state/cvalue.mli -+++ b/src/memory_state/cvalue.mli -@@ -35,8 +35,8 @@ module V : sig - include module type of Location_Bytes - (* Too many aliases, and OCaml module system is not able to keep track - of all of them. Use some shortcuts *) -- with type z = Location_Bytes.z -- and type M.t = Location_Bytes.M.t -+ with type M.t = Location_Bytes.M.t -+ and type z = Location_Bytes.z - - include Lattice_With_Isotropy.S - with type t := t -diff --git a/src/wp/qed/src/idxset.ml b/src/wp/qed/src/idxset.ml -index 32dd645..7549515 100644 ---- a/src/wp/qed/src/idxset.ml -+++ b/src/wp/qed/src/idxset.ml -@@ -59,6 +59,8 @@ struct - - let mem e s = mem_k (E.id e) s - -+ let find e s = if mem e s then e else raise Not_found -+ - let lowest_bit x = x land (-x) - - let branching_bit p0 p1 = lowest_bit (p0 lxor p1) -@@ -360,6 +362,8 @@ struct - - let mem e s = mem_k (index e) s - -+ let find e s = if mem e s then e else raise Not_found -+ - let mask k m = (k lor (m-1)) land (lnot m) - - (* we first write a naive implementation of [highest_bit] --- diff --git a/debian/patches/0005-Port-to-OCamlgraph-1.8.5.patch b/debian/patches/0005-Port-to-OCamlgraph-1.8.5.patch new file mode 100644 index 0000000..798d17f --- /dev/null +++ b/debian/patches/0005-Port-to-OCamlgraph-1.8.5.patch @@ -0,0 +1,254 @@ +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/series b/debian/patches/series index cfa21fb..fb55382 100644 --- a/debian/patches/series +++ b/debian/patches/series @@ -2,4 +2,4 @@ 0002-Use-bin-cp-instead-of-usr-bin-install.patch 0003-Disable-CHMOD_RO-invocations.patch 0004-Fix-auto-detection-of-ocaml-zarith.patch -0005-Fix-compilation-with-OCaml-4.01.0.patch +0005-Port-to-OCamlgraph-1.8.5.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