Merge branch 'feature/potassium-19.1' into 'stable/potassium'

Feature/potassium 19.1

See merge request frama-c/frama-c!2362

.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

.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

ALL_VERSIONS

 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

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
 

VERSION

-19.0
\ No newline at end of file
+19.1

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

opam/opam

 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"

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

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

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 *)

src/plugins/gui/dgraph.ml.in → 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

src/plugins/gui/dgraph.mli.in → 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 ()

src/plugins/gui/dgraph_helper.yes.ml

+(**************************************************************************)
+(*                                                                        *)
+(*  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)

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 =

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

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 ->

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