From 3fc99662118610af4dd6568a8c4c2d7b3c3e4139 Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?David=20B=C3=BChler?= <david.buhler@cea.fr>
Date: Tue, 8 Jun 2021 10:45:38 +0200
Subject: [PATCH] [dive] Removes unused record field context.focus.
---
src/plugins/dive/context.ml | 4 ----
1 file changed, 4 deletions(-)
diff --git a/src/plugins/dive/context.ml b/src/plugins/dive/context.ml
index 4472ff2629e..3b91fbdf9ea 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=[] }
--
GitLab