diff --git a/src/plugins/dive/build.ml b/src/plugins/dive/build.ml index b737adb26e8afba58933e6e7b7e761e96430052a..7753090c4a029d7f3029e05c601970cce5299abd 100644 --- a/src/plugins/dive/build.ml +++ b/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 diff --git a/src/plugins/dive/tests/dive/oracle/manydeps.dot b/src/plugins/dive/tests/dive/oracle/manydeps.dot index 7a7b73389b9ad1670245d843d14906cc6c1468e5..88e1b23c12dd0692aca2aca454387139eeec13d9 100644 --- a/src/plugins/dive/tests/dive/oracle/manydeps.dot +++ b/src/plugins/dive/tests/dive/oracle/manydeps.dot @@ -1,6 +1,6 @@ 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