Commit f35e8676 authored by Allan Blanchard's avatar Allan Blanchard
Browse files

Merge branch 'fix/support/ocamlgraph' into 'master'

Support for OCamlgraph 2.0.0

Closes #970

See merge request frama-c/frama-c!2902
parents 2b27d0b6 b996adcc
...@@ -201,8 +201,8 @@ Makefile.plugin.generated ...@@ -201,8 +201,8 @@ Makefile.plugin.generated
/src/kernel_internals/parsing/cparser.ml /src/kernel_internals/parsing/cparser.ml
/src/kernel_internals/parsing/cparser.mli /src/kernel_internals/parsing/cparser.mli
/src/libraries/stdlib/transitioning.ml /src/libraries/stdlib/transitioning.ml
/src/plugins/gui/dgraph.ml /src/plugins/callgraph/cg_viewer.ml
/src/plugins/gui/dgraph.mli /src/plugins/gui/debug_manager.ml
/src/plugins/gui/dgraph_helper.ml /src/plugins/gui/dgraph_helper.ml
/src/plugins/gui/GSourceView.ml /src/plugins/gui/GSourceView.ml
/src/plugins/gui/GSourceView.mli /src/plugins/gui/GSourceView.mli
......
...@@ -18,6 +18,7 @@ Open Source Release <next-release> ...@@ -18,6 +18,7 @@ Open Source Release <next-release>
################################## ##################################
- MdR [2020-10-19] Update Sarif output to 2.1.0 + prettier URI - 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 - ACSL [2020-10-16] Allows for axiomatic blocks-like extensions
- Variadic [2020-10-14] Don't print generated function name but print - Variadic [2020-10-14] Don't print generated function name but print
original name and a comment with the generated name so that the original name and a comment with the generated name so that the
......
...@@ -413,25 +413,6 @@ clean_share_link: ...@@ -413,25 +413,6 @@ clean_share_link:
clean:: 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 # # Frama-C Kernel #
################## ##################
...@@ -739,18 +720,6 @@ src/plugins/gui/gtk_compat.ml: src/plugins/gui/gtk_compat.2.ml ...@@ -739,18 +720,6 @@ src/plugins/gui/gtk_compat.ml: src/plugins/gui/gtk_compat.2.ml
endif endif
GENERATED+=src/plugins/gui/gtk_compat.ml 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:= \ SINGLE_GUI_CMO:= \
wutil_once \ wutil_once \
gtk_compat \ gtk_compat \
...@@ -813,6 +782,7 @@ PLUGIN_DIR:=src/plugins/callgraph ...@@ -813,6 +782,7 @@ PLUGIN_DIR:=src/plugins/callgraph
PLUGIN_CMO:= options journalize subgraph cg services uses register PLUGIN_CMO:= options journalize subgraph cg services uses register
ifeq ($(HAS_DGRAPH),yes) ifeq ($(HAS_DGRAPH),yes)
PLUGIN_GUI_CMO:=cg_viewer PLUGIN_GUI_CMO:=cg_viewer
PLUGIN_GENERATED:=$(PLUGIN_DIR)/cg_viewer.ml
else else
PLUGIN_GUI_CMO:= PLUGIN_GUI_CMO:=
PLUGIN_DISTRIB_EXTERNAL:=cg_viewer.ml 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 ...@@ -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 ALL_ML_FILES+=ptests/ptests.ml
ifeq ($(origin MANUAL_ML_FILES),undefined) 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 endif
MANUAL_ML_FILES:=\
$(filter-out $(GENERATED) $(PLUGIN_GENERATED_LIST), $(MANUAL_ML_FILES))
# Allow control of files to be linted/fixed by external sources # Allow control of files to be linted/fixed by external sources
# (e.g. pre-commit hook that will concentrate on files which have changed) # (e.g. pre-commit hook that will concentrate on files which have changed)
...@@ -2307,6 +2280,10 @@ PLUGIN_DEP_LIST:=$(PLUGIN_LIST) ...@@ -2307,6 +2280,10 @@ PLUGIN_DEP_LIST:=$(PLUGIN_LIST)
.PHONY: depend .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 # in case .depend is absent, we will make it. Otherwise, it will be left
# untouched. Only make depend will force a recomputation of dependencies # untouched. Only make depend will force a recomputation of dependencies
.depend: $(GENERATED) share/Makefile.dynamic_config .depend: $(GENERATED) share/Makefile.dynamic_config
......
...@@ -134,6 +134,30 @@ src/libraries/stdlib/transitioning.ml: \ ...@@ -134,6 +134,30 @@ src/libraries/stdlib/transitioning.ml: \
cat $< > $@ cat $< > $@
$(CHMOD_RO) $@ $(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 # # Frama-C-config #
################## ##################
......
...@@ -279,6 +279,10 @@ if test -z "$OCAMLGRAPH" ; then ...@@ -279,6 +279,10 @@ if test -z "$OCAMLGRAPH" ; then
AC_MSG_ERROR(Cannot find ocamlgraph via ocamlfind \ AC_MSG_ERROR(Cannot find ocamlgraph via ocamlfind \
(requires ocamlgraph 1.8.5 or higher).) (requires ocamlgraph 1.8.5 or higher).)
fi fi
AC_SUBST(HAS_OCAMLGRAPH_2)
HAS_OCAMLGRAPH_2=no
case $OCAMLGRAPH in case $OCAMLGRAPH in
0.* | 1.[[01234567]].* \ 0.* | 1.[[01234567]].* \
| 1.8.0 | 1.8.0+dev \ | 1.8.0 | 1.8.0+dev \
...@@ -287,10 +291,14 @@ case $OCAMLGRAPH in ...@@ -287,10 +291,14 @@ case $OCAMLGRAPH in
| 1.8.3 | 1.8.3+dev \ | 1.8.3 | 1.8.3+dev \
| 1.8.4 | 1.8.4+dev) | 1.8.4 | 1.8.4+dev)
AC_MSG_ERROR(found $OCAMLGRAPH: requires 1.8.5 or higher.);; 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);;
*) *)
AC_MSG_RESULT(found $OCAMLGRAPH: should work);; HAS_OCAMLGRAPH_2=yes
AC_MSG_RESULT(found $OCAMLGRAPH: should work, but is not tested);;
esac esac
# zarith # zarith
...@@ -733,7 +741,13 @@ plugin_require(from_analysis,callgraph) ...@@ -733,7 +741,13 @@ plugin_require(from_analysis,callgraph)
check_plugin(gui,src/plugins/gui,[support for gui],yes) check_plugin(gui,src/plugins/gui,[support for gui],yes)
plugin_require_external(gui,lablgtk) 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_require_external(gui,gtksourceview)
plugin_use_external(gui,dot) plugin_use_external(gui,dot)
...@@ -973,6 +987,10 @@ configure_library([LABLGTK], ...@@ -973,6 +987,10 @@ configure_library([LABLGTK],
[$LABLGTKPATH_FOR_CONFIGURE/lablgtk.$LIB_SUFFIX not found.], [$LABLGTKPATH_FOR_CONFIGURE/lablgtk.$LIB_SUFFIX not found.],
no) no)
if test "$HAS_OCAMLGRAPH_2" = yes; then
configure_pkg([ocamlgraph_gtk],[package ocamlgraph_gtk not found])
fi
# dot and xdot tools # dot and xdot tools
#################### ####################
...@@ -991,6 +1009,13 @@ new_section "checking for plug-in dependencies" ...@@ -991,6 +1009,13 @@ new_section "checking for plug-in dependencies"
check_frama_c_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 # # Substitutions to perform #
############################ ############################
......
...@@ -810,7 +810,7 @@ src/plugins/gui/analyses_manager.ml: CEA_LGPL_OR_PROPRIETARY ...@@ -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/analyses_manager.mli: CEA_LGPL_OR_PROPRIETARY
src/plugins/gui/book_manager.ml: 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/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/debug_manager.mli: CEA_LGPL_OR_PROPRIETARY
src/plugins/gui/design.ml: CEA_LGPL_OR_PROPRIETARY src/plugins/gui/design.ml: CEA_LGPL_OR_PROPRIETARY
src/plugins/gui/design.mli: CEA_LGPL_OR_PROPRIETARY src/plugins/gui/design.mli: CEA_LGPL_OR_PROPRIETARY
......
...@@ -103,11 +103,12 @@ run-test: [ ...@@ -103,11 +103,12 @@ run-test: [
depends: [ depends: [
"ocaml" { >= "4.08.1" } "ocaml" { >= "4.08.1" }
"ocamlgraph" { >= "1.8.8" & < "1.9~" } "ocamlgraph" { >= "1.8.8" }
"ocamlfind" # needed beyond build stage, used by -load-module "ocamlfind" # needed beyond build stage, used by -load-module
"zarith" "zarith"
"conf-autoconf" { build } "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" { >= "3.1.0" & os!="macos" }
& "lablgtk3-sourceview3" & "conf-gtksourceview3" ) ) & "lablgtk3-sourceview3" & "conf-gtksourceview3" ) )
( "alt-ergo-free" | "alt-ergo" ) ( "alt-ergo-free" | "alt-ergo" )
......
...@@ -98,6 +98,10 @@ DEVELOPMENT ?=@DEVELOPMENT@ ...@@ -98,6 +98,10 @@ DEVELOPMENT ?=@DEVELOPMENT@
# Libraries # # Libraries #
############# #############
# ocamlgraph
HAS_OCAMLGRAPH_2 ?= @HAS_OCAMLGRAPH_2@
HAS_DGRAPH ?= @HAS_DGRAPH@
# lablgtk # lablgtk
HAS_LABLGTK ?=@HAS_LABLGTK@ HAS_LABLGTK ?=@HAS_LABLGTK@
HAS_LABLGTK_CUSTOM_MODEL ?=@HAS_LABLGTK@ HAS_LABLGTK_CUSTOM_MODEL ?=@HAS_LABLGTK@
...@@ -105,6 +109,8 @@ LABLGTK_PATH ?=@LABLGTK_PATH@ ...@@ -105,6 +109,8 @@ LABLGTK_PATH ?=@LABLGTK_PATH@
LABLGTK ?= lablgtk@LABLGTK_VERSION@ LABLGTK ?= lablgtk@LABLGTK_VERSION@
# lablgtksourceview # lablgtksourceview
HAS_GTKSOURCEVIEW ?=@HAS_GTKSOURCEVIEW@ HAS_GTKSOURCEVIEW ?=@HAS_GTKSOURCEVIEW@
#gnomecanvas
HAS_GNOMECANVAS ?=@HAS_GNOMECANVAS@
LABLGTK_VERSION ?=@LABLGTK_VERSION@ LABLGTK_VERSION ?=@LABLGTK_VERSION@
ifeq ("$(LABLGTK_VERSION)","3") ifeq ("$(LABLGTK_VERSION)","3")
...@@ -116,9 +122,6 @@ else ...@@ -116,9 +122,6 @@ else
THREAD:= THREAD:=
endif endif
# lablgnomecanvas
HAS_GNOMECANVAS ?=@HAS_GNOMECANVAS@
# apron # apron
HAS_APRON ?=@HAS_APRON@ HAS_APRON ?=@HAS_APRON@
...@@ -202,8 +205,17 @@ endif ...@@ -202,8 +205,17 @@ endif
ifneq ($(ENABLE_GUI),no) ifneq ($(ENABLE_GUI),no)
LIBRARY_NAMES_GUI = $(LABLGTK) $(GTKSOURCEVIEW) LIBRARY_NAMES_GUI = $(LABLGTK) $(GTKSOURCEVIEW)
ifeq ($(HAS_GNOMECANVAS),yes) ifeq ($(HAS_OCAMLGRAPH_2),yes)
LIBRARY_NAMES_GUI+=lablgtk2.gnomecanvas 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 endif
else else
LIBRARY_NAMES_GUI = LIBRARY_NAMES_GUI =
......
...@@ -20,7 +20,7 @@ ...@@ -20,7 +20,7 @@
(* *) (* *)
(**************************************************************************) (**************************************************************************)
open Dgraph open DGRAPH_MODULE
let ($) f x = f x let ($) f x = f x
......
...@@ -20,9 +20,9 @@ ...@@ -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 graph_view ~packing mk_dot =
let f = let f =
......
...@@ -20,6 +20,8 @@ ...@@ -20,6 +20,8 @@
(* *) (* *)
(**************************************************************************) (**************************************************************************)
open DGRAPH_MODULE
let graph_window ~parent ~title make_view = let graph_window ~parent ~title make_view =
let height = int_of_float (float parent#default_height *. 3. /. 4.) in let height = int_of_float (float parent#default_height *. 3. /. 4.) in
let width = int_of_float (float parent#default_width *. 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 = ...@@ -46,13 +48,13 @@ let graph_window_through_dot ~parent ~title dot_formatter =
Format.pp_print_flush fmt (); Format.pp_print_flush fmt ();
let view = let view =
snd snd
(Dgraph.DGraphContainer.Dot.from_dot_with_commands ~packing temp_file) (DGraphContainer.Dot.from_dot_with_commands ~packing temp_file)
in in
view view
in in
try try
graph_window ~parent ~title make_view graph_window ~parent ~title make_view
with Dgraph.DGraphModel.DotError _ as exn -> with DGRAPH_ERROR _ as exn ->
Gui_parameters.error Gui_parameters.error
"@[cannot display dot graph:@ %s@]" "@[cannot display dot graph:@ %s@]"
(Printexc.to_string exn) (Printexc.to_string exn)
Markdown is supported
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment