[Pkg-ocaml-maint-commits] [frama-c] 05/07: Refresh patches.
Mehdi Dogguy
mehdi at moszumanska.debian.org
Sun Apr 27 12:26:09 UTC 2014
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 <mehdi at 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 <mehdi at 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 <steph at 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 <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/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
More information about the Pkg-ocaml-maint-commits
mailing list