From c7fa0f796a9a5f5d15beb9f8b2606d0811d78596 Mon Sep 17 00:00:00 2001
From: Virgile Prevosto <virgile.prevosto@m4x.org>
Date: Wed, 11 Sep 2019 19:54:04 +0200
Subject: [PATCH] [gui] restore property panel in absence of dgraph
only the graph dependencies window is replaced by a dialog indicating
that it is not available
---
Makefile | 30 ++++++++++++++++------
src/plugins/gui/dgraph_helper.no.ml | 14 +++++++++++
src/plugins/gui/dgraph_helper.yes.ml | 36 +++++++++++++++++++++++++++
src/plugins/gui/property_navigator.ml | 3 ++-
4 files changed, 75 insertions(+), 8 deletions(-)
create mode 100644 src/plugins/gui/dgraph_helper.no.ml
create mode 100644 src/plugins/gui/dgraph_helper.yes.ml
diff --git a/Makefile b/Makefile
index 5e6dc25df8a..c7683ce1271 100644
--- a/Makefile
+++ b/Makefile
@@ -30,7 +30,8 @@ include share/Makefile.dynamic_config.internal
#Check share/Makefile.config available
ifndef FRAMAC_ROOT_SRCDIR
-$(error "You should run ./configure first (or autoconf if there is no configure)")
+$(error \
+ "You should run ./configure first (or autoconf if there is no configure)")
endif
###################
@@ -99,7 +100,8 @@ DEFAULT_HEADER_DIRS := headers
DEFAULT_HEADER_EXCEPTIONS := configure
# default value used for CEA_PROPRIETARY_FILES and PLUGIN_CEA_PROPRIETARY_FILES
DEFAULT_CEA_PROPRIETARY_FILES := tests/non-free/%
-# default value used for CEA_PROPRIETARY_HEADERS and PLUGIN_CEA_PROPRIETARY_HEADERS
+# default value used for CEA_PROPRIETARY_HEADERS
+# and PLUGIN_CEA_PROPRIETARY_HEADERS
DEFAULT_CEA_PROPRIETARY_HEADERS := CEA_PROPRIETARY
MERLIN_PACKAGES:=
@@ -306,7 +308,11 @@ DISTRIB_FILES:=\
# Test files to be included in the distribution (without header checking).
# Plug-ins should use PLUGIN_DISTRIB_TESTS to export their test files.
-DISTRIB_TESTS=$(shell git ls-files tests src/plugins/aorai/tests src/plugins/report/tests src/plugins/wp/tests)
+DISTRIB_TESTS=$(shell git ls-files \
+ tests \
+ src/plugins/aorai/tests \
+ src/plugins/report/tests \
+ src/plugins/wp/tests)
# files that are needed to compile API documentation of external plugins
@@ -349,7 +355,8 @@ rebuild: config.status
$(MAKE) depend $(FRAMAC_PARALLEL) && \
$(MAKE) all $(FRAMAC_PARALLEL))
-sinclude .Makefile.user # Should defines FRAMAC_PARALLEL, FRAMAC_USER_FLAGS, FRAMAC_USER_MERLIN_FLAGS
+sinclude .Makefile.user
+# Should define FRAMAC_PARALLEL, FRAMAC_USER_FLAGS, FRAMAC_USER_MERLIN_FLAGS
#Create link in share for local execution if
.PHONY:create_share_link
@@ -700,7 +707,8 @@ src/plugins/gui/GSourceView.mli: src/plugins/gui/GSourceView2.mli.in
endif
SOURCEVIEWCOMPAT:=GSourceView
-GENERATED+=src/plugins/gui/GSourceView.ml src/plugins/gui/GSourceView.mli
+GENERATED+=src/plugins/gui/GSourceView.ml src/plugins/gui/GSourceView.mli \
+ src/plugins/gui/dgraph_helper.ml src/plugins/gui/gtk_compat.ml
ifeq ($(LABLGTK),lablgtk3)
src/plugins/gui/gtk_compat.ml: src/plugins/gui/gtk_compat.3.ml
@@ -714,9 +722,15 @@ endif
GENERATED+=src/plugins/gui/gtk_compat.ml
ifeq ($(HAS_DGRAPH),yes)
- DGRAPHFILES:=debug_manager property_navigator
+ 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:= \
@@ -726,6 +740,7 @@ SINGLE_GUI_CMO:= \
$(SOURCEVIEWCOMPAT) \
gui_parameters \
gtk_helper \
+ dgraph_helper \
gtk_form \
source_viewer pretty_source source_manager book_manager \
warning_manager \
@@ -737,7 +752,8 @@ SINGLE_GUI_CMO:= \
design \
analyses_manager file_manager project_manager \
help_manager \
- $(DGRAPHFILES)
+ $(DGRAPHFILES) \
+ property_navigator \
SINGLE_GUI_CMO:= $(patsubst %,src/plugins/gui/%.cmo,$(SINGLE_GUI_CMO))
diff --git a/src/plugins/gui/dgraph_helper.no.ml b/src/plugins/gui/dgraph_helper.no.ml
new file mode 100644
index 00000000000..0c570ff6a57
--- /dev/null
+++ b/src/plugins/gui/dgraph_helper.no.ml
@@ -0,0 +1,14 @@
+let window_msg_unavailable () =
+ let buttons = GWindow.Buttons.ok in
+ let message_type = `WARNING in
+ let message =
+ "Frama-C has not been compiled against a library with \
+ working graph visualization. Property dependencies graph can't be shown."
+ in
+ ignore (GWindow.message_dialog ~buttons ~message_type ~message ())
+
+let graph_window ~parent:_ ~title:_ _ =
+ window_msg_unavailable ()
+
+let graph_window_through_dot ~parent:_ ~title:_ _ =
+ window_msg_unavailable ()
diff --git a/src/plugins/gui/dgraph_helper.yes.ml b/src/plugins/gui/dgraph_helper.yes.ml
new file mode 100644
index 00000000000..08ca0a0166a
--- /dev/null
+++ b/src/plugins/gui/dgraph_helper.yes.ml
@@ -0,0 +1,36 @@
+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
+ let graph_window =
+ GWindow.window
+ ~width ~height ~title ~resizable:true ~position:`CENTER ()
+ in
+ let view = make_view ~packing:graph_window#add () in
+ graph_window#show();
+ view#adapt_zoom();
+ ()
+;;
+
+let graph_window_through_dot ~parent ~title dot_formatter =
+ let make_view ~packing () =
+ let temp_file =
+ try
+ Extlib.temp_file_cleanup_at_exit
+ "framac_property_status_navigator_graph" "dot"
+ with Extlib.Temp_file_error s ->
+ Gui_parameters.abort "cannot create temporary file: %s" s in
+ let fmt = Format.formatter_of_out_channel (open_out temp_file) in
+ dot_formatter fmt;
+ Format.pp_print_flush fmt ();
+ let view =
+ snd
+ (Dgraph.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 ->
+ Gui_parameters.error
+ "@[cannot display dot graph:@ %s@]"
+ (Printexc.to_string exn)
diff --git a/src/plugins/gui/property_navigator.ml b/src/plugins/gui/property_navigator.ml
index 8ada692acfd..bfa397d868d 100644
--- a/src/plugins/gui/property_navigator.ml
+++ b/src/plugins/gui/property_navigator.ml
@@ -554,7 +554,8 @@ let make_panel (main_ui:main_window_extension_points) =
| Some { MODEL.finfo = { ip = ip } } ->
let format_graph ppf =
Consolidation_graph.dump (Consolidation_graph.get ip) ppf in
- Gtk_helper.graph_window_through_dot main_ui#main_window "Dependencies" format_graph
+ Dgraph_helper.graph_window_through_dot
+ main_ui#main_window "Dependencies" format_graph
| None -> ()));
view#selection#set_select_function
(fun path currently_selected ->
--
GitLab