diff --git a/src/plugins/dive/Makefile.in b/src/plugins/dive/Makefile.in
index 4600d3c506fd744208c28dc03aa5c97669664c51..b435afe3c72513c03691628b2a5b15316322e302 100644
--- a/src/plugins/dive/Makefile.in
+++ b/src/plugins/dive/Makefile.in
@@ -38,9 +38,10 @@ endif
PLUGIN_DIR ?=.
PLUGIN_NAME := Dive
-PLUGIN_CMO := self callstack node_kind imprecision_graph build main
+PLUGIN_CMO := self callstack node_kind imprecision_graph build main \
+ server_interface
PLUGIN_CMI:= graph_types
-PLUGIN_DEPENDENCIES:= Eva Studia
+PLUGIN_DEPENDENCIES:= Eva Studia Server
PLUGIN_HAS_MLI:= yes
PLUGIN_TESTS_DIRS:=dive
PLUGIN_GENERATED:=
diff --git a/src/plugins/dive/imprecision_graph.ml b/src/plugins/dive/imprecision_graph.ml
index cb504b91cad7214775b000a0cf826fcb1d8370dc..a2bd2a9b4544d849db5b29895adda5b8324f34e7 100644
--- a/src/plugins/dive/imprecision_graph.ml
+++ b/src/plugins/dive/imprecision_graph.ml
@@ -181,7 +181,7 @@ let ouptput_to_dot out_channel g =
in
Dot.output_graph out_channel g
-let ouptput_to_json out_channel g =
+let to_json g =
let rec output_kinstr = function
| Cil_types.Kglobal -> Json.of_string "global"
| Cil_types.Kstmt stmt -> Json.of_int stmt.Cil_types.sid
@@ -250,5 +250,8 @@ let ouptput_to_json out_channel g =
in
let nodes = Json.of_list (fold_vertex output_node g [])
and deps = Json.of_list (fold_edges_e output_dep g []) in
- let json = Json.of_fields [("nodes", nodes) ; ("deps", deps)] in
- Json.save_channel ~pretty:true out_channel json
\ No newline at end of file
+ Json.of_fields [("nodes", nodes) ; ("deps", deps)]
+
+let ouptput_to_json out_channel g =
+ let json = to_json g in
+ Json.save_channel ~pretty:true out_channel json
diff --git a/src/plugins/dive/imprecision_graph.mli b/src/plugins/dive/imprecision_graph.mli
index 7fb85551be20a995bf9319b1a61f7215690e8f2d..0f4308e57a16e06e81f4982b30c9b99b46d4e3be 100644
--- a/src/plugins/dive/imprecision_graph.mli
+++ b/src/plugins/dive/imprecision_graph.mli
@@ -36,5 +36,6 @@ val update_node_precision : node -> node_precision -> unit
val create_dependency : allow_folding:bool -> t -> node -> dependency_kind ->
node -> unit
+val to_json : t -> Json.t
val ouptput_to_dot : out_channel -> t -> unit
val ouptput_to_json : out_channel -> t -> unit
diff --git a/src/plugins/dive/server_interface.ml b/src/plugins/dive/server_interface.ml
new file mode 100644
index 0000000000000000000000000000000000000000..7b1923c7cba31d3de6afd9362f7ecf0bf8c28ac9
--- /dev/null
+++ b/src/plugins/dive/server_interface.ml
@@ -0,0 +1,116 @@
+(**************************************************************************)
+(* *)
+(* This file is part of the Frama-C plug-in `Dive'. *)
+(* *)
+(* Copyright (C) 2018 *)
+(* 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). *)
+(* *)
+(**************************************************************************)
+
+open Server
+
+(* TODO: state *)
+let get_graph =
+ let graph = ref None in
+ fun () ->
+ match !graph with
+ | Some g -> g
+ | None ->
+ let g = Build.create () in
+ graph := Some g;
+ g
+
+
+let page = Doc.page (`Plugin "Dive")
+ ~title:"Dive into dependency graph"
+ ~filename:"dive.md"
+
+module Graph =
+struct
+ type t = Imprecision_graph.t
+ let syntax = Syntax.any
+ let to_json = Imprecision_graph.to_json
+end
+
+module Variable = Data.Collection (struct
+ type t = Cil_types.varinfo
+ let syntax = Syntax.publish ~page ~name:"variable"
+ ~synopsis:(Syntax.record [
+ "fun", Syntax.option Syntax.string ;
+ "var", Syntax.string ])
+ ~descr:(Markdown.rm "Variable from the program") ()
+
+ let to_json v =
+ let varname = v.Cil_types.vname in
+ let fields = [ "var" , `String varname ] in
+ let fields = match Kernel_function.find_defining_kf v with
+ | Some kf -> ("fun", `String (Kernel_function.get_name kf)) :: fields
+ | None -> fields
+ in
+ `Assoc fields
+
+ let of_json json =
+ try
+ let funname =
+ try Some (Json.(string (field "fun" json)))
+ with Not_found -> None
+ and varname = Json.(string (field "var" json)) in
+ match funname with
+ | Some name ->
+ let kf =
+ try
+ Globals.Functions.find_by_name name
+ with Not_found ->
+ Data.failure json "no function '%s'" name
+ in
+ let vi =
+ try Globals.Vars.find_from_astinfo varname (Cil_types.VLocal kf)
+ with Not_found ->
+ try Globals.Vars.find_from_astinfo varname (Cil_types.VFormal kf)
+ with Not_found ->
+ Data.failure json "no variable '%s' in function '%s'"
+ varname name
+ in
+ vi
+ | None ->
+ match
+ Globals.Syntactic_search.find_in_scope varname Cil_types.Program
+ with
+ | Some vi -> vi
+ | None ->
+ Data.failure json "no global variable '%s'" varname
+ with Not_found | Failure _ ->
+ Data.failure json "Invalid source format"
+ end)
+
+
+let () = Request.register ~page
+ ~kind:`GET ~name:"dive.graph"
+ ~descr:(Markdown.rm "Retrieve the whole graph")
+ ~input:(module Data.Junit) ~output:(module Graph)
+ (fun () -> Build.get_graph (get_graph ()))
+
+let () = Request.register ~page
+ ~kind:`EXEC ~name:"dive.add_var"
+ ~descr:(Markdown.rm "Add a variable to the graph")
+ ~input:(module Variable) ~output:(module Graph)
+ begin fun var ->
+ let depth = Self.DepthLimit.get () in
+ let g = get_graph () in
+ Build.add_var ~depth g var;
+ Build.get_graph g
+ end
+
diff --git a/src/plugins/dive/server_interface.mli b/src/plugins/dive/server_interface.mli
new file mode 100644
index 0000000000000000000000000000000000000000..77495598c83d67066115ad227517a0865e17396a
--- /dev/null
+++ b/src/plugins/dive/server_interface.mli
@@ -0,0 +1,23 @@
+(**************************************************************************)
+(* *)
+(* This file is part of the Frama-C plug-in `Dive'. *)
+(* *)
+(* Copyright (C) 2018 *)
+(* 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). *)
+(* *)
+(**************************************************************************)
+
+module Variable : Server.Data.S_collection with type t = Cil_types.varinfo