diff --git a/ivette/src/frama-c/dive/Dive.tsx b/ivette/src/frama-c/dive/Dive.tsx index 6a968c76708f309bd2a78a6b9e615b1ba1cf9e08..3f8c31dd406812c80124fade9ae33646544f1be3 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 8480a4418709954d658728b7b27bd9b3040096a5..b621e26021a7286590d1caf62b8a4f42a136c4f6 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 75bc7d1cce238aad412ea6d2bb83842f8b65b297..e83c8f924e328e0ab973b79770def00fff504f1a 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 826b52e8d663f04ff3c7d421edabcabe75923ee6..b17d0b267f3640caadc63d692e3e03342862fbf8 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 7001746bea33cc57f5d2f0d0a678118be3606e08..622693ee684b1587bd5092c255096d84527beee3 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 e6bd4f47db024a2e99baa09be7a14905108f0fe2..197ef953ebf268f3e89ab473fe4ee3616f25f0cc 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)