From cdc9862c619b50a4cbe3a397406f39082fa6b337 Mon Sep 17 00:00:00 2001
From: Valentin Perrelle <valentin.perrelle@cea.fr>
Date: Fri, 7 Oct 2022 18:00:15 +0200
Subject: [PATCH] [Ivette] dive: fix nodes range disapearing
---
ivette/src/frama-c/plugins/dive/index.tsx | 17 ++++++-----------
1 file changed, 6 insertions(+), 11 deletions(-)
diff --git a/ivette/src/frama-c/plugins/dive/index.tsx b/ivette/src/frama-c/plugins/dive/index.tsx
index ce655035adc..144288bb1c3 100644
--- a/ivette/src/frama-c/plugins/dive/index.tsx
+++ b/ivette/src/frama-c/plugins/dive/index.tsx
@@ -306,28 +306,23 @@ class Dive {
let newNodes = this.cy.collection();
for (const node of data.nodes) {
- let stops = undefined;
+ const data : { [k: string]: unknown } = { ...node};
if (typeof node.range === 'number')
- stops = `0% ${node.range}% ${node.range}% 100%`;
+ data.stops = `0% ${node.range}% ${node.range}% 100%`;
let ele = this.cy.$id(node.id.toString());
if (ele.nonempty()) {
ele.removeData();
- ele.data(node);
+ ele.data(data);
ele.neighborhood('edge').remove();
}
else {
- let parent = null;
if (node.locality.callstack)
- parent = this.referenceCallstack(node.locality.callstack)?.id();
+ data.parent = this.referenceCallstack(node.locality.callstack)?.id();
else
- parent = this.referenceFile(node.locality.file).id();
+ data.parent = this.referenceFile(node.locality.file).id();
- ele = this.cy.add({
- group: 'nodes',
- data: { ...(node as { [k: string]: unknown }), stops, parent },
- classes: 'new',
- });
+ ele = this.cy.add({group: 'nodes', data, classes: 'new'});
this.addTips(ele);
newNodes = ele.union(newNodes);
}
--
GitLab