From 297cc06923aeecf3c81a37c2cb2dc19f27e60626 Mon Sep 17 00:00:00 2001
From: Valentin Perrelle <valentin.perrelle@cea.fr>
Date: Fri, 9 Aug 2019 23:24:35 +0200
Subject: [PATCH] [Dive] Add command dive.clear
---
src/plugins/dive/build.ml | 17 ++++++++++++-----
src/plugins/dive/build.mli | 2 ++
src/plugins/dive/server_interface.ml | 6 ++++++
3 files changed, 20 insertions(+), 5 deletions(-)
diff --git a/src/plugins/dive/build.ml b/src/plugins/dive/build.ml
index f2ce511fcff..ed0d5855126 100644
--- a/src/plugins/dive/build.ml
+++ b/src/plugins/dive/build.ml
@@ -161,10 +161,10 @@ module BaseSet = Cil_datatype.Varinfo.Set
module FunctionMap = Kernel_function.Map
type t = {
- graph: Graph.t;
- node_table: node NodeTable.t;
- file_table: node FileTable.t;
- callstack_table: node CallstackTable.t;
+ mutable graph: Graph.t;
+ mutable node_table: node NodeTable.t;
+ mutable file_table: node FileTable.t;
+ mutable callstack_table: node CallstackTable.t;
mutable unfolded_bases: BaseSet.t;
mutable hidden_bases: BaseSet.t;
mutable focus: bool FunctionMap.t;
@@ -411,7 +411,6 @@ let build_node_deps context node =
| Cluster -> ()
-
(* --- Graph initialization --- *)
let create () =
@@ -427,6 +426,14 @@ let create () =
roots = [];
}
+let clear context =
+ context.graph <- Graph.create ();
+ context.node_table <- NodeTable.create 13;
+ context.file_table <- FileTable.create 13;
+ context.callstack_table <- CallstackTable.create 13;
+ context.focus <- FunctionMap.empty;
+ context.roots <- []
+
(* --- Accessors --- *)
diff --git a/src/plugins/dive/build.mli b/src/plugins/dive/build.mli
index 2bbfacc2431..c710f021829 100644
--- a/src/plugins/dive/build.mli
+++ b/src/plugins/dive/build.mli
@@ -23,6 +23,8 @@
type t
val create : unit -> t
+val clear : t -> unit (* reset to almost an empty context,
+ but keeps folded and hidden bases *)
val get_graph : t -> Imprecision_graph.t
val get_roots : t -> Graph_types.node list
diff --git a/src/plugins/dive/server_interface.ml b/src/plugins/dive/server_interface.ml
index 7b1923c7cba..510d80955cb 100644
--- a/src/plugins/dive/server_interface.ml
+++ b/src/plugins/dive/server_interface.ml
@@ -103,6 +103,12 @@ let () = Request.register ~page
~input:(module Data.Junit) ~output:(module Graph)
(fun () -> Build.get_graph (get_graph ()))
+let () = Request.register ~page
+ ~kind:`EXEC ~name:"dive.clear"
+ ~descr:(Markdown.rm "Erase the graph and start over with an empty one")
+ ~input:(module Data.Junit) ~output:(module Data.Junit)
+ (fun () -> Build.clear (get_graph ()))
+
let () = Request.register ~page
~kind:`EXEC ~name:"dive.add_var"
~descr:(Markdown.rm "Add a variable to the graph")
--
GitLab