From 7ec5db2dbbae1492aeb914aa6c3a37d0049481c4 Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?David=20B=C3=BChler?= <david.buhler@cea.fr>
Date: Tue, 3 Oct 2023 22:22:06 +0200
Subject: [PATCH] [Ivette] ASTview: minor change to the computation of
unreachable ranges.
---
ivette/src/dome/renderer/text/editor.tsx | 5 -----
ivette/src/frama-c/kernel/ASTview.tsx | 16 ++++++++++++----
2 files changed, 12 insertions(+), 9 deletions(-)
diff --git a/ivette/src/dome/renderer/text/editor.tsx b/ivette/src/dome/renderer/text/editor.tsx
index 094988c0656..45a5e4583af 100644
--- a/ivette/src/dome/renderer/text/editor.tsx
+++ b/ivette/src/dome/renderer/text/editor.tsx
@@ -55,11 +55,6 @@ export { RangeSet } from '@codemirror/state';
// Type definition.
export type Range = { from: number, to: number };
-// Comparison function
-export function compareRange(x: Range, y: Range): number {
- return (x.from !== y.from) ? (x.from - y.from) : (y.to - x.to);
-}
-
// Checks if the start of the range x belongs in y.
export function startInto(x: Range, y: Range): boolean {
return y.from <= x.from && x.from < y.to;
diff --git a/ivette/src/frama-c/kernel/ASTview.tsx b/ivette/src/frama-c/kernel/ASTview.tsx
index 7d8d6e34d10..ac867fed84a 100644
--- a/ivette/src/frama-c/kernel/ASTview.tsx
+++ b/ivette/src/frama-c/kernel/ASTview.tsx
@@ -325,16 +325,24 @@ function createMultipleDecorator(): Editor.Extension {
const emptyDeadCode = { reached: [], unreachable: [], nonTerminating: [] };
const Dead = Editor.createField<Eva.deadCode>(emptyDeadCode);
+// Comparison function on ranges
+export function compareRange(x: Range, y: Range): number {
+ return (x.from !== y.from) ? (x.from - y.from) : (y.to - x.to);
+}
+
// The unreachable statements given by the server may contain reachable
// statements. This function is used to filter those reached statements.
function filterReached(unreachables: Range[], reachables: Range[]): Range[] {
+ /* Sort [reachables] to always find the first largest reachable statement
+ within an unreachable one (if any). */
+ reachables.sort(compareRange);
function keepTrulyUnreached(unreached: Range): Range[] {
const reached = reachables.find((r) => Editor.startInto(r, unreached));
if (reached === undefined) return [unreached];
+ const firstUnreached = { from: unreached.from, to: reached.from - 1 };
const next = { from: reached.to + 1, to: unreached.to };
const result = (reached.to < unreached.to) ? keepTrulyUnreached(next) : [];
- const reallyUnreached = { from: unreached.from, to: reached.from - 1 };
- if (unreached.from < reached.from) result.unshift(reallyUnreached);
+ if (unreached.from < reached.from) result.unshift(firstUnreached);
return result;
}
return unreachables.map(keepTrulyUnreached).flat();
@@ -345,8 +353,8 @@ function createUnreachableRanges(): Editor.Aspect<Editor.Range[]> {
const deps = { dead: Dead, ranges: Ranges };
return Editor.createAspect(deps, ({ dead, ranges: rs }) => {
const get = (ms: Ast.marker[]): Range[][] => mapFilter(ms, m => rs.get(m));
- const unreachable = get(dead.unreachable).flat().sort(Editor.compareRange);
- const reached = get(dead.reached).flat().sort(Editor.compareRange);
+ const unreachable = get(dead.unreachable).flat();
+ const reached = get(dead.reached).flat();
return filterReached(unreachable, reached);
});
}
--
GitLab