[ivette] display three dots when all (backward) dependencies are not computed

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();

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"
     }

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

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) ;

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 ];