[dive] Do not explore several time the same node

src/plugins/dive/build.ml

@@ -557,11 +557,14 @@ let should_explore node =
   | _ -> not node.node_hidden
 
 let bfs ~depth ~iter_succ f root =
+  let module NodeSet = Graph.Node.Set in
   let queue : (node * int) Queue.t = Queue.create () in
+  let marks = ref NodeSet.empty in
   Queue.add (root,0) queue;
   while not (Queue.is_empty queue) do
     let (n,d) = Queue.take queue in
-    if d < depth then begin
+    if not (NodeSet.mem n !marks) && d < depth then begin
+      marks := NodeSet.add n !marks;
       f n;
       iter_succ (fun n' -> Queue.add (n',d+1) queue) n
     end

src/plugins/dive/tests/dive/oracle/manydeps.dot

 digraph G {
   cp2 [label=<x>, shape=box, fillcolor="#AACCFF", color="#88AAFF",
-       style="filled,bold", ];
+       style="filled,dotted,bold", ];
   cp4 [label=<t14>, shape=box, fillcolor="#AACCFF", color="#88AAFF",
        style="filled", ];
   cp6 [label=<t13>, shape=box, fillcolor="#AACCFF", color="#88AAFF",
@@ -21,23 +21,15 @@ digraph G {
         style="filled", ];
   cp22 [label=<t6>, shape=box, fillcolor="#AACCFF", color="#88AAFF",
         style="filled", ];
-  cp24 [label=<t5>, shape=box, fillcolor="#AACCFF", color="#88AAFF",
-        style="filled", ];
-  cp26 [label=<t4>, shape=box, fillcolor="#AACCFF", color="#88AAFF",
-        style="filled", ];
-  cp28 [label=<t3>, shape=box, fillcolor="#AACCFF", color="#88AAFF",
-        style="filled", ];
-  cp30 [label=<t2>, shape=box, fillcolor="#AACCFF", color="#88AAFF",
-        style="filled", ];
-  cp32 [label=<__retres>, shape=box, style="bold", ];
-  cp33 [label=<*(pt[x])>, shape=parallelogram, fillcolor="#AACCFF",
+  cp24 [label=<__retres>, shape=box, style="bold", ];
+  cp25 [label=<*(pt[x])>, shape=parallelogram, fillcolor="#AACCFF",
         color="#88AAFF", style="filled,dotted", ];
   
   subgraph cluster_cs_1 { label=<many_writes>; cp2;
      };
-  subgraph cluster_cs_2 { label=<many_values>; cp33;cp32;
+  subgraph cluster_cs_2 { label=<many_values>; cp25;cp24;
      };
-  subgraph cluster_file_1 { label=<tests/dive/manydeps.i>; cp30;cp28;cp26;cp24;cp22;cp20;cp18;cp16;cp14;cp12;cp10;cp8;cp6;cp4;
+  subgraph cluster_file_1 { label=<tests/dive/manydeps.i>; cp22;cp20;cp18;cp16;cp14;cp12;cp10;cp8;cp6;cp4;
      };
   
   cp2 -> cp2 [style="bold", ];
@@ -46,15 +38,11 @@ digraph G {
   cp8 -> cp2;
   cp10 -> cp2;
   cp12 -> cp2;
-  cp14 -> cp2 [style="bold", ];
+  cp14 -> cp2;
   cp16 -> cp2;
   cp18 -> cp2;
   cp20 -> cp2;
   cp22 -> cp2;
-  cp24 -> cp2;
-  cp26 -> cp2;
-  cp28 -> cp2;
-  cp30 -> cp2;
-  cp33 -> cp32;
+  cp25 -> cp24;
   
   }
\ No newline at end of file