diff --git a/.Makefile.lint b/.Makefile.lint
index 435f216117ecf3308c9576750bfb67e112b34b8d..4536da7d562b0c4ac3876063d18c4cc46be07ab9 100644
--- a/.Makefile.lint
+++ b/.Makefile.lint
@@ -241,7 +241,6 @@ ML_LINT_KO+=src/plugins/aorai/utils_parser.ml
ML_LINT_KO+=src/plugins/callgraph/callgraph_api.mli
ML_LINT_KO+=src/plugins/callgraph/cg.ml
ML_LINT_KO+=src/plugins/callgraph/cg.mli
-ML_LINT_KO+=src/plugins/callgraph/cg_viewer.ml
ML_LINT_KO+=src/plugins/callgraph/journalize.ml
ML_LINT_KO+=src/plugins/callgraph/journalize.mli
ML_LINT_KO+=src/plugins/callgraph/register.ml
@@ -300,9 +299,7 @@ ML_LINT_KO+=src/plugins/impact/options.ml
ML_LINT_KO+=src/plugins/impact/options.mli
ML_LINT_KO+=src/plugins/impact/pdg_aux.ml
ML_LINT_KO+=src/plugins/impact/pdg_aux.mli
-ML_LINT_KO+=src/plugins/impact/reason_graph.ml
ML_LINT_KO+=src/plugins/impact/register.ml
-ML_LINT_KO+=src/plugins/impact/register_gui.ml
ML_LINT_KO+=src/plugins/inout/cumulative_analysis.ml
ML_LINT_KO+=src/plugins/inout/cumulative_analysis.mli
ML_LINT_KO+=src/plugins/inout/derefs.ml
diff --git a/.gitignore b/.gitignore
index 633a7d72b4f6a96980eec0d1d508467a17ddfa92..4a02282acf004d3b931b47a2a0979ec39c846a98 100644
--- a/.gitignore
+++ b/.gitignore
@@ -205,3 +205,5 @@ hello-*.tar.gz
/src/plugins/gui/GSourceView.ml
/src/plugins/gui/GSourceView.mli
/tests/crowbar/integer_bb_pretty
+/src/plugins/gui/dgraph_helper.ml
+/doc/doxygen
diff --git a/ALL_VERSIONS b/ALL_VERSIONS
index 41c8714b5e8cec36bdab5450c57eb8db4568e653..0d98b133fbd3666344798215bdcc8aa5f9077db4 100644
--- a/ALL_VERSIONS
+++ b/ALL_VERSIONS
@@ -1,5 +1,6 @@
Version number Date of release Notes
============== =============== =====
+19.1 (Potassium) 2019, September 18 OCaml 4.08 compatibility
19.0 (Potassium) 2019, June 21
18.0 (Argon) 2018, November 29
Chlorine-20180502 2018, July 06 Bug fixed
diff --git a/Makefile b/Makefile
index 90e779f26d5e8b41b527d0d974ff726fedb5e349..a77fa77553286ac32e2f96b052a6311f27e5ff06 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:=
@@ -231,7 +233,7 @@ clean-check-libc:
# itself, rather than copied: otherwise, it could include references to
# non-distributed plug-ins.
DISTRIB_FILES:=\
- $(wildcard bin/migration_scripts/*2*.sh) bin/local_export.sh \
+ $(wildcard bin/migration_scripts/*2*.sh) bin/local_export.sh \
bin/frama-c bin/frama-c.byte bin/frama-c-gui bin/frama-c-gui.byte \
bin/frama-c-config bin/frama-c-script \
share/frama-c.WIN32.rc share/frama-c.Unix.rc \
@@ -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,40 +707,41 @@ 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
-DGRAPHCOMPAT:=
-ifeq ($(HAS_GNOMECANVAS),no)
-DGRAPHCOMPAT:=dgraph
-src/plugins/gui/dgraph.ml: src/plugins/gui/dgraph.ml.in
+ifeq ($(LABLGTK),lablgtk3)
+src/plugins/gui/gtk_compat.ml: src/plugins/gui/gtk_compat.3.ml
$(CP) $< $@
$(CHMOD_RO) $@
-src/plugins/gui/dgraph.mli: src/plugins/gui/dgraph.mli.in
+else
+src/plugins/gui/gtk_compat.ml: src/plugins/gui/gtk_compat.2.ml
$(CP) $< $@
$(CHMOD_RO) $@
-
-GENERATED+=src/plugins/gui/dgraph.ml src/plugins/gui/dgraph.mli
endif
+GENERATED+=src/plugins/gui/gtk_compat.ml
-ifeq ($(LABLGTK),lablgtk3)
-src/plugins/gui/gtk_compat.ml: src/plugins/gui/gtk_compat.3.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
-src/plugins/gui/gtk_compat.ml: src/plugins/gui/gtk_compat.2.ml
+ DGRAPHFILES:=
+ src/plugins/gui/dgraph_helper.ml: src/plugins/gui/dgraph_helper.no.ml
$(CP) $< $@
$(CHMOD_RO) $@
endif
-GENERATED+=src/plugins/gui/gtk_compat.ml
SINGLE_GUI_CMO:= \
wutil_once \
gtk_compat \
$(WTOOLKIT) \
$(SOURCEVIEWCOMPAT) \
- $(DGRAPHCOMPAT) \
gui_parameters \
- gtk_helper gtk_form \
+ gtk_helper \
+ dgraph_helper \
+ gtk_form \
source_viewer pretty_source source_manager book_manager \
warning_manager \
filetree \
@@ -742,9 +750,10 @@ SINGLE_GUI_CMO:= \
history \
gui_printers \
design \
- analyses_manager file_manager project_manager debug_manager \
+ analyses_manager file_manager project_manager \
help_manager \
- property_navigator
+ $(DGRAPHFILES) \
+ property_navigator \
SINGLE_GUI_CMO:= $(patsubst %,src/plugins/gui/%.cmo,$(SINGLE_GUI_CMO))
@@ -784,11 +793,11 @@ PLUGIN_NAME:=Callgraph
PLUGIN_DISTRIBUTED:=yes
PLUGIN_DIR:=src/plugins/callgraph
PLUGIN_CMO:= options journalize subgraph cg services uses register
-#GTK3: no DGraph available.
-ifeq ($(HAS_GNOMECANVAS),yes)
+ifeq ($(HAS_DGRAPH),yes)
PLUGIN_GUI_CMO:=cg_viewer
else
PLUGIN_GUI_CMO:=
+PLUGIN_DISTRIB_EXTERNAL:=cg_viewer.ml
endif
PLUGIN_CMI:= callgraph_api
PLUGIN_INTERNAL_TEST:=yes
@@ -1054,7 +1063,6 @@ PLUGIN_DIR:=src/plugins/impact
PLUGIN_CMO:= options pdg_aux reason_graph compute_impact register
PLUGIN_GUI_CMO:= register_gui
PLUGIN_DISTRIBUTED:=yes
-# PLUGIN_UNDOC:=impact_gui.ml
PLUGIN_INTERNAL_TEST:=yes
PLUGIN_DEPENDENCIES:=Inout Eva Pdg Slicing
diff --git a/VERSION b/VERSION
index 0c48b6c985e328b88a009121a6e0431a102a7db0..187bf91fcf39e005e7c6cef66284730dca1d65fd 100644
--- a/VERSION
+++ b/VERSION
@@ -1 +1 @@
-19.0
\ No newline at end of file
+19.1
diff --git a/headers/header_spec.txt b/headers/header_spec.txt
index 77d65e786310853aecf3d25fbb866511d83f5bee..8e2357fb4f23c7db39b97cc42ead13905959fe37 100644
--- a/headers/header_spec.txt
+++ b/headers/header_spec.txt
@@ -767,8 +767,9 @@ src/plugins/gui/debug_manager.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
-src/plugins/gui/dgraph.ml.in: CEA_LGPL_OR_PROPRIETARY
-src/plugins/gui/dgraph.mli.in: CEA_LGPL_OR_PROPRIETARY
+src/plugins/gui/dgraph_helper.mli: CEA_LGPL_OR_PROPRIETARY
+src/plugins/gui/dgraph_helper.no.ml: CEA_LGPL_OR_PROPRIETARY
+src/plugins/gui/dgraph_helper.yes.ml: CEA_LGPL_OR_PROPRIETARY
src/plugins/gui/file_manager.ml: CEA_LGPL_OR_PROPRIETARY
src/plugins/gui/file_manager.mli: CEA_LGPL_OR_PROPRIETARY
src/plugins/gui/filetree.ml: CEA_LGPL_OR_PROPRIETARY
diff --git a/opam/opam b/opam/opam
index bac0804058ead8e4a206b5a7e108b2643056e68a..1bb7d339a62b66c36b82031bd4dbf04fa5ae3f85 100644
--- a/opam/opam
+++ b/opam/opam
@@ -1,7 +1,7 @@
opam-version: "2.0"
name: "frama-c"
synopsis: "Platform dedicated to the analysis of source code written in C"
-version: "19.0"
+version: "19.1"
maintainer: "francois.bobot@cea.fr"
authors: [
"Michele Alberti"
@@ -86,7 +86,7 @@ run-test: [
]
depends: [
- "ocaml" { >= "4.02.3" }
+ "ocaml" { >= "4.02.3" & ( < "4.08.0~" | >= "4.08.1" ) }
"ocamlgraph" { >= "1.8.8" & < "1.9~" }
"ocamlfind" # needed beyond build stage, used by -load-module
"zarith"
diff --git a/share/Makefile.config.in b/share/Makefile.config.in
index f0bc8ae518d5973c1e46e30e979ecf6e1dcdfd73..4d24fca3ac243f90bf049292f68a9035d33cc660 100644
--- a/share/Makefile.config.in
+++ b/share/Makefile.config.in
@@ -186,7 +186,8 @@ ENABLE_USERS ?=@ENABLE_USERS@
ENABLE_EVA ?=@ENABLE_EVA@
#bytes is part of the stdlib, but is used as a transitional package.
-LIBRARY_NAMES := findlib ocamlgraph unix str dynlink bytes zarith yojson
+LIBRARY_NAMES := \
+ findlib ocamlgraph unix str dynlink bytes zarith yojson bigarray
ifeq ($(HAS_LANDMARKS),yes)
LIBRARY_NAMES += landmarks landmarks.ppx
diff --git a/src/libraries/datatype/unmarshal.ml b/src/libraries/datatype/unmarshal.ml
index 888573ad32561e550d7ee883224466c68a787de1..df6726ec62cf6d0fe9da6e13ae9dfa59fe2829c0 100644
--- a/src/libraries/datatype/unmarshal.ml
+++ b/src/libraries/datatype/unmarshal.ml
@@ -472,13 +472,25 @@ let input_val ch t =
let clos = intern_rec [] t in
return stk (Obj.add_offset (Obj.repr clos) ofs)
- | 0x12 (* CODE_CUSTOM *) ->
+ | 0x12 | 0x19 (* CODE_CUSTOM (deprecated) or CODE_CUSTOM_FIXED *) ->
let id = read_customident ch in
let v = read_custom ch id in
let dest = !ctr in
ctr := dest + 1;
return_block stk t v dest
+ | 0x18 (* CODE_CUSTOM_LEN *) ->
+ let id = read_customident ch in
+ (* Note: CODE_CUSTOM_FIXED and CODE_CUSTOM_LEN has the length of the
+ payload statically computable, but contrary to the C code,
+ we don't check that the size matches. *)
+ let _sz_32 = read32u ch in
+ let _sz_64 = read64u ch in
+ let v = read_custom ch id in
+ let dest = !ctr in
+ ctr := dest + 1;
+ return_block stk t v dest
+
| _ when code >= 0x80 (* PREFIX_SMALL_BLOCK *) ->
let tag = code land 0xF in
let size = (code lsr 4) land 0x7 in
diff --git a/src/plugins/callgraph/cg_viewer.ml b/src/plugins/callgraph/cg_viewer.ml
index 26f47325cfcf36a1f50705424bfee48b100a9f4c..bf2158b9fab14e633ff4ca3c32dece254eba31b8 100644
--- a/src/plugins/callgraph/cg_viewer.ml
+++ b/src/plugins/callgraph/cg_viewer.ml
@@ -33,7 +33,7 @@ class ['v, 'e, 'c] services_view view = object (self)
val services:
(service_id,
bool ref * Services.G.V.t DGraphViewItem.view_item list ref)
- Hashtbl.t
+ Hashtbl.t
= Hashtbl.create 10
method is_root (n:'v DGraphViewItem.view_item) = n#item.Service_graph.is_root
@@ -57,10 +57,10 @@ class ['v, 'e, 'c] services_view view = object (self)
if not (self#is_root n) then n#show ();
view#iter_succ_e
(fun e -> match self#edge_kind e with
- | Service_graph.Inter_functions | Service_graph.Both ->
+ | Service_graph.Inter_functions | Service_graph.Both ->
e#compute ();
e#show ()
- | Service_graph.Inter_services ->
+ | Service_graph.Inter_services ->
e#hide ())
n)
!nodes
@@ -77,8 +77,8 @@ class ['v, 'e, 'c] services_view view = object (self)
if not (self#is_root n) then n#hide ();
view#iter_succ_e
(fun e -> match self#edge_kind e with
- | Service_graph.Inter_services | Service_graph.Both -> e#show ()
- | Service_graph.Inter_functions -> e#hide ())
+ | Service_graph.Inter_services | Service_graph.Both -> e#show ()
+ | Service_graph.Inter_functions -> e#hide ())
n)
!nodes
@@ -86,32 +86,32 @@ class ['v, 'e, 'c] services_view view = object (self)
Kernel_function.get_id n#item.Service_graph.root.Service_graph.node
initializer
- let add_in_service n s =
- try
- let _, nodes = Hashtbl.find services s in
- nodes := n :: !nodes
- with Not_found ->
- Hashtbl.add services s (ref false, ref [ n ])
- in
- let connect_trigger_to_node n =
- let callback = function
- | `BUTTON_PRESS _ ->
+ let add_in_service n s =
+ try
+ let _, nodes = Hashtbl.find services s in
+ nodes := n :: !nodes
+ with Not_found ->
+ Hashtbl.add services s (ref false, ref [ n ])
+ in
+ let connect_trigger_to_node n =
+ let callback = function
+ | `BUTTON_PRESS _ ->
if self#is_deployed (self#service n) then self#undeploy n
else self#deploy n;
false
- | _ ->
+ | _ ->
false
+ in
+ n#connect_event ~callback
in
- n#connect_event ~callback
- in
- view#iter_nodes
- (fun n ->
- add_in_service n (self#service n);
- if self#is_root n then connect_trigger_to_node n else n#hide ());
- view#iter_edges_e
- (fun e -> match self#edge_kind e with
- | Service_graph.Inter_services | Service_graph.Both -> e#show ()
- | Service_graph.Inter_functions -> e#hide ())
+ view#iter_nodes
+ (fun n ->
+ add_in_service n (self#service n);
+ if self#is_root n then connect_trigger_to_node n else n#hide ());
+ view#iter_edges_e
+ (fun e -> match self#edge_kind e with
+ | Service_graph.Inter_services | Service_graph.Both -> e#show ()
+ | Service_graph.Inter_functions -> e#hide ())
end
@@ -160,7 +160,7 @@ let has_entry_point () =
with Globals.No_such_entry_point _ -> false
let can_show_service_graph () =
- has_entry_point () && Options.Service_roots.is_empty ()
+ has_entry_point () && Options.Service_roots.is_empty ()
let get_current_function () =
match History.get_current () with
@@ -200,7 +200,7 @@ let main (window: Design.main_window_extension_points) =
try
(* display the callgraph through its dot output *)
Service_graph.frama_c_display true;
- Gtk_helper.graph_window
+ Dgraph_helper.graph_window
~parent:window#main_window ~title:"Callgraph"
(make_graph_view services);
if warn then
@@ -232,7 +232,7 @@ let main (window: Design.main_window_extension_points) =
else false, false
in
Service_graph.frama_c_display true;
- Gtk_helper.graph_window
+ Dgraph_helper.graph_window
~parent:window#main_window ~title:"Callgraph"
(make_graph_view ~root:kf services);
(* restore old value *)
diff --git a/src/plugins/gui/dgraph.ml.in b/src/plugins/gui/dgraph_helper.mli
similarity index 79%
rename from src/plugins/gui/dgraph.ml.in
rename to src/plugins/gui/dgraph_helper.mli
index f672460d995880f279523fed4cc47a9e9b3625a3..632035356b8644aace00e2b837cf568565b0285c 100644
--- a/src/plugins/gui/dgraph.ml.in
+++ b/src/plugins/gui/dgraph_helper.mli
@@ -20,19 +20,18 @@
(* *)
(**************************************************************************)
-(* dgraph module that always generates an error: Dgraph is not available
- with gtk3
-*)
+(** Create a new window displaying a graph.
+ @plugin development guide *)
+val graph_window:
+ parent: GWindow.window ->
+ title:string ->
+ (packing:(GObj.widget -> unit) -> unit ->
+ <adapt_zoom: unit -> unit; ..>) ->
+ unit
-module DGraphModel = struct
- exception DotError of string
-end
-
-module DGraphContainer = struct
- type status = Global | Tree | Both
-
- module Dot = struct
- let from_dot_with_commands ?packing:_ ?status:_ _ =
- raise (DGraphModel.DotError "DGraph is unsupported in GTK3")
- end
-end
+(** Create a new window displaying a graph, by printing dot commands. *)
+val graph_window_through_dot:
+ parent: GWindow.window ->
+ title:string ->
+ (Format.formatter -> unit) ->
+ unit
diff --git a/src/plugins/gui/dgraph.mli.in b/src/plugins/gui/dgraph_helper.no.ml
similarity index 73%
rename from src/plugins/gui/dgraph.mli.in
rename to src/plugins/gui/dgraph_helper.no.ml
index 5cf0b53f22586ca29745199c4b73efdbd7401939..9770014dbce818815badcdb8913b9f9fc03c4110 100644
--- a/src/plugins/gui/dgraph.mli.in
+++ b/src/plugins/gui/dgraph_helper.no.ml
@@ -20,23 +20,21 @@
(* *)
(**************************************************************************)
-(* dgraph module that always generates an error: Dgraph is not available
- with gtk3
-*)
+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
+ let dialog =
+ GWindow.message_dialog ~buttons ~show:true ~message_type ~message ()
+ in
+ let callback _ = dialog#destroy () in
+ ignore (dialog#connect#response ~callback)
-module DGraphModel: sig
- exception DotError of string
-end
+let graph_window ~parent:_ ~title:_ _ =
+ window_msg_unavailable ()
-module DGraphContainer: sig
-
- type status = Global | Tree | Both
-
- module Dot: sig
- val from_dot_with_commands:
- ?packing:(GObj.widget ->unit) ->
- ?status:status ->
- string ->
- GPack.table * <adapt_zoom: unit -> unit>
- end
-end
+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 0000000000000000000000000000000000000000..4ad9e14978b4957569ef8e5594e73f4ef850225a
--- /dev/null
+++ b/src/plugins/gui/dgraph_helper.yes.ml
@@ -0,0 +1,58 @@
+(**************************************************************************)
+(* *)
+(* This file is part of Frama-C. *)
+(* *)
+(* Copyright (C) 2007-2019 *)
+(* CEA (Commissariat à l'énergie atomique et aux énergies *)
+(* alternatives) *)
+(* *)
+(* you can redistribute it and/or modify it under the terms of the GNU *)
+(* Lesser General Public License as published by the Free Software *)
+(* Foundation, version 2.1. *)
+(* *)
+(* It is distributed in the hope that it will be useful, *)
+(* but WITHOUT ANY WARRANTY; without even the implied warranty of *)
+(* MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the *)
+(* GNU Lesser General Public License for more details. *)
+(* *)
+(* See the GNU Lesser General Public License version 2.1 *)
+(* for more details (enclosed in the file licenses/LGPLv2.1). *)
+(* *)
+(**************************************************************************)
+
+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/gtk_helper.ml b/src/plugins/gui/gtk_helper.ml
index 0c3551ccbb0663fc2a0859f8a2c8561377f999f7..24f8b32bd9b57253fcc8bffd85fe726c751c6ad8 100644
--- a/src/plugins/gui/gtk_helper.ml
+++ b/src/plugins/gui/gtk_helper.ml
@@ -1014,44 +1014,6 @@ let spawn_command ?(timeout=0) ?stdout ?stderr s args f =
let prio = Glib.int_of_priority `LOW in
ignore (Glib.Idle.add ~prio for_idle)
-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)
-;;
-
let image_menu_item ~(image:GObj.widget) ~text ~packing =
let mi = GMenu.menu_item () in
let box =
diff --git a/src/plugins/gui/gtk_helper.mli b/src/plugins/gui/gtk_helper.mli
index 6d9d605b34bf5dd4da7058b20f071f786cbb47f5..c07246254458ee9ab58d18160fa79967b68dd951 100644
--- a/src/plugins/gui/gtk_helper.mli
+++ b/src/plugins/gui/gtk_helper.mli
@@ -426,22 +426,6 @@ val input_string :
parent: GWindow.window -> title:string ->
?ok:string -> ?cancel:string -> ?text:string -> string -> string option
-(** Create a new window displaying a graph.
- @plugin development guide *)
-val graph_window:
- parent: GWindow.window ->
- title:string ->
- (packing:(GObj.widget -> unit) -> unit ->
- <adapt_zoom: unit -> unit; ..>) ->
- unit
-
-(** Create a new window displaying a graph, by printing dot commands. *)
-val graph_window_through_dot:
- parent: GWindow.window ->
- title:string ->
- (Format.formatter -> unit) ->
- unit
-
(** calls the packing function to append a new menu item
with an icon and a label.
replaces GMenu.image_menu_item that has been deprecated in GTK3
diff --git a/src/plugins/gui/property_navigator.ml b/src/plugins/gui/property_navigator.ml
index 8ada692acfdd87176caef70de3dad2c766e3f90f..bfa397d868d560d33f1c2da5d3a8fe7461762d0c 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 ->
diff --git a/src/plugins/impact/reason_graph.ml b/src/plugins/impact/reason_graph.ml
index 105e52e8137497b06ca8870dbaa70666c37160d6..7b0ec744c4a346bb3ac4bf55dd11b2064dbb2f24 100644
--- a/src/plugins/impact/reason_graph.ml
+++ b/src/plugins/impact/reason_graph.ml
@@ -27,13 +27,13 @@ module NodeSet = PdgTypes.NodeSet
by the effect of [n'], and the impact is of type reason]. *)
type reason_type =
| Intraprocedural of PdgTypes.Dpd.t
- (** The effect of [n'] in [f] impact [n], which is also in [f]. *)
+ (** The effect of [n'] in [f] impact [n], which is also in [f]. *)
| InterproceduralDownward (** the effect of [n'] in [f] has an effect on a
- callee [f'] of [f], in which [n] is located. *)
+ callee [f'] of [f], in which [n] is located. *)
| InterproceduralUpward (** the effect of [n'] in [f] has an effect on a
- caller [f'] of [f] (once the call to [f] has ended), [n] being in [f']. *)
+ caller [f'] of [f] (once the call to [f] has ended), [n] being in [f']. *)
module ReasonType = Datatype.Make(
struct
@@ -75,11 +75,11 @@ let empty = {
}
module DatatypeReason = Datatype.Make(struct
- include Datatype.Serializable_undefined
- type t = reason
- let name = "Impact.Reason_graph.reason"
- let reprs = [empty]
-end)
+ include Datatype.Serializable_undefined
+ type t = reason
+ let name = "Impact.Reason_graph.reason"
+ let reprs = [empty]
+ end)
module type AdditionalInfo = sig
@@ -111,13 +111,13 @@ module Printer (X: AdditionalInfo) = struct
of the nodes belong to X.in_kf *)
let keep_edge (n1, n2, _) =
match X.in_kf with
- | None -> true
- | Some kf ->
- let in_kf n =
- try Kernel_function.equal kf (node_kf n)
- with Not_found -> false
- in
- in_kf n1 || in_kf n2
+ | None -> true
+ | Some kf ->
+ let in_kf n =
+ try Kernel_function.equal kf (node_kf n)
+ with Not_found -> false
+ in
+ in_kf n1 || in_kf n2
let iter_vertex f graph =
(* Construct a set, then iter on it. Otherwise, nodes will be seen more
@@ -125,9 +125,9 @@ module Printer (X: AdditionalInfo) = struct
let all =
Reason.Set.fold
(fun (src, dst, _ as e) acc ->
- if keep_edge e then
- NodeSet.add src (NodeSet.add dst acc)
- else acc
+ if keep_edge e then
+ NodeSet.add src (NodeSet.add dst acc)
+ else acc
) graph NodeSet.empty
in
NodeSet.iter f all
@@ -151,7 +151,7 @@ module Printer (X: AdditionalInfo) = struct
if Pdg_aux.NS.mem v X.initial_nodes then
[`Shape `Diamond; `Color 0x9090FF]
else []
- in
+ in
shape @ [`Label txt]
let edge_attributes (_, _, reason) =
@@ -162,9 +162,9 @@ module Printer (X: AdditionalInfo) = struct
in
let attribs = [`Color color] in
match reason with
- | Intraprocedural dpd ->
- `Label (Pretty_utils.to_string PdgTypes.Dpd.pretty dpd) :: attribs
- | _ -> attribs
+ | Intraprocedural dpd ->
+ `Label (Pretty_utils.to_string PdgTypes.Dpd.pretty dpd) :: attribs
+ | _ -> attribs
let get_subgraph n =
@@ -177,11 +177,18 @@ module Printer (X: AdditionalInfo) = struct
} in
Some attrs
with Not_found -> None
-
end
module Dot (X: AdditionalInfo)= Graph.Graphviz.Dot(Printer(X))
+let to_dot_formatter ?in_kf reason fmt =
+ let module Dot = Dot(struct
+ let nodes_origin = reason.nodes_origin
+ let initial_nodes = reason.initial_nodes
+ let in_kf = in_kf
+ end) in
+ Kernel.Unicode.without_unicode (Dot.fprint_graph fmt) reason.reason_graph
+
(* May raise [Sys_error] *)
let to_dot_file ~temp ?in_kf reason =
let dot_file =
@@ -196,12 +203,8 @@ let to_dot_file ~temp ?in_kf reason =
Options.abort "cannot create temporary file: %s" s
in
let cout = open_out dot_file in
- let module Dot = Dot(struct
- let nodes_origin = reason.nodes_origin
- let initial_nodes = reason.initial_nodes
- let in_kf = in_kf
- end) in
- Kernel.Unicode.without_unicode (Dot.output_graph cout) reason.reason_graph;
+ let fmt = Format.formatter_of_out_channel cout in
+ to_dot_formatter ?in_kf reason fmt;
close_out cout;
dot_file
@@ -213,8 +216,6 @@ let print_dot_graph reason =
Options.error "Could not generate impact graph: %s"
(Printexc.to_string exn)
-
-
(* Very basic textual debugging function *)
let print_reason reason =
let pp_node = !Db.Pdg.pretty_node false in
@@ -222,10 +223,10 @@ let print_reason reason =
Format.fprintf fmt "@[<v 2>%a -> %a (%s)@]"
pp_node nsrc pp_node ndst
(match reason with
- | Intraprocedural dpd ->
- Format.asprintf "intra %a" PdgTypes.Dpd.pretty dpd
- | InterproceduralDownward -> "downward"
- | InterproceduralUpward -> "upward"
+ | Intraprocedural dpd ->
+ Format.asprintf "intra %a" PdgTypes.Dpd.pretty dpd
+ | InterproceduralDownward -> "downward"
+ | InterproceduralUpward -> "upward"
)
in
Options.result "Impact graph:@.%a"
diff --git a/src/plugins/impact/register_gui.ml b/src/plugins/impact/register_gui.ml
index 8d5440c104e789c97c1057151d64ef8d26847445..322197c5bc6bf2c291164653964f996eae190a15 100644
--- a/src/plugins/impact/register_gui.ml
+++ b/src/plugins/impact/register_gui.ml
@@ -27,11 +27,11 @@ open Cil_types
module SelectedStmt = struct
include State_builder.Option_ref
- (Cil_datatype.Stmt)
- (struct
- let name = "Impact_gui.SelectedStmt"
- let dependencies = [ Ast.self ]
- end)
+ (Cil_datatype.Stmt)
+ (struct
+ let name = "Impact_gui.SelectedStmt"
+ let dependencies = [ Ast.self ]
+ end)
let set s =
set s;
@@ -41,9 +41,9 @@ end
let () =
Cmdline.run_after_extended_stage
(fun () ->
- State_dependency_graph.add_codependencies
- ~onto:SelectedStmt.self
- [ !Db.Pdg.self ])
+ State_dependency_graph.add_codependencies
+ ~onto:SelectedStmt.self
+ [ !Db.Pdg.self ])
module Highlighted_stmt : sig
val add: Kernel_function.t -> stmt -> unit
@@ -57,10 +57,10 @@ end = struct
Kernel_function.Make_Table
(Stmt.Set)
(struct
- let name = "Impact_gui.Highlighted_stmt"
- let size = 7
- let dependencies = [ SelectedStmt.self ]
- end)
+ let name = "Impact_gui.Highlighted_stmt"
+ let size = 7
+ let dependencies = [ SelectedStmt.self ]
+ end)
let add kf s =
ignore
@@ -109,12 +109,12 @@ let update_column = ref (fun _ -> ())
(* Are results shown? *)
module Enabled = struct
include State_builder.Ref
- (Datatype.Bool)
- (struct
- let name = "Impact_gui.State"
- let dependencies = []
- let default () = false
- end)
+ (Datatype.Bool)
+ (struct
+ let name = "Impact_gui.State"
+ let dependencies = []
+ let default () = false
+ end)
end
(* Should perform slicing after impact? *)
@@ -125,7 +125,7 @@ module Slicing =
let name = "Impact_gui.Slicing"
let dependencies = []
let default () = false
- end)
+ end)
(* Follow Focus mode *)
module FollowFocus =
@@ -135,7 +135,7 @@ module FollowFocus =
let name = "Impact_gui.FollowFocus"
let dependencies = []
let default () = false
- end)
+ end)
let apply_on_stmt f = function
| PStmt (kf,s) -> f kf s
@@ -154,31 +154,19 @@ let impact_highlighter buffer loc ~start ~stop =
else
SelectedStmt.may
(fun sel -> if Cil_datatype.Stmt.equal sel s then
- tag "selected_impact" "cyan")
+ tag "selected_impact" "cyan")
in
apply_on_stmt hilight loc
-let reason_graph_window main_window ?in_kf reason =
+let reason_graph_window parent ?in_kf reason =
try
- let dot_file = Reason_graph.to_dot_file ~temp:true ?in_kf reason in
- let reason_graph ~packing =
- snd (Dgraph.DGraphContainer.Dot.from_dot_with_commands ~packing dot_file)
- in
- let height = int_of_float (float main_window#default_height *. 3. /. 4.) in
- let width = int_of_float (float main_window#default_width *. 3. /. 4.) in
- let window =
- GWindow.window ~width ~height ~resizable:true ~position:`CENTER ()
- in
- let view = reason_graph ~packing:window#add in
- window#show ();
- view#adapt_zoom ()
+ let mk_dot_file = Reason_graph.to_dot_formatter ?in_kf reason in
+ Dgraph_helper.graph_window_through_dot
+ ~parent ~title:"Impact graph" mk_dot_file
with
- | Dgraph.DGraphModel.DotError _ as exn ->
- Options.error "@[cannot display impact graph:@ %s@]"
- (Printexc.to_string exn)
- | Sys_error _ as exn ->
- Options.error "issue when generating impact graph: %s"
- (Printexc.to_string exn)
+ | Sys_error _ as exn ->
+ Options.error "issue when generating impact graph: %s"
+ (Printexc.to_string exn)
let impact_statement restrict s =
@@ -195,9 +183,9 @@ let impact_statement restrict s =
let stmts = ref [] in
Kernel_function.Map.iter
(fun kf s ->
- let stmts' = Compute_impact.nodes_to_stmts s in
- stmts := stmts' :: !stmts;
- List.iter (Highlighted_stmt.add kf) stmts'
+ let stmts' = Compute_impact.nodes_to_stmts s in
+ stmts := stmts' :: !stmts;
+ List.iter (Highlighted_stmt.add kf) stmts'
) impact;
let impact = List.concat !stmts in
if Slicing.get () then ignore (Register.slice impact);
@@ -227,16 +215,11 @@ let impact_statement_ui (main_ui:Design.main_window_extension_points) s =
else (
!update_column `Contents;
main_ui#rehighlight ()
- );
- if false && Options.Reason.get () then
- let g = ReasonGraph.get () in
- let open Reason_graph in
- if not (Reason.Set.is_empty g.reason_graph) then
- reason_graph_window main_ui#main_window g
+ )
let impact_graph_of_function (main_ui:Design.main_window_extension_points) kf =
let g = ReasonGraph.get () in
- let open Reason_graph in
+ let open Reason_graph in
if not (Reason.Set.is_empty g.reason_graph) then
reason_graph_window main_ui#main_window ~in_kf:kf g
@@ -250,16 +233,16 @@ let pp_impact_on_inputs (main_ui:Design.main_window_extension_points) kf =
let call, formals, zones =
Pdg_aux.NS.fold
(fun (node, z) (call, formals, zones as acc) ->
- match !Pdg.node_key node with
- | SigCallKey _ | CallStmt _ | Stmt _ | Label _ ->
- acc (* Related to one stmt: skip *)
- | VarDecl _ -> acc (* skip *)
- | SigKey (Out _) -> acc (* probably impossible *)
- | SigKey (In InCtrl) -> (true, formals, zones)
- | SigKey (In (InNum i)) -> (call, i :: formals, zones)
- | SigKey (In (InImpl z')) ->
- let z = Locations.Zone.narrow z z' in
- (call, formals, Locations.Zone.join zones z)
+ match !Pdg.node_key node with
+ | SigCallKey _ | CallStmt _ | Stmt _ | Label _ ->
+ acc (* Related to one stmt: skip *)
+ | VarDecl _ -> acc (* skip *)
+ | SigKey (Out _) -> acc (* probably impossible *)
+ | SigKey (In InCtrl) -> (true, formals, zones)
+ | SigKey (In (InNum i)) -> (call, i :: formals, zones)
+ | SigKey (In (InImpl z')) ->
+ let z = Locations.Zone.narrow z z' in
+ (call, formals, Locations.Zone.join zones z)
) nodes (false, [], Locations.Zone.bottom)
in
if call = true || formals <> [] || not (Locations.Zone.is_bottom zones) then
@@ -267,17 +250,18 @@ let pp_impact_on_inputs (main_ui:Design.main_window_extension_points) kf =
main_ui#pretty_information
"@[<hov 2>Impacted inputs of the function:@ %t%t@]@."
(fun fmt ->
- if call then
- Format.fprintf fmt "call@ may@ be@ entirely@ skipped; ")
+ if call then
+ Format.fprintf fmt "call@ may@ be@ entirely@ skipped; ")
(fun fmt ->
- if formals <> [] then
- Pretty_utils.pp_list ~pre:"argument(s)@ " ~sep:"@ " ~suf:",@ "
- Datatype.Int.pretty fmt formals;
- if not (Locations.Zone.is_bottom zones) then
- Locations.Zone.pretty fmt zones
+ if formals <> [] then
+ Pretty_utils.pp_list ~pre:"argument(s)@ " ~sep:"@ " ~suf:",@ "
+ Datatype.Int.pretty fmt formals;
+ if not (Locations.Zone.is_bottom zones) then
+ Locations.Zone.pretty fmt zones
)
-let pp_impacted_call_outputs (main_ui:Design.main_window_extension_points) kf call_stmt =
+let pp_impacted_call_outputs
+ (main_ui:Design.main_window_extension_points) kf call_stmt =
let nodes = impact_in_kf kf in
if !pretty_info && not (Pdg_aux.NS.is_empty nodes) then
let open PdgIndex.Signature in
@@ -285,17 +269,17 @@ let pp_impacted_call_outputs (main_ui:Design.main_window_extension_points) kf ca
let ret, zones =
Pdg_aux.NS.fold
(fun (node, z) (ret, zones as acc) ->
- match !Pdg.node_key node with
- | SigCallKey (stmt', key)
- when Cil_datatype.Stmt.equal call_stmt stmt' ->
- (match key with
- | In _ -> acc (* impossible *)
- | Out OutRet -> (true, zones)
- | Out (OutLoc z') ->
- let z = Locations.Zone.narrow z z' in
- (ret, Locations.Zone.join zones z)
- )
- | _ -> acc
+ match !Pdg.node_key node with
+ | SigCallKey (stmt', key)
+ when Cil_datatype.Stmt.equal call_stmt stmt' ->
+ (match key with
+ | In _ -> acc (* impossible *)
+ | Out OutRet -> (true, zones)
+ | Out (OutLoc z') ->
+ let z = Locations.Zone.narrow z z' in
+ (ret, Locations.Zone.join zones z)
+ )
+ | _ -> acc
) nodes (false, Locations.Zone.bottom)
in
if ret = true || not (Locations.Zone.is_bottom zones) then
@@ -303,49 +287,57 @@ let pp_impacted_call_outputs (main_ui:Design.main_window_extension_points) kf ca
"@[<hov 2>Memory impacted by this call:@ %t%t@]@."
(fun fmt -> if ret then Format.fprintf fmt "return code; ")
(fun fmt ->
- if not (Locations.Zone.is_bottom zones) then
- Locations.Zone.pretty fmt zones
+ if not (Locations.Zone.is_bottom zones) then
+ Locations.Zone.pretty fmt zones
)
let impact_selector
(popup_factory:GMenu.menu GMenu.factory) main_ui ~button localizable =
match localizable with
- | PStmt (kf, s) ->
- if button = 3 || FollowFocus.get () then (
- let callback () = ignore (impact_statement_ui main_ui s) in
- ignore (popup_factory#add_item "_Impact analysis" ~callback);
- if FollowFocus.get () then
- ignore (Glib.Idle.add (fun () -> callback (); false))
- );
- if button = 1 then begin
- (* Initial nodes, at the source of the impact *)
- (match SelectedStmt.get_option () with
- | Some s' when Cil_datatype.Stmt.equal s s' ->
- if !pretty_info then
- main_ui#pretty_information "@[Impact initial nodes:@ %a@]@."
- (Pretty_utils.pp_iter Pdg_aux.NS.iter'
- ~sep:",@ " Pdg_aux.pretty_node)
- (InitialNodes.get ());
- | _ -> ()
- );
- pp_impacted_call_outputs main_ui kf s
- end
-
- | PVDecl (_, _, vi) | PGlobal (GFun ({ svar = vi }, _))
- when Cil.isFunctionType vi.vtype ->
- if button = 1 then begin
- let kf = Globals.Functions.get vi in
- pp_impact_on_inputs main_ui kf;
- end;
- if button = 3 then begin
- let g = ReasonGraph.get () in
- let open Reason_graph in
- if not (Reason.Set.is_empty g.reason_graph) then
- let kf = Globals.Functions.get vi in
- let callback () = impact_graph_of_function main_ui kf in
- ignore (popup_factory#add_item "_Impact graph" ~callback);
- end
- | _ -> ()
+ | PStmt (kf, s) ->
+ if button = 3 || FollowFocus.get () then (
+ let callback () = ignore (impact_statement_ui main_ui s) in
+ ignore (popup_factory#add_item "_Impact analysis" ~callback);
+ if Options.Reason.get ()then begin
+ let g = ReasonGraph.get () in
+ if not Reason_graph.(Reason.Set.is_empty g.reason_graph) then begin
+ let callback () =
+ reason_graph_window main_ui#main_window ~in_kf:kf g in
+ ignore (popup_factory#add_item "Impact _graph" ~callback);
+ end;
+ end;
+ if FollowFocus.get () then
+ ignore (Glib.Idle.add (fun () -> callback (); false))
+ );
+ if button = 1 then begin
+ (* Initial nodes, at the source of the impact *)
+ (match SelectedStmt.get_option () with
+ | Some s' when Cil_datatype.Stmt.equal s s' ->
+ if !pretty_info then
+ main_ui#pretty_information "@[Impact initial nodes:@ %a@]@."
+ (Pretty_utils.pp_iter Pdg_aux.NS.iter'
+ ~sep:",@ " Pdg_aux.pretty_node)
+ (InitialNodes.get ());
+ | _ -> ()
+ );
+ pp_impacted_call_outputs main_ui kf s
+ end
+
+ | PVDecl (_, _, vi) | PGlobal (GFun ({ svar = vi }, _))
+ when Cil.isFunctionType vi.vtype ->
+ if button = 1 then begin
+ let kf = Globals.Functions.get vi in
+ pp_impact_on_inputs main_ui kf;
+ end;
+ if button = 3 then begin
+ let g = ReasonGraph.get () in
+ let open Reason_graph in
+ if not (Reason.Set.is_empty g.reason_graph) then
+ let kf = Globals.Functions.get vi in
+ let callback () = impact_graph_of_function main_ui kf in
+ ignore (popup_factory#add_item "_Impact graph" ~callback);
+ end
+ | _ -> ()
let impact_panel main_ui =
let w = GPack.vbox () in
@@ -353,9 +345,9 @@ let impact_panel main_ui =
let enabled_button =
on_bool w "Enable" Enabled.get
(fun b ->
- Enabled.set b;
- !update_column `Visibility;
- main_ui#rehighlight ())
+ Enabled.set b;
+ !update_column `Visibility;
+ main_ui#rehighlight ())
in
let slicing_button =
on_bool w "Slicing after impact" Slicing.get Slicing.set
@@ -376,19 +368,19 @@ let file_tree_decorate (file_tree:Filetree.t) =
file_tree#append_pixbuf_column
~title:"Impact"
(fun globs ->
- let is_hilighted = function
- | GFun ({svar = v }, _) ->
- Highlighted_stmt.mem_kf (Globals.Functions.get v)
- | _ -> false
- in
- let id =
- (* laziness of && is used for efficiency *)
- if Enabled.get () && SelectedStmt.get_option () <> None &&
- List.exists is_hilighted globs then "gtk-apply"
- else ""
- in
- [ `STOCK_ID id ])
- (fun () -> Enabled.get () && SelectedStmt.get_option () <> None);
+ let is_hilighted = function
+ | GFun ({svar = v }, _) ->
+ Highlighted_stmt.mem_kf (Globals.Functions.get v)
+ | _ -> false
+ in
+ let id =
+ (* laziness of && is used for efficiency *)
+ if Enabled.get () && SelectedStmt.get_option () <> None &&
+ List.exists is_hilighted globs then "gtk-apply"
+ else ""
+ in
+ [ `STOCK_ID id ])
+ (fun () -> Enabled.get () && SelectedStmt.get_option () <> None);
!update_column `Visibility
let main main_ui =