From a052353965e8b9d7eb0e582a31ab2762c1037c1f Mon Sep 17 00:00:00 2001
From: Maxime Jacquemin <maxime.jacquemin@cea.fr>
Date: Tue, 3 Oct 2023 13:51:21 +0200
Subject: [PATCH] [Ivette] Minor modification
Tried to make the code cleaner and clearer.
---
ivette/src/dome/renderer/text/editor.tsx | 22 +++++++++++-
ivette/src/frama-c/kernel/ASTview.tsx | 36 +++++++++----------
src/plugins/eva/api/general_requests.ml | 46 +++++++++++-------------
3 files changed, 59 insertions(+), 45 deletions(-)
diff --git a/ivette/src/dome/renderer/text/editor.tsx b/ivette/src/dome/renderer/text/editor.tsx
index ea59f699394..094988c0656 100644
--- a/ivette/src/dome/renderer/text/editor.tsx
+++ b/ivette/src/dome/renderer/text/editor.tsx
@@ -48,13 +48,33 @@ export { RangeSet } from '@codemirror/state';
+// -----------------------------------------------------------------------------
+// Ranges definition and interface
+// -----------------------------------------------------------------------------
+
+// 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;
+}
+
+// -----------------------------------------------------------------------------
+
+
+
// -----------------------------------------------------------------------------
// CodeMirror state's extensions types definitions
// -----------------------------------------------------------------------------
// Helper types definitions.
export type View = EditorView | null;
-export type Range = { from: number, to: number };
export type Set<A> = (view: View, value: A) => void;
export type Get<A> = (state: EditorState | undefined) => A;
export type IsUpdated = (update: ViewUpdate) => boolean;
diff --git a/ivette/src/frama-c/kernel/ASTview.tsx b/ivette/src/frama-c/kernel/ASTview.tsx
index 531e0bee723..7d8d6e34d10 100644
--- a/ivette/src/frama-c/kernel/ASTview.tsx
+++ b/ivette/src/frama-c/kernel/ASTview.tsx
@@ -325,31 +325,29 @@ function createMultipleDecorator(): Editor.Extension {
const emptyDeadCode = { reached: [], unreachable: [], nonTerminating: [] };
const Dead = Editor.createField<Eva.deadCode>(emptyDeadCode);
-function diffRanges(a: Editor.Range[], b: Editor.Range[]): Editor.Range[] {
- const cmp = (x: Editor.Range, y: Editor.Range): number => {
- return (x.from !== y.from) ? (x.from - y.from) : (y.to - x.to);
- };
- a.sort(cmp);
- b.sort(cmp);
- function split(x: Editor.Range): Editor.Range[] {
- const y = b.find((r) => r.from >= x.from && r.from < x.to);
- if (y === undefined) return [x];
- const t = [];
- if (x.from < y.from) t.push({ from: x.from, to: y.from - 1 });
- if (y.to < x.to) return t.concat(split({ from: y.to + 1, to: x.to }));
- return t;
+// 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[] {
+ function keepTrulyUnreached(unreached: Range): Range[] {
+ const reached = reachables.find((r) => Editor.startInto(r, unreached));
+ if (reached === undefined) return [unreached];
+ 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);
+ return result;
}
- return a.flatMap(split);
+ return unreachables.map(keepTrulyUnreached).flat();
}
const UnreachableRanges = createUnreachableRanges();
function createUnreachableRanges(): Editor.Aspect<Editor.Range[]> {
const deps = { dead: Dead, ranges: Ranges };
- return Editor.createAspect(deps, ({ dead, ranges }) => {
- const unreachable = mapFilter(dead.unreachable, m => ranges.get(m)).flat();
- const reached = mapFilter(dead.reached, m => ranges.get(m)).flat();
- const r = diffRanges(unreachable, reached);
- return r;
+ 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);
+ return filterReached(unreachable, reached);
});
}
diff --git a/src/plugins/eva/api/general_requests.ml b/src/plugins/eva/api/general_requests.ml
index edfea51036a..76c68cd47ab 100644
--- a/src/plugins/eva/api/general_requests.ml
+++ b/src/plugins/eva/api/general_requests.ml
@@ -168,8 +168,8 @@ module DeadCode = struct
let jtype = R.jtype
let to_json (dead_code) =
- let make_stmt stmt = Printer_tag.PStmt (dead_code.kf, stmt)
- and make_non_term stmt = Printer_tag.PStmtStart (dead_code.kf, stmt) in
+ let make_stmt stmt = Printer_tag.PStmt (dead_code.kf, stmt) in
+ let make_non_term stmt = Printer_tag.PStmtStart (dead_code.kf, stmt) in
R.default |>
R.set reached (List.map make_stmt dead_code.reached) |>
R.set unreachable (List.map make_stmt dead_code.unreachable) |>
@@ -177,30 +177,26 @@ module DeadCode = struct
R.to_json
end
+let all_statements kf =
+ try (Kernel_function.get_definition kf).sallstmts
+ with Kernel_function.No_Definition -> []
+
let dead_code kf =
- let empty =
- { kf; reached = []; unreachable = []; non_terminating = []; }
- in
- if Analysis.is_computed ()
- then
- try
- let fundec = Kernel_function.get_definition kf in
- match Analysis.status kf with
- | Unreachable | SpecUsed | Builtin _ ->
- { empty with unreachable = fundec.sallstmts; }
- | Analyzed NoResults -> empty
- | Analyzed (Partial | Complete) ->
- let classify acc stmt =
- if Results.(before stmt |> is_empty)
- then { acc with unreachable = stmt :: acc.unreachable }
- else
- let acc = { acc with reached = stmt :: acc.reached } in
- if Results.(after stmt |> is_empty)
- then { acc with non_terminating = stmt :: acc.non_terminating }
- else acc
- in
- List.fold_left classify empty fundec.sallstmts
- with Kernel_function.No_Definition -> empty
+ let empty = { kf ; reached = [] ; unreachable = [] ; non_terminating = [] } in
+ if Analysis.is_computed () then
+ let body = all_statements kf in
+ match Analysis.status kf with
+ | Unreachable | SpecUsed | Builtin _ -> { empty with unreachable = body }
+ | Analyzed NoResults -> empty
+ | Analyzed (Partial | Complete) ->
+ let classify { kf ; reached ; unreachable ; non_terminating = nt } stmt =
+ let before = Results.(before stmt |> is_empty) in
+ let after = Results.(after stmt |> is_empty) in
+ let unreachable = if before then stmt :: unreachable else unreachable in
+ let reached = if not before then stmt :: reached else reached in
+ let non_terminating = if not before && after then stmt :: nt else nt in
+ { kf ; reached ; unreachable ; non_terminating }
+ in List.fold_left classify empty body
else empty
let () = Request.register ~package
--
GitLab