diff --git a/ivette/src/frama-c/plugins/region/api/index.ts b/ivette/src/frama-c/plugins/region/api/index.ts index a0b2fef89282dafb2469897c389922c546a54e65..122c71d9f6779139ce2900e322a7360e18e30c6d 100644 --- a/ivette/src/frama-c/plugins/region/api/index.ts +++ b/ivette/src/frama-c/plugins/region/api/index.ts @@ -149,7 +149,7 @@ const compute_internal: Server.ExecRequest<decl,null> = { output: Json.jNull, signals: [], }; -/** Compute region domain for the given declaration */ +/** Compute regions for the given declaration */ export const compute: Server.ExecRequest<decl,null>= compute_internal; const regions_internal: Server.GetRequest<decl,region[]> = { @@ -159,7 +159,7 @@ const regions_internal: Server.GetRequest<decl,region[]> = { output: Json.jArray(jRegion), signals: [ { name: 'plugins.region.updated' } ], }; -/** Compute regions for the given declaration */ +/** Returns computed regions for the given declaration */ export const regions: Server.GetRequest<decl,region[]>= regions_internal; const regionsAt_internal: Server.GetRequest<[ marker, boolean ],region[]> = { diff --git a/ivette/src/frama-c/plugins/region/memory.tsx b/ivette/src/frama-c/plugins/region/memory.tsx index 4b091613708dba177d8a9d489089d7cab920bf02..4e011695b5dc2c92ddcc710a994460501ac417f3 100644 --- a/ivette/src/frama-c/plugins/region/memory.tsx +++ b/ivette/src/frama-c/plugins/region/memory.tsx @@ -54,7 +54,12 @@ function makeRecord( return cells; } -function makeDiagram(regions: readonly Region.region[]): Dot.DiagramProps { +interface Diagram { + nodes: Dot.Node[] ; + edges: Dot.Edge[] ; +} + +function makeDiagram(regions: readonly Region.region[]): Diagram { const nodes: Dot.Node[] = []; const edges: Dot.Edge[] = []; regions.forEach(r => { @@ -87,12 +92,24 @@ function makeDiagram(regions: readonly Region.region[]): Dot.DiagramProps { return { nodes, edges }; } +function addSelected(d: Diagram, label: string, node: Region.node): void { + d.nodes.push({ + id: 'Selected', label, title: "Selected Marker", shape: 'note' + }); + d.edges.push({ source: 'Selected', target: `n${node}` }); +} + export interface MemoryViewProps { - regions: readonly Region.region[]; + regions?: readonly Region.region[]; + node?: Region.node | undefined; + label?: string; } export function MemoryView(props: MemoryViewProps): JSX.Element { - const { regions } = props; + const { regions=[], label, node } = props; const diagram = React.useMemo(() => makeDiagram(regions), [regions]); + if (label && node) addSelected(diagram, label, node); return <Dot.Diagram {...diagram} />; } + +// -------------------------------------------------------------------------- diff --git a/src/plugins/region/services.ml b/src/plugins/region/services.ml index d92e5850987d719e45010172f9f6795cf63aaf22..72d94683a11b1bc50491d6e844db9e6e5815bf2a 100644 --- a/src/plugins/region/services.ml +++ b/src/plugins/region/services.ml @@ -211,7 +211,7 @@ let () = Analysis.add_hook (fun () -> Request.emit signal) let () = Request.register ~package ~kind:`EXEC ~name:"compute" - ~descr:(Md.plain "Compute region domain for the given declaration") + ~descr:(Md.plain "Compute regions for the given declaration") ~input:(module Kernel_ast.Decl) ~output:(module Data.Junit) (function SFunction kf -> Analysis.compute kf | _ -> ()) @@ -219,7 +219,7 @@ let () = let () = Request.register ~package ~kind:`GET ~name:"regions" - ~descr:(Md.plain "Compute regions for the given declaration") + ~descr:(Md.plain "Returns computed regions for the given declaration") ~input:(module Kernel_ast.Decl) ~output:(module Regions) ~signals:[signal]