From aa4cb35c49c72aa38c29883bf6c236748dc53078 Mon Sep 17 00:00:00 2001
From: Valentin Perrelle <valentin.perrelle@cea.fr>
Date: Sat, 25 Jul 2020 14:27:29 +0200
Subject: [PATCH] [dive] offset exploration range by 1 to be more consistent
---
ivette/src/frama-c/dive/Dive.tsx | 4 ++--
src/plugins/dive/build.ml | 20 +++++++++-----------
src/plugins/dive/self.ml | 2 +-
src/plugins/dive/server_interface.ml | 13 +++++++++----
src/plugins/dive/tests/dive/const.i | 2 +-
src/plugins/dive/tests/dive/pointed_param.i | 2 +-
6 files changed, 23 insertions(+), 20 deletions(-)
diff --git a/ivette/src/frama-c/dive/Dive.tsx b/ivette/src/frama-c/dive/Dive.tsx
index 6a968c76708..3f8c31dd406 100644
--- a/ivette/src/frama-c/dive/Dive.tsx
+++ b/ivette/src/frama-c/dive/Dive.tsx
@@ -377,13 +377,13 @@ class Dive {
switch (this.mode) {
case 'explore':
await Dive.setWindow({
- perception: { backward: 2, forward: 0 },
+ perception: { backward: 3, forward: 1 },
horizon: { backward: 3, forward: 1 },
});
break;
case 'overview':
await Dive.setWindow({
- perception: { backward: 3, forward: 0 },
+ perception: { backward: 4, forward: 1 },
horizon: { backward: null, forward: null },
});
break;
diff --git a/src/plugins/dive/build.ml b/src/plugins/dive/build.ml
index 8480a441870..b621e26021a 100644
--- a/src/plugins/dive/build.ml
+++ b/src/plugins/dive/build.ml
@@ -667,24 +667,25 @@ let bfs ~depth ~iter_succ f root =
Queue.add (root,0) queue;
while not (Queue.is_empty queue) do
let (n,d) = Queue.take queue in
- f n d;
- if d < depth then
+ if d < depth then begin
+ f n;
iter_succ (fun n' -> Queue.add (n',d+1) queue) n
+ end
done
let explore_backward ~depth context root =
context.graph_diff <- { context.graph_diff with last_root = Some root };
let iter_succ f n = Graph.iter_pred f context.graph n
- and explore_node n d =
- if n.node_writes_computation <> Done && (should_explore n || d <= 0) then
+ and explore_node n =
+ if n.node_writes_computation <> Done && should_explore n then
build_node_writes context n
in
bfs ~depth ~iter_succ explore_node root
let explore_forward ~depth context root =
let iter_succ f n = Graph.iter_succ f context.graph n
- and explore_node n d =
- if n.node_reads_computation <> Done && (should_explore n || d <= 0) then
+ and explore_node n =
+ if n.node_reads_computation <> Done && should_explore n then
build_node_reads context n;
in
bfs ~depth ~iter_succ explore_node root
@@ -777,11 +778,8 @@ let reduce_to_horizon ({ graph } as context) range new_root =
in
Graph.iter_vertex update graph
-let show context node =
- if node.node_hidden then begin
- node.node_hidden <- false;
- explore_backward ~depth:0 context node
- end
+let show _context node =
+ node.node_hidden <- false
let hide context node =
if not node.node_hidden then begin
diff --git a/src/plugins/dive/self.ml b/src/plugins/dive/self.ml
index 75bc7d1cce2..e83c8f924e3 100644
--- a/src/plugins/dive/self.ml
+++ b/src/plugins/dive/self.ml
@@ -48,7 +48,7 @@ module DepthLimit = Int
let option_name = "-dive-depth-limit"
let help = "Build dependencies up to a depth of N."
let arg_name = "N"
- let default = 2
+ let default = 3
end)
module FromFunctionAlarms = Kernel_function_set
diff --git a/src/plugins/dive/server_interface.ml b/src/plugins/dive/server_interface.ml
index 826b52e8d66..b17d0b267f3 100644
--- a/src/plugins/dive/server_interface.ml
+++ b/src/plugins/dive/server_interface.ml
@@ -44,7 +44,7 @@ let get_context =
let global_window = ref {
- perception = { backward = Some 2 ; forward = Some 0 };
+ perception = { backward = Some 2 ; forward = Some 1 };
horizon = { backward = None ; forward = None };
}
@@ -238,6 +238,9 @@ end
(* --- Actions --- *)
(* -------------------------------------------------------------------------- *)
+let result context =
+ Build.get_graph context, Build.take_last_differences context
+
let finalize' context node_opt =
begin match node_opt with
| None -> ()
@@ -253,7 +256,7 @@ let finalize' context node_opt =
then
Build.reduce_to_horizon context horizon node
end;
- Build.get_graph context, Build.take_last_differences context
+ result context
let finalize context node =
finalize' context (Some node)
@@ -291,6 +294,7 @@ let () = Request.register ~package
~input:(module NodeId) ~output:(module GraphDiff)
begin fun node ->
let context = get_context () in
+ Build.show context node;
finalize context node
end
@@ -301,7 +305,8 @@ let () = Request.register ~package
begin fun node ->
let context = get_context () in
Build.show context node;
- finalize context node
+ Build.explore_backward ~depth:1 context node;
+ result context
end
let () = Request.register ~package
@@ -311,5 +316,5 @@ let () = Request.register ~package
begin fun node ->
let context = get_context () in
Build.hide context node;
- finalize' context None
+ result context
end
diff --git a/src/plugins/dive/tests/dive/const.i b/src/plugins/dive/tests/dive/const.i
index 7001746bea3..622693ee684 100644
--- a/src/plugins/dive/tests/dive/const.i
+++ b/src/plugins/dive/tests/dive/const.i
@@ -1,5 +1,5 @@
/* run.config
-STDOPT: +"-dive-from-variables main::res -dive-depth-limit 4"
+STDOPT: +"-dive-from-variables main::res -dive-depth-limit 5"
*/
int f(int x, int y)
diff --git a/src/plugins/dive/tests/dive/pointed_param.i b/src/plugins/dive/tests/dive/pointed_param.i
index e6bd4f47db0..197ef953ebf 100644
--- a/src/plugins/dive/tests/dive/pointed_param.i
+++ b/src/plugins/dive/tests/dive/pointed_param.i
@@ -1,5 +1,5 @@
/* run.config
-STDOPT: +"-dive-from-variables main::y -dive-depth-limit 5"
+STDOPT: +"-dive-from-variables main::y -dive-depth-limit 6"
*/
float h(float *p)
--
GitLab