diff --git a/src/plugins/dive/build.ml b/src/plugins/dive/build.ml index f2ce511fcfffd13fe02118a4a31d4e46d67fbb05..ed0d5855126c6a964dbcebc1464e59d72e5b389b 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 2bbfacc2431b289d09b0c292f54cfe699f56f144..c710f021829c06b0cb4849e25cac5be4b765d6a5 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 7b1923c7cba31d3de6afd9362f7ecf0bf8c28ac9..510d80955cb14477551e07c9337820001c9c01c9 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")