[Ivette] Minor modification

Tried to make the code cleaner and clearer.

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;

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

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