diff --git a/src/plugins/dive/build.ml b/src/plugins/dive/build.ml
index 5a5f88fc82d42bddef0c71ad0bd83df0a3ec5a93..b888bc94484725b403272360d295a35ead90c79b 100644
--- a/src/plugins/dive/build.ml
+++ b/src/plugins/dive/build.ml
@@ -419,7 +419,6 @@ let build_node_deps context node =
| Scattered (_lval, _location) -> () (* TODO: implements *)
| Alarm (stmt,alarm) ->
build_alarm_deps callstack stmt alarm
- | Cluster -> ()
(* --- Graph initialization --- *)
@@ -474,7 +473,7 @@ let explore ~depth context root =
let is_root = Graph.Node.equal node root (* the root is always explored *)
and is_intersting_kind = match node.node_kind with
| Scalar _ | Composite _ | Alarm _ -> true
- | Scattered _ | Cluster -> false
+ | Scattered _ -> false
in
is_root || (not node.node_hidden && is_intersting_kind)
in
diff --git a/src/plugins/dive/graph_types.mli b/src/plugins/dive/graph_types.mli
index e8f4943518996149c7bb6a0118e7b0565876892d..2089520d8d209e68bc36dbe0097ddb56650e4dde 100644
--- a/src/plugins/dive/graph_types.mli
+++ b/src/plugins/dive/graph_types.mli
@@ -25,7 +25,6 @@ type node_kind =
| Composite of Cil_types.varinfo
| Scattered of Cil_types.lval * Locations.location
| Alarm of Cil_types.stmt * Alarms.alarm
- | Cluster (* Dummy node, hack for Ocamlgraph Graphviz Dot module *)
type node_locality = {
loc_file : string;
diff --git a/src/plugins/dive/imprecision_graph.ml b/src/plugins/dive/imprecision_graph.ml
index 4816eb263b0d48e782f29e9ddab03ab2df0b5f04..01732d253bb58e9880f3bdd65d603a3a127f1b3d 100644
--- a/src/plugins/dive/imprecision_graph.ml
+++ b/src/plugins/dive/imprecision_graph.ml
@@ -47,6 +47,12 @@ module G =
Graph.Imperative.Digraph.ConcreteBidirectionalLabeled (Node) (Dependency)
include G
+let vertices g =
+ fold_vertex (fun n acc -> n ::acc) g []
+
+let edges g =
+ fold_edges_e (fun d acc -> d ::acc) g []
+
let next_key = ref 0
let create_node ?node_values ~node_kind ~node_locality g =
@@ -127,45 +133,12 @@ let find_independant_nodes g roots =
let module Table = Hashtbl.Make (Node) in
let table = Table.create 13 in
List.iter (Dfs.prefix_component (fun n -> Table.add table n true) g) roots;
- let keep_node n =
- Table.mem table n || n.node_kind = Cluster
- in
- fold_vertex (fun n acc -> if keep_node n then acc else n :: acc) g []
-
-
-let add_dummy_nodes g =
- let module FileTable = Datatype.String.Hashtbl in
- let module CallstackTable = Value_types.Callstack.Hashtbl in
- let file_table = FileTable.create 13 in
- let callstack_table = CallstackTable.create 13 in
- let g = copy g in
-
- let create_locality_vertex { node_locality } =
- let { loc_file ; loc_callstack } = node_locality in
- let rec add_file _ =
- let node_locality = { node_locality with loc_callstack = [] } in
- create_node g ~node_kind:Cluster ~node_locality
- and add_callstack = function
- | [] -> assert false
- | _ :: t as loc_callstack ->
- let node_locality = { node_locality with loc_callstack } in
- if t <> [] then
- ignore (CallstackTable.memo callstack_table t add_callstack);
- create_node g ~node_kind:Cluster ~node_locality
- in
- match loc_callstack with
- | [] ->
- ignore (FileTable.memo file_table loc_file add_file)
- | cs ->
- ignore (CallstackTable.memo callstack_table cs add_callstack)
- in
- iter_vertex create_locality_vertex g;
- g
+ fold_vertex (fun n acc -> if Table.mem table n then acc else n :: acc) g []
let ouptput_to_dot out_channel g =
let open Graph.Graphviz.DotAttributes in
- let g = add_dummy_nodes g in
+ (* let g = add_dummy_nodes g in *)
let build_label s = `HtmlLabel (Extlib.html_escape s) in
@@ -216,7 +189,6 @@ let ouptput_to_dot out_channel g =
| Alarm _ -> [ `Shape `Doubleoctagon ;
`Style `Bold ; `Color 0xff0000 ;
`Style `Filled ; `Fillcolor 0xff0000 ]
- | Cluster -> [ `Style `Invis ]
and values = match v.node_values with
| None -> []
| Some ({values_grade=Singleton}) ->
@@ -269,7 +241,6 @@ struct
| Composite _ -> "composite"
| Scattered _ -> "scattered"
| Alarm _ -> "alarm"
- | Cluster -> "dummy"
in
Json.of_string s
@@ -343,28 +314,13 @@ struct
]
let output_graph g =
- let add_node node acc =
- if node.node_kind = Cluster
- then acc
- else output_node node :: acc
- and add_edge d acc =
- output_dep d :: acc
- in
Json.of_fields [
- ("nodes", Json.of_list (fold_vertex add_node g [])) ;
- ("deps", Json.of_list (fold_edges_e add_edge g []))
+ ("nodes", Json.of_list (List.map output_node (vertices g))) ;
+ ("deps", Json.of_list (List.map output_dep (edges g)))
]
let output_diff g diff =
- let add_node acc node =
- if node.node_kind = Cluster
- then acc
- else output_node node :: acc
- and add_dep d acc =
- output_dep d :: acc
- in
- let added_nodes =
- List.fold_left add_node [] diff.added_nodes
+ let added_nodes = List.map output_node diff.added_nodes
and added_deps =
let module Set = Set.Make (struct
type t = edge
@@ -377,7 +333,7 @@ struct
set
in
let set = List.fold_left collect_deps Set.empty diff.added_nodes in
- Set.fold add_dep set []
+ List.map output_dep (Set.elements set)
and removed_nodes =
List.map (fun node -> Json.of_int node.node_key) diff.removed_nodes
in
diff --git a/src/plugins/dive/node_kind.ml b/src/plugins/dive/node_kind.ml
index 396119c63e5ccf6b3a782ffbafe49531f5c646de..a59e6de12f390a0dfbc1757eb688d0258d2648ec 100644
--- a/src/plugins/dive/node_kind.ml
+++ b/src/plugins/dive/node_kind.ml
@@ -35,14 +35,14 @@ struct
let name = "Node_kind"
- let reprs = [ Cluster ]
+ let reprs = [ Scalar (
+ List.hd Cil_datatype.Varinfo.reprs,
+ List.hd Cil_datatype.Typ.reprs,
+ List.hd Cil_datatype.Offset.reprs) ]
let compare k1 k2 =
let open Cil_datatype in
match k1, k2 with
- | Cluster, Cluster -> 0
- | Cluster, _ -> 1
- | _, Cluster -> -1
| Scalar (vi1, _, offset1), Scalar (vi2, _, offset2) ->
Varinfo.compare vi1 vi2 <?> (OffsetStructEq.compare, offset1, offset2)
| Scalar _, _ -> 1
@@ -60,7 +60,6 @@ struct
let equal k1 k2 =
let open Cil_datatype in
match k1, k2 with
- | Cluster, Cluster -> true
| Scalar (vi1, _, offset1), Scalar (vi2, _, offset2) ->
Varinfo.equal vi1 vi2 && OffsetStructEq.equal offset1 offset2
| Composite vi1, Composite vi2 -> Varinfo.equal vi1 vi2
@@ -73,7 +72,6 @@ struct
let hash k =
let open Cil_datatype in
match k with
- | Cluster -> Hashtbl.hash 0
| Scalar (vi, _, offset) ->
Hashtbl.hash (1, Varinfo.hash vi, OffsetStructEq.hash offset)
| Composite vi -> Hashtbl.hash (2, Varinfo.hash vi)
@@ -88,7 +86,7 @@ include Datatype.Make (DatatypeInput)
let get_base = function
| Scalar (vi,_,_) | Composite (vi) -> Some vi
- | Scattered _ | Alarm _ | Cluster -> None
+ | Scattered _ | Alarm _ -> None
let to_location = function
| Scalar (vi,typ,offset) ->
@@ -98,17 +96,16 @@ let to_location = function
Some (Locations.loc_of_varinfo vi)
| Scattered (_,loc) ->
Some loc
- | Alarm _ | Cluster -> None
+ | Alarm _ -> None
let to_lval = function
| Scalar (vi,_typ,offset) -> Some (Cil_types.Var vi, offset)
| Composite (vi) -> Some (Cil_types.Var vi, Cil_types.NoOffset)
| Scattered (lval,_) -> Some lval
- | Alarm (_,_) | Cluster -> None
+ | Alarm (_,_) -> None
let pretty fmt = function
| (Scalar _ | Composite _ | Scattered _) as kind ->
Cil_printer.pp_lval fmt (Extlib.the (to_lval kind))
| Alarm (_stmt,alarm) ->
Cil_printer.pp_predicate fmt (Alarms.create_predicate alarm)
- | Cluster -> ()