diff --git a/.gitignore b/.gitignore
index a2f38663078062c50368522097ca56df17535309..ff935dfef44e08ebbb11a4f7154ac69cc577441b 100644
--- a/.gitignore
+++ b/.gitignore
@@ -201,8 +201,8 @@ Makefile.plugin.generated
/src/kernel_internals/parsing/cparser.ml
/src/kernel_internals/parsing/cparser.mli
/src/libraries/stdlib/transitioning.ml
-/src/plugins/gui/dgraph.ml
-/src/plugins/gui/dgraph.mli
+/src/plugins/callgraph/cg_viewer.ml
+/src/plugins/gui/debug_manager.ml
/src/plugins/gui/dgraph_helper.ml
/src/plugins/gui/GSourceView.ml
/src/plugins/gui/GSourceView.mli
diff --git a/Changelog b/Changelog
index 908241542fe1af9b7a233dbc248d7841f0735f32..dacbfdaa926ba2b344c0bc94599c957f5d6fabd7 100644
--- a/Changelog
+++ b/Changelog
@@ -18,6 +18,7 @@ Open Source Release <next-release>
##################################
- MdR [2020-10-19] Update Sarif output to 2.1.0 + prettier URI
+- Dev [2020-10-20] Support for OCamlGraph 2.0.0
- ACSL [2020-10-16] Allows for axiomatic blocks-like extensions
- Variadic [2020-10-14] Don't print generated function name but print
original name and a comment with the generated name so that the
diff --git a/Makefile b/Makefile
index 425f754815018e9fc44c1fb3cd645dfefc513942..64c9342a84132a7b20497f917d6822f09645d03b 100644
--- a/Makefile
+++ b/Makefile
@@ -413,25 +413,6 @@ clean_share_link:
clean:: clean_share_link
-##############
-# Ocamlgraph #
-##############
-
-# dgraph (included in ocamlgraph)
-#[LC] Cf https://github.com/backtracking/ocamlgraph/pull/32
-ifeq ($(HAS_GNOMECANVAS),yes)
-ifneq ($(ENABLE_GUI),no)
-GRAPH_GUICMO= dgraph.cmo
-GRAPH_GUICMX= dgraph.cmx
-GRAPH_GUIO= dgraph.o
-HAS_DGRAPH=yes
-else # enable_gui is no: disable dgraph
-HAS_DGRAPH=no
-endif
-else # gnome_canvas is not yes: disable dgraph
-HAS_DGRAPH=no
-endif
-
##################
# Frama-C Kernel #
##################
@@ -739,18 +720,6 @@ src/plugins/gui/gtk_compat.ml: src/plugins/gui/gtk_compat.2.ml
endif
GENERATED+=src/plugins/gui/gtk_compat.ml
-ifeq ($(HAS_DGRAPH),yes)
- DGRAPHFILES:=debug_manager
- src/plugins/gui/dgraph_helper.ml: src/plugins/gui/dgraph_helper.yes.ml
- $(CP) $< $@
- $(CHMOD_RO) $@
-else
- DGRAPHFILES:=
- src/plugins/gui/dgraph_helper.ml: src/plugins/gui/dgraph_helper.no.ml
- $(CP) $< $@
- $(CHMOD_RO) $@
-endif
-
SINGLE_GUI_CMO:= \
wutil_once \
gtk_compat \
@@ -813,6 +782,7 @@ PLUGIN_DIR:=src/plugins/callgraph
PLUGIN_CMO:= options journalize subgraph cg services uses register
ifeq ($(HAS_DGRAPH),yes)
PLUGIN_GUI_CMO:=cg_viewer
+PLUGIN_GENERATED:=$(PLUGIN_DIR)/cg_viewer.ml
else
PLUGIN_GUI_CMO:=
PLUGIN_DISTRIB_EXTERNAL:=cg_viewer.ml
@@ -1710,9 +1680,12 @@ ALL_ML_FILES:=$(shell find src -name '*.ml' -print -o -name '*.mli' -print -o -p
ALL_ML_FILES+=ptests/ptests.ml
ifeq ($(origin MANUAL_ML_FILES),undefined)
-MANUAL_ML_FILES:=$(filter-out $(GENERATED) $(PLUGIN_GENERATED_LIST), $(ALL_ML_FILES))
+MANUAL_ML_FILES:=$(ALL_ML_FILES)
endif
+MANUAL_ML_FILES:=\
+ $(filter-out $(GENERATED) $(PLUGIN_GENERATED_LIST), $(MANUAL_ML_FILES))
+
# Allow control of files to be linted/fixed by external sources
# (e.g. pre-commit hook that will concentrate on files which have changed)
@@ -2307,6 +2280,10 @@ PLUGIN_DEP_LIST:=$(PLUGIN_LIST)
.PHONY: depend
+# tell make not to remove generated files even if they are only a byproduct
+# of making .depend.
+.PRECIOUS: $(GENERATED) share/Makefile.dynamic_config
+
# in case .depend is absent, we will make it. Otherwise, it will be left
# untouched. Only make depend will force a recomputation of dependencies
.depend: $(GENERATED) share/Makefile.dynamic_config
diff --git a/Makefile.generating b/Makefile.generating
index e55a39ff38ce2e325850aa68aff2c11074ca1a24..1c89d12715aba8629f180701b1d767f9df1620f0 100644
--- a/Makefile.generating
+++ b/Makefile.generating
@@ -134,6 +134,30 @@ src/libraries/stdlib/transitioning.ml: \
cat $< > $@
$(CHMOD_RO) $@
+ifeq ($(HAS_DGRAPH),yes)
+ DGRAPHFILES:=debug_manager
+ GENERATED+=src/plugins/gui/debug_manager.ml
+ ifeq ($(HAS_OCAMLGRAPH_2), yes)
+ DGRAPH_MODULE=Graph_gtk
+ DGRAPH_ERROR=Graph_gtk.DGraphMake.DotError
+ else
+ DGRAPH_MODULE=Dgraph
+ DGRAPH_ERROR=Dgraph.DGraphModel.DotError
+ endif
+ src/plugins/gui/debug_manager.ml \
+ src/plugins/gui/dgraph_helper.ml \
+ src/plugins/callgraph/cg_viewer.ml: %.ml: %.yes.ml Makefile.generating share/Makefile.config
+ $(RM) $@
+ $(SED) -e 's/DGRAPH_MODULE/$(DGRAPH_MODULE)/g' \
+ -e 's/DGRAPH_ERROR/$(DGRAPH_ERROR)/g' $< > $@
+ $(CHMOD_RO) $@
+else
+ DGRAPHFILES:=
+ src/plugins/gui/dgraph_helper.ml: src/plugins/gui/dgraph_helper.no.ml Makefile.generating share/Makefile.config
+ $(CP) $< $@
+ $(CHMOD_RO) $@
+endif
+
##################
# Frama-C-config #
##################
diff --git a/configure.in b/configure.in
index f1375a9fcbe30d122437275a30cd041ee8566eb1..b98dcfa282fe08c9e11e2054a1db0708fa2f423c 100644
--- a/configure.in
+++ b/configure.in
@@ -279,6 +279,10 @@ if test -z "$OCAMLGRAPH" ; then
AC_MSG_ERROR(Cannot find ocamlgraph via ocamlfind \
(requires ocamlgraph 1.8.5 or higher).)
fi
+
+AC_SUBST(HAS_OCAMLGRAPH_2)
+HAS_OCAMLGRAPH_2=no
+
case $OCAMLGRAPH in
0.* | 1.[[01234567]].* \
| 1.8.0 | 1.8.0+dev \
@@ -287,10 +291,14 @@ case $OCAMLGRAPH in
| 1.8.3 | 1.8.3+dev \
| 1.8.4 | 1.8.4+dev)
AC_MSG_ERROR(found $OCAMLGRAPH: requires 1.8.5 or higher.);;
- 1.8.5 | 1.8.6 | 1.8.7)
+ 1.8.5 | 1.8.6 | 1.8.7|1.8.8)
+ AC_MSG_RESULT(found);;
+ 2.0.*)
+ HAS_OCAMLGRAPH_2=yes
AC_MSG_RESULT(found);;
*)
- AC_MSG_RESULT(found $OCAMLGRAPH: should work);;
+ HAS_OCAMLGRAPH_2=yes
+ AC_MSG_RESULT(found $OCAMLGRAPH: should work, but is not tested);;
esac
# zarith
@@ -733,7 +741,13 @@ plugin_require(from_analysis,callgraph)
check_plugin(gui,src/plugins/gui,[support for gui],yes)
plugin_require_external(gui,lablgtk)
-plugin_use_external(gui,gnomecanvas)
+# in ocamlgraph 2, the gtk part is separated. Hence if we found it,
+# there's no need to check specifically for gnomecanvas
+if test "$HAS_OCAMLGRAPH_2" = "yes"; then
+ plugin_use_external(gui,ocaml_ocamlgraph_gtk)
+else
+ plugin_use_external(gui,gnomecanvas)
+fi
plugin_require_external(gui,gtksourceview)
plugin_use_external(gui,dot)
@@ -973,6 +987,10 @@ configure_library([LABLGTK],
[$LABLGTKPATH_FOR_CONFIGURE/lablgtk.$LIB_SUFFIX not found.],
no)
+if test "$HAS_OCAMLGRAPH_2" = yes; then
+ configure_pkg([ocamlgraph_gtk],[package ocamlgraph_gtk not found])
+fi
+
# dot and xdot tools
####################
@@ -991,6 +1009,13 @@ new_section "checking for plug-in dependencies"
check_frama_c_dependencies
+AC_SUBST(HAS_DGRAPH)
+if test "$HAS_OCAMLGRAPH_2" = "yes"; then
+ HAS_DGRAPH=$HAS_OCAML_OCAMLGRAPH_GTK;
+else
+ HAS_DGRAPH=$HAS_GNOMECANVAS
+fi
+
############################
# Substitutions to perform #
############################
diff --git a/headers/header_spec.txt b/headers/header_spec.txt
index 300b449ff1e5e07979e205ce37a16e2552ee48b3..3292d5c140719b154d3caefeac71af3922106fdf 100644
--- a/headers/header_spec.txt
+++ b/headers/header_spec.txt
@@ -810,7 +810,7 @@ src/plugins/gui/analyses_manager.ml: CEA_LGPL_OR_PROPRIETARY
src/plugins/gui/analyses_manager.mli: CEA_LGPL_OR_PROPRIETARY
src/plugins/gui/book_manager.ml: CEA_LGPL_OR_PROPRIETARY
src/plugins/gui/book_manager.mli: CEA_LGPL_OR_PROPRIETARY
-src/plugins/gui/debug_manager.ml: CEA_LGPL_OR_PROPRIETARY
+src/plugins/gui/debug_manager.yes.ml: CEA_LGPL_OR_PROPRIETARY
src/plugins/gui/debug_manager.mli: CEA_LGPL_OR_PROPRIETARY
src/plugins/gui/design.ml: CEA_LGPL_OR_PROPRIETARY
src/plugins/gui/design.mli: CEA_LGPL_OR_PROPRIETARY
diff --git a/opam/opam b/opam/opam
index d183cd513d31a989cc7a04f3df78bb13edf28501..8a26457240b7753f0f27e8d8bd9c657eb4332ae2 100644
--- a/opam/opam
+++ b/opam/opam
@@ -103,11 +103,12 @@ run-test: [
depends: [
"ocaml" { >= "4.08.1" }
- "ocamlgraph" { >= "1.8.8" & < "1.9~" }
+ "ocamlgraph" { >= "1.8.8" }
"ocamlfind" # needed beyond build stage, used by -load-module
"zarith"
"conf-autoconf" { build }
- ( ( "lablgtk" { >= "2.18.8" } & "conf-gnomecanvas" & "conf-gtksourceview" )
+ ( ( "lablgtk" { >= "2.18.8" } & "conf-gnomecanvas" & "conf-gtksourceview"
+ & ("ocamlgraph" { < "2.0" } | "ocamlgraph_gtk" ))
| ( "lablgtk3" { >= "3.1.0" & os!="macos" }
& "lablgtk3-sourceview3" & "conf-gtksourceview3" ) )
( "alt-ergo-free" | "alt-ergo" )
diff --git a/share/Makefile.config.in b/share/Makefile.config.in
index ab0d6b1f7fdb02ab20c6b8dee0202d39c144160c..7c83e350988bef5d04459f08f6e821386d646bd0 100644
--- a/share/Makefile.config.in
+++ b/share/Makefile.config.in
@@ -98,6 +98,10 @@ DEVELOPMENT ?=@DEVELOPMENT@
# Libraries #
#############
+# ocamlgraph
+HAS_OCAMLGRAPH_2 ?= @HAS_OCAMLGRAPH_2@
+HAS_DGRAPH ?= @HAS_DGRAPH@
+
# lablgtk
HAS_LABLGTK ?=@HAS_LABLGTK@
HAS_LABLGTK_CUSTOM_MODEL ?=@HAS_LABLGTK@
@@ -105,6 +109,8 @@ LABLGTK_PATH ?=@LABLGTK_PATH@
LABLGTK ?= lablgtk@LABLGTK_VERSION@
# lablgtksourceview
HAS_GTKSOURCEVIEW ?=@HAS_GTKSOURCEVIEW@
+#gnomecanvas
+HAS_GNOMECANVAS ?=@HAS_GNOMECANVAS@
LABLGTK_VERSION ?=@LABLGTK_VERSION@
ifeq ("$(LABLGTK_VERSION)","3")
@@ -116,9 +122,6 @@ else
THREAD:=
endif
-# lablgnomecanvas
-HAS_GNOMECANVAS ?=@HAS_GNOMECANVAS@
-
# apron
HAS_APRON ?=@HAS_APRON@
@@ -202,8 +205,17 @@ endif
ifneq ($(ENABLE_GUI),no)
LIBRARY_NAMES_GUI = $(LABLGTK) $(GTKSOURCEVIEW)
- ifeq ($(HAS_GNOMECANVAS),yes)
- LIBRARY_NAMES_GUI+=lablgtk2.gnomecanvas
+ ifeq ($(HAS_OCAMLGRAPH_2),yes)
+ ifeq ($(HAS_DGRAPH),yes)
+ LIBRARY_NAMES_GUI+=ocamlgraph_gtk
+ endif
+ else
+ ifeq ($(HAS_GNOMECANVAS),yes)
+ LIBRARY_NAMES_GUI+=lablgtk2.gnomecanvas
+ GRAPH_GUICMO= dgraph.cmo
+ GRAPH_GUICMX= dgraph.cmx
+ GRAPH_GUIO= dgraph.o
+ endif
endif
else
LIBRARY_NAMES_GUI =
diff --git a/src/plugins/callgraph/cg_viewer.ml b/src/plugins/callgraph/cg_viewer.yes.ml
similarity index 99%
rename from src/plugins/callgraph/cg_viewer.ml
rename to src/plugins/callgraph/cg_viewer.yes.ml
index 2d314d42fa52d7076b11bc8ce746d6a5be8ed1cc..d29b123e0cbc76b13a5a75ad2b2a69ef1897c008 100644
--- a/src/plugins/callgraph/cg_viewer.ml
+++ b/src/plugins/callgraph/cg_viewer.yes.ml
@@ -20,7 +20,7 @@
(* *)
(**************************************************************************)
-open Dgraph
+open DGRAPH_MODULE
let ($) f x = f x
diff --git a/src/plugins/gui/debug_manager.ml b/src/plugins/gui/debug_manager.yes.ml
similarity index 97%
rename from src/plugins/gui/debug_manager.ml
rename to src/plugins/gui/debug_manager.yes.ml
index 3ae5cdd11d46cc172fdf75e78bb579f8635625dc..32eb2f1965f43ca1d812787c1f350caccbb754dc 100644
--- a/src/plugins/gui/debug_manager.ml
+++ b/src/plugins/gui/debug_manager.yes.ml
@@ -20,9 +20,9 @@
(* *)
(**************************************************************************)
-(* Require Dgraph included in Ocamlgraph, thus GnomeCanvas *)
+(* Require Dgraph included in OCamlgraph/Ocamlgraph_gtk, thus GnomeCanvas *)
-open Dgraph
+open DGRAPH_MODULE
let graph_view ~packing mk_dot =
let f =
diff --git a/src/plugins/gui/dgraph_helper.yes.ml b/src/plugins/gui/dgraph_helper.yes.ml
index 30fa88ec14d5b77eeae769521ac859bb7d8ec37d..f547f895cb8bb737ed10b9421b0db40f7a8cd064 100644
--- a/src/plugins/gui/dgraph_helper.yes.ml
+++ b/src/plugins/gui/dgraph_helper.yes.ml
@@ -20,6 +20,8 @@
(* *)
(**************************************************************************)
+open DGRAPH_MODULE
+
let graph_window ~parent ~title make_view =
let height = int_of_float (float parent#default_height *. 3. /. 4.) in
let width = int_of_float (float parent#default_width *. 3. /. 4.) in
@@ -46,13 +48,13 @@ let graph_window_through_dot ~parent ~title dot_formatter =
Format.pp_print_flush fmt ();
let view =
snd
- (Dgraph.DGraphContainer.Dot.from_dot_with_commands ~packing temp_file)
+ (DGraphContainer.Dot.from_dot_with_commands ~packing temp_file)
in
view
in
try
graph_window ~parent ~title make_view
- with Dgraph.DGraphModel.DotError _ as exn ->
+ with DGRAPH_ERROR _ as exn ->
Gui_parameters.error
"@[cannot display dot graph:@ %s@]"
(Printexc.to_string exn)