diff --git a/ivette/src/dome/renderer/dark.css b/ivette/src/dome/renderer/dark.css index 0660868825afc53f7e051a476f593e2d9c4d15f6..cbe9a2b73b54eb26904eb96adbb7a80fef9c2000 100644 --- a/ivette/src/dome/renderer/dark.css +++ b/ivette/src/dome/renderer/dark.css @@ -10,8 +10,8 @@ --code-hover: #005137; --code-select: #4f3d24; --code-select-hover: #5f4d34; - --dead-code: #444; - --non-terminating: #444; + --dead-code: #777; + --non-terminating: #d84954; --highlighted-marker: #778822; --code-bullet: #0a2234; diff --git a/ivette/src/dome/renderer/light.css b/ivette/src/dome/renderer/light.css index 0caf3fb0e549257228f9e19d34c17a8b73f51b34..135bd1ef348473c56143123b5e73d2b6cd9e5c82 100644 --- a/ivette/src/dome/renderer/light.css +++ b/ivette/src/dome/renderer/light.css @@ -10,8 +10,8 @@ --code-hover: lightgreen; --code-select: #ffda95; --code-select-hover: orange; - --dead-code: #bbb; - --non-terminating: #bbb; + --dead-code: #999; + --non-terminating: #fb4e4a; --highlighted-marker: #ffff66; --code-bullet: #ddd; diff --git a/ivette/src/dome/renderer/text/style.css b/ivette/src/dome/renderer/text/style.css index a299cc047c2f86f9defd7ed5d4fd6bce27577fa3..3b26fd8a537d41bdaa6ec097adc1eb648e4ce690 100644 --- a/ivette/src/dome/renderer/text/style.css +++ b/ivette/src/dome/renderer/text/style.css @@ -183,6 +183,12 @@ background: var(--code-bullet); } +.cm-deadcode-gutter { + width: 4px; + background: var(--code-bullet); + color: var(--dead-code); +} + .cm-hovered-code { background-color: var(--code-hover); } @@ -199,14 +205,12 @@ background-color: var(--highlighted-marker); } -.cm-dead-code { +:not(.cm-dead-code) > .cm-dead-code { font-style: italic; - filter: opacity(0.7); + filter: opacity(0.5); } .cm-non-term-code { - font-style: italic; - filter: opacity(0.7); } .cm-tainted { diff --git a/ivette/src/frama-c/kernel/ASTview.tsx b/ivette/src/frama-c/kernel/ASTview.tsx index c02f1b2fcf9b96ca3f33f2e400cee4112fe707c0..7dcbbef248889106cc029b7b5c279ef90eef41fe 100644 --- a/ivette/src/frama-c/kernel/ASTview.tsx +++ b/ivette/src/frama-c/kernel/ASTview.tsx @@ -322,18 +322,68 @@ function createMultipleDecorator(): Editor.Extension { const emptyDeadCode = { unreachable: [], nonTerminating: [] }; const Dead = Editor.createField<Eva.deadCode>(emptyDeadCode); +const UnreachableRanges = createUnreachableRanges(); +function createUnreachableRanges(): Editor.Aspect<Editor.Range[]> { + const deps = { dead: Dead, ranges: Ranges }; + return Editor.createAspect(deps, ({ dead, ranges }) => { + return mapFilter(dead.unreachable, m => ranges.get(m)).flat(); + }); +} + +const NonTerminatingRanges = createNonTerminatingRanges(); +function createNonTerminatingRanges(): Editor.Aspect<Editor.Range[]> { + const deps = { dead: Dead, ranges: Ranges }; + return Editor.createAspect(deps, ({ dead, ranges }) => { + return mapFilter(dead.nonTerminating, m => ranges.get(m)).flat(); + }); +} + const DeadCodeDecorator = createDeadCodeDecorator(); function createDeadCodeDecorator(): Editor.Extension { - const uClass = Editor.Decoration.mark({ class: 'cm-dead-code' }); - const tClass = Editor.Decoration.mark({ class: 'cm-non-term-code' }); - const deps = { dead: Dead, ranges: Ranges }; - return Editor.createDecorator(deps, ({ dead, ranges }) => { - const range = (m: string): Range[] | undefined => ranges.get(m); - const unreachableRanges = mapFilter(dead.unreachable, range).flat(); - const unreachable = unreachableRanges.map(r => uClass.range(r.from, r.to)); - const nonTermRanges = mapFilter(dead.nonTerminating, range).flat(); - const nonTerm = nonTermRanges.map(r => tClass.range(r.from, r.to)); - return Editor.RangeSet.of(unreachable.concat(nonTerm), true); + const uCls = Editor.Decoration.mark({ class: 'cm-dead-code' }); + const tCls = Editor.Decoration.mark({ class: 'cm-non-term-code' }); + const deps = { unreach: UnreachableRanges, nonTerm: NonTerminatingRanges }; + return Editor.createDecorator(deps, ({ unreach, nonTerm }) => { + const unreachable = unreach.map(r => uCls.range(r.from, r.to)); + const nonTerminating = nonTerm.map(r => tCls.range(r.from, r.to)); + return Editor.RangeSet.of(unreachable.concat(nonTerminating), true); + }); +} + +type DeadCodeKind = 'unreachable' | 'non terminating'; +class DeadCodeGutterMarker extends Editor.GutterMarker { + readonly element: HTMLDivElement; + toDOM(): HTMLDivElement { return this.element; } + constructor(kind: DeadCodeKind) { + super(); + const color = kind === 'unreachable' ? 'dead-code' : 'non-terminating'; + this.element = document.createElement('div'); + this.element.innerHTML = 'a'; + this.element.title = `This code is ${kind}`; + this.element.style.width = '4px'; + this.element.style.color = `var(--${color})`; + this.element.style.borderRight = `4px solid var(--${color})`; + } +} + +const DeadCodeGutter = createDeadCodeGutter(); +function createDeadCodeGutter(): Editor.Extension { + const deps = { unreach: UnreachableRanges, nonTerm: NonTerminatingRanges }; + const cls = 'cm-deadcode-gutter'; + return Editor.createGutter(deps, cls, (props, block, view) => { + const doc = view.state.doc; + const line = doc.lineAt(block.from); + const unreachable = props.unreach + .filter(r => r.from <= doc.length) + .map(r => ({ from: doc.lineAt(r.from).from, to: doc.lineAt(r.to).to })) + .find(r => r.from <= line.from && line.to <= r.to); + if (unreachable) return new DeadCodeGutterMarker('unreachable'); + const nonTerm = props.nonTerm + .filter(r => r.from <= doc.length) + .map(r => ({ from: doc.lineAt(r.from).from, to: doc.lineAt(r.to).to })) + .find(r => r.from <= line.from && line.to <= r.to); + if (nonTerm) return new DeadCodeGutterMarker('non terminating'); + return null; }); } @@ -641,6 +691,7 @@ const extensions: Editor.Extension[] = [ DeadCodeDecorator, ContextMenuHandler, PropertiesGutter, + DeadCodeGutter, TaintedLvaluesDecorator, TaintTooltip, Editor.ReadOnly,