diff --git a/ivette/src/dome/renderer/graph/diagram.tsx b/ivette/src/dome/renderer/graph/diagram.tsx index abc9c7bcf00f5cc8c97f80da3f0444fde2b54a67..ec0325a9dcc403b3da70add407567c299832114e 100644 --- a/ivette/src/dome/renderer/graph/diagram.tsx +++ b/ivette/src/dome/renderer/graph/diagram.tsx @@ -49,6 +49,9 @@ export type Shape = | 'circle' | 'ellipse' | 'note' | 'tab' | 'folder' | 'cds'; +export type Anchor = + 'n' | 'ne' | 'e' | 'se' | 's' | 'sw' | 'w' | 'nw' | 'c' | '_'; + export type Arrow = 'none' | 'arrow' | 'tee' | 'box' | 'dot'; export type Line = 'solid' | 'dashed' | 'dotted'; @@ -94,20 +97,19 @@ export interface Edge { line?: Line; /** Default is `dark` */ color?: Color; - /** Default is `arrow` */ head?: Arrow; - /** Default is `none` */ + headLabel?: string, + headAnchor?: Anchor; tail?: Arrow; - /** Label font */ + tailLabel?: string, + tailAnchor?: Anchor; font?: Font; - /** Label */ label?: string; - /** Tooltip */ title?: string; - /** Head label */ - headLabel?: string, - /** Tail label */ - tailLabel?: string, + /** Edge constraints node placement (default: true). */ + constraint?: boolean; + /** Node placement on the same rank (default: false). */ + aligned?: boolean; } export interface Cluster { @@ -319,7 +321,10 @@ class Builder { } attr(a: string, v: string | number | boolean | undefined): Builder { - return v ? this.print(' ', a, '=').value(v).print(';') : this; + if (v !== undefined && v !== '') + return this.print(' ', a, '=').value(v).print(';'); + else + return this; } // --- Node Table Shape @@ -405,6 +410,11 @@ class Builder { edge(e: Edge): void { const { line = 'solid', head = 'arrow', tail = 'none' } = e; const tooltip = e.title ?? e.label ?? `${e.source} -> ${e.target}`; + if (e.aligned === true) + this + .print('{ rank=same; ') + .port(e.source).print(' ') + .port(e.target).println(' };'); this .print(' ') .port(e.source, e.sourcePort) @@ -413,8 +423,11 @@ class Builder { .print(' [') .attr('label', e.label) .attr('fontname', e.font ? FONTNAME[e.font] : undefined) + .attr('headport', e.tailAnchor) + .attr('tailport', e.headAnchor) .attr('headlabel', e.headLabel) .attr('taillabel', e.tailLabel) + .attr('constraint', e.constraint === false ? false : undefined) .attr('labeltooltip', e.label ? tooltip : undefined) .attr('headtooltip', e.headLabel ? tooltip : undefined) .attr('tailtooltip', e.tailLabel ? tooltip : undefined) diff --git a/ivette/src/frama-c/plugins/region/index.tsx b/ivette/src/frama-c/plugins/region/index.tsx index 3bf4a449f4d090e5ca54729f46038ae513192bc3..d489e0a5a214626a7a8abb04af7c0346ff75207d 100644 --- a/ivette/src/frama-c/plugins/region/index.tsx +++ b/ivette/src/frama-c/plugins/region/index.tsx @@ -45,7 +45,8 @@ function RegionAnalys(): JSX.Element { const setComputing = Dome.useProtected(setRunning); const scope = States.useCurrentScope(); const { kind, name } = States.useDeclaration(scope); - const regions = States.useRequest(Region.regions, kf) ?? []; + const regions = + States.useRequest(Region.regions, kf, { pending: null }) ?? []; React.useEffect(() => { if (!pinned && kind === 'FUNCTION' && scope !== kf) { setKf(scope); diff --git a/ivette/src/frama-c/plugins/region/memory.tsx b/ivette/src/frama-c/plugins/region/memory.tsx index 29c9b5a634185fcc805c749f8be5421549a6dd6b..a59a4adac95021d3e17cd48d6e10cb0e9aceb15f 100644 --- a/ivette/src/frama-c/plugins/region/memory.tsx +++ b/ivette/src/frama-c/plugins/region/memory.tsx @@ -82,7 +82,7 @@ function makeDiagram(regions: readonly Region.region[]): Diagram { r.labels.forEach(a => { const lid = `L${a}`; nodes.push({ ...L, id: lid, label: `${a}:` }); - edges.push({ source: lid, target: id }); + edges.push({ source: lid, aligned: true, head: 'tee', target: id }); }); // --- Roots const R: Dot.Node = @@ -90,7 +90,7 @@ function makeDiagram(regions: readonly Region.region[]): Diagram { r.roots.forEach(x => { const xid = `X${x}`; nodes.push({ ...R, id: xid, label: x }); - edges.push({ source: xid, target: id }); + edges.push({ source: xid, headAnchor: "e", target: id }); }); // --- Pointed if (r.pointed !== undefined) {