diff --git a/src/plugins/dive/build.ml b/src/plugins/dive/build.ml index 19d7f0d5832d2a752f1e02ab2fa90a9f30174607..fa8bd1e797a12f25e05eda59fe46d2c0c9947551 100644 --- a/src/plugins/dive/build.ml +++ b/src/plugins/dive/build.ml @@ -198,13 +198,19 @@ type t = { let get_node context node_key = VertexTable.find context.vertex_table node_key +let update_node context node = + if + not (List.exists (Graph.Node.equal node) context.graph_diff.added_nodes) + then + context.graph_diff <- { + context.graph_diff with + added_nodes = node :: context.graph_diff.added_nodes + } + let add_node context ~node_kind ~node_locality = let node = Graph.create_node context.graph ~node_kind ~node_locality in VertexTable.add context.vertex_table node.node_key node; - context.graph_diff <- { - context.graph_diff with - added_nodes = node :: context.graph_diff.added_nodes - }; + update_node context node; node let _remove_node context node = @@ -438,6 +444,7 @@ let build_node_deps context node = Graph.create_dependency ~allow_folding context.graph dst kind node in + update_node context node; let callstack = node.node_locality.loc_callstack in match node.node_kind with | Scalar (vi,_typ,offset) -> diff --git a/src/plugins/dive/imprecision_graph.ml b/src/plugins/dive/imprecision_graph.ml index 167d850effde26c8f2dca77a8c1fbad51322d83c..55cacf98272a399f903e992ebe526cbf08aed863 100644 --- a/src/plugins/dive/imprecision_graph.ml +++ b/src/plugins/dive/imprecision_graph.ml @@ -22,7 +22,7 @@ open Graph_types -module Vertex = +module Node = struct type t = node let compare v1 v2 = v1.node_key - v2.node_key @@ -30,12 +30,12 @@ struct let equal v1 v2 = v1.node_key = v2.node_key end -module Edge = +module Dependency = struct type t = dependency let compare e1 e2 = e1.dependency_key - e2.dependency_key - let _hash e = e.dependency_key - let _equal e1 e2 = e1.dependency_key = e2.dependency_key + let hash e = e.dependency_key + let equal e1 e2 = e1.dependency_key = e2.dependency_key let default = { dependency_key = -1; dependency_kind = Data; @@ -43,22 +43,22 @@ struct } end -module G = Graph.Imperative.Digraph.ConcreteBidirectionalLabeled (Vertex) (Edge) +module G = + Graph.Imperative.Digraph.ConcreteBidirectionalLabeled (Node) (Dependency) include G -let next_node_key = ref 0 -let next_dependency_key = ref 0 +let next_key = ref 0 let create_node ?node_values ~node_kind ~node_locality g = let node = { - node_key = !next_node_key; + node_key = !next_key; node_kind; node_locality; node_values; node_deps_computed = false; } in - incr next_node_key; + incr next_key; add_vertex g node; node @@ -104,12 +104,12 @@ let create_dependency ~allow_folding g v1 dependency_kind v2 = e.dependency_multiple <- true | None -> let e = { - dependency_key = !next_dependency_key; + dependency_key = !next_key; dependency_kind; dependency_multiple = false; } in - incr next_dependency_key; + incr next_key; add_edge_e g (v1,e,v2) diff --git a/src/plugins/dive/imprecision_graph.mli b/src/plugins/dive/imprecision_graph.mli index 3a88646f26df93877c7a140209b2530c1d64cfb1..7e1162beb32be99d45313d65ff8c0928be5d7433 100644 --- a/src/plugins/dive/imprecision_graph.mli +++ b/src/plugins/dive/imprecision_graph.mli @@ -22,7 +22,13 @@ open Graph_types -include Graph.Sig.G with type V.t = node +include Graph.Sig.G + with type V.t = node + and type E.t = node * dependency * node + +module Node : Graph.Sig.COMPARABLE with type t = node + +module Dependency : Graph.Sig.COMPARABLE with type t = dependency val create : ?size:int -> unit -> t