diff --git a/ivette/src/frama-c/dive/Dive.tsx b/ivette/src/frama-c/dive/Dive.tsx index ffefe26a194928af95f2d173d13478978a02fe60..7f86636c5b8b9e313a349fdb577eefae766aa315 100644 --- a/ivette/src/frama-c/dive/Dive.tsx +++ b/ivette/src/frama-c/dive/Dive.tsx @@ -243,11 +243,11 @@ class Dive { if (typeof node.range === 'number') node.stops = `0% ${node.range}% ${node.range}% 100%`; - const previous = this.cy.$id(node.id); - if (previous.nonempty()) { - previous.removeData(); - previous.data(node); - previous.neighborhood('edge').remove(); + let ele = this.cy.$id(node.id); + if (ele.nonempty()) { + ele.removeData(); + ele.data(node); + ele.neighborhood('edge').remove(); } else { let parent = null; @@ -256,9 +256,25 @@ class Dive { else parent = this.referenceFile(node.locality.file).id(); - const ele = this.cy.add({ data: { ...node, parent } }); + ele = this.cy.add({ group: 'nodes', data: { ...node, parent } }); this.addTips(ele); - newEles = this.cy.add(ele).union(newEles); + newEles = ele.union(newEles); + } + + // Add a node for the user to ask for more dependencies + const idmore = `${node.id}-more`; + this.cy.remove(`#${idmore}`); + if (node.backward_explored === 'partial') { + let elemore = this.cy.add({ + group: 'nodes', + data: { id: idmore, parent: ele.data('parent') }, + classes: ['more'] }); + newEles = elemore.union(newEles); + let depmore = this.cy.add({ + group: 'edges', + data: { source: idmore, target: node.id } + }); + newEles = this.cy.add(depmore).union(newEles); } } @@ -400,7 +416,7 @@ class Dive { this.currentSelection = writes[index + 1 in writes ? index + 1 : 0]; const hasOrigin = (ele: Cytoscape.NodeSingular) => ( - ele.data().origins.includes(this.currentSelection) + ele.data().origins?.includes(this.currentSelection) ); node.select(); diff --git a/ivette/src/frama-c/dive/style.json b/ivette/src/frama-c/dive/style.json index f1e63e8835d5561c3ea0f2bdbc32a93bc03f380b..9cc4e1f03b470741af3df8d11b8b99b43140da7e 100644 --- a/ivette/src/frama-c/dive/style.json +++ b/ivette/src/frama-c/dive/style.json @@ -36,6 +36,16 @@ "selector": "node[label]", "style": { "label": "data(label)" + + } + }, + { + "selector": "node.more", + "style": { + "background-opacity": 0, + "label": "...", + "padding" : "0", + "border-width": 0 } }, { @@ -122,7 +132,7 @@ } }, { - "selector": "node[kind][!explored]", + "selector": "node[kind][backward_explored='no']", "style": { "opacity" : "0.3" } diff --git a/src/plugins/dive/build.ml b/src/plugins/dive/build.ml index 92a3ff2e6081271441e87b3f0206219a3c6aa30d..18cbfb50a29fd0d8a98ba338d8c7b960a59ce1b7 100644 --- a/src/plugins/dive/build.ml +++ b/src/plugins/dive/build.ml @@ -467,7 +467,7 @@ let build_node_writes context node = Graph.create_dependency context.graph kinstr dst kind node in List.iter add_dep nodes; - if complete then Done else NotDone + if complete then Done else Partial [] in let callstack = node.node_locality.loc_callstack in diff --git a/src/plugins/dive/dive_graph.ml b/src/plugins/dive/dive_graph.ml index ec524bd1872e45b6a654e2d817b23470fcccd04d..7805c5325996cd6c651cedf0dd134b0440231b6f 100644 --- a/src/plugins/dive/dive_graph.ml +++ b/src/plugins/dive/dive_graph.ml @@ -306,6 +306,11 @@ struct | Some cvalue when Cvalue.V.is_bottom cvalue -> `Null | Some cvalue -> `String (Pretty_utils.to_string Cvalue.V.pretty cvalue) + let output_computation = function + | Done -> `String "yes" + | Partial _ -> `String "partial" + | NotDone -> `String "no" + let output_node node = let label = Pretty_utils.to_string Node_kind.pretty node.node_kind in `Assoc ([ @@ -313,7 +318,8 @@ struct ("label", `String label) ; ("kind", output_node_kind node.node_kind) ; ("locality", output_node_locality node.node_locality) ; - ("explored", `Bool (node.node_writes_computation = Done)) ; + ("backward_explored", output_computation node.node_writes_computation) ; + ("forward_explored", output_computation node.node_reads_computation) ; ("writes", `List (List.map output_stmt node.node_writes_stmts)) ; ("values", output_node_values node.node_values) ; ("range", output_range node.node_range) ; diff --git a/src/plugins/dive/server_interface.ml b/src/plugins/dive/server_interface.ml index af50ee49d3abb88cada025e22092cbaa07e48ba4..f0c1048067cc938c88fce1aca596eb1665da9fda 100644 --- a/src/plugins/dive/server_interface.ml +++ b/src/plugins/dive/server_interface.ml @@ -199,7 +199,8 @@ struct "label", Syntax.string; "kind", Syntax.string; "locality", NodeLocality.syntax; - "explored", Syntax.boolean; + "backward_explored", Syntax.string; + "forward_explored", Syntax.string; "writes", Syntax.array Kernel_ast.Marker.syntax; "values", Syntax.option Syntax.string; "range", Syntax.union [ Syntax.string ; Syntax.int ];