diff --git a/src/plugins/dive/context.ml b/src/plugins/dive/context.ml index 4472ff2629e74ad168806decb5cc8bb251ad0311..3b91fbdf9ea2bbd5eb459079d421414f051f59c7 100644 --- a/src/plugins/dive/context.ml +++ b/src/plugins/dive/context.ml @@ -35,7 +35,6 @@ module Index = Datatype.Int.Hashtbl module NodeTable = FCHashtbl.Make (NodeRef) module NodeSet = Graph.Node.Set module BaseSet = Cil_datatype.Varinfo.Set -module FunctionMap = Kernel_function.Map type t = { mutable graph: Graph.t; @@ -43,7 +42,6 @@ type t = { mutable node_table: node NodeTable.t; (* node_kind * callstack -> node *) mutable unfolded_bases: BaseSet.t; mutable hidden_bases: BaseSet.t; - mutable focus: bool FunctionMap.t; mutable max_dep_fetch_count: int; mutable roots: NodeSet.t; mutable graph_diff: graph_diff; @@ -60,7 +58,6 @@ let create () = node_table = NodeTable.create 13; unfolded_bases = BaseSet.empty; hidden_bases = BaseSet.empty; - focus = FunctionMap.empty; max_dep_fetch_count = 10; roots = NodeSet.empty; graph_diff = { last_root = None ; added_nodes=[] ; removed_nodes=[] }; @@ -70,7 +67,6 @@ let clear context = context.graph <- Graph.create (); context.vertex_table <- Index.create 13; context.node_table <- NodeTable.create 13; - context.focus <- FunctionMap.empty; context.max_dep_fetch_count <- 10; context.roots <- NodeSet.empty; context.graph_diff <- { last_root = None ; added_nodes=[] ; removed_nodes=[] }