diff --git a/ivette/src/frama-c/plugins/region/api/index.ts b/ivette/src/frama-c/plugins/region/api/index.ts
index 5d01bdbe22ac529ecefaa43e5a11963c12441397..909a2221fa87d0fb8d0aae232e7a8d8ac64ffba8 100644
--- a/ivette/src/frama-c/plugins/region/api/index.ts
+++ b/ivette/src/frama-c/plugins/region/api/index.ts
@@ -166,34 +166,26 @@ const regions_internal: Server.GetRequest<decl,region[]> = {
/** Returns computed regions for the given declaration */
export const regions: Server.GetRequest<decl,region[]>= regions_internal;
-const regionsAt_internal: Server.GetRequest<[ marker, boolean ],region[]> = {
+const regionsAt_internal: Server.GetRequest<marker,region[]> = {
kind: Server.RqKind.GET,
name: 'plugins.region.regionsAt',
- input: Json.jPair( jMarker, Json.jBoolean,),
+ input: jMarker,
output: Json.jArray(jRegion),
fallback: [],
signals: [ { name: 'plugins.region.updated' } ],
};
-/** Compute regions at the given marker */
-export const regionsAt: Server.GetRequest<[ marker, boolean ],region[]>= regionsAt_internal;
-
-const localize_internal: Server.GetRequest<
- [ marker, boolean ],
- node |
- undefined
- > = {
+/** Compute regions at the given marker program point */
+export const regionsAt: Server.GetRequest<marker,region[]>= regionsAt_internal;
+
+const localize_internal: Server.GetRequest<marker,node | undefined> = {
kind: Server.RqKind.GET,
name: 'plugins.region.localize',
- input: Json.jPair( jMarker, Json.jBoolean,),
+ input: jMarker,
output: Json.jOption(jNode),
fallback: undefined,
signals: [ { name: 'plugins.region.updated' } ],
};
-/** Localize in the local (true) or global map (false) */
-export const localize: Server.GetRequest<
- [ marker, boolean ],
- node |
- undefined
- >= localize_internal;
+/** Localize the marker in its map */
+export const localize: Server.GetRequest<marker,node | undefined>= localize_internal;
/* ------------------------------------- */
diff --git a/ivette/src/frama-c/plugins/region/index.tsx b/ivette/src/frama-c/plugins/region/index.tsx
index eed8bea5b81bb105826aaab9a9c1e05b85593f5a..b5faa2a37f188475eda35a31e74a5f6aead76ef9 100644
--- a/ivette/src/frama-c/plugins/region/index.tsx
+++ b/ivette/src/frama-c/plugins/region/index.tsx
@@ -43,9 +43,11 @@ function RegionAnalys(): JSX.Element {
const [pinned, setPinned] = React.useState(false);
const [running, setRunning] = React.useState(false);
const setComputing = Dome.useProtected(setRunning);
- const scope = States.useCurrentScope();
+ const { scope, marker } = States.useCurrentLocation();
const { kind, name } = States.useDeclaration(scope);
const regions = States.useRequestStable(Region.regions, kf);
+ const node = States.useRequestStable(Region.localize, marker);
+ const { descr: label } = States.useMarker(marker);
React.useEffect(() => {
if (!pinned && kind === 'FUNCTION' && scope !== kf) {
setKf(scope);
@@ -84,7 +86,7 @@ function RegionAnalys(): JSX.Element {
onClick={() => setPinned(!pinned)}
/>
</Tools.ToolBar>
- <MemoryView regions={regions} />
+ <MemoryView regions={regions} node={node} label={label} />
</>
);
}
diff --git a/ivette/src/frama-c/plugins/region/memory.tsx b/ivette/src/frama-c/plugins/region/memory.tsx
index 2b00616c491b2acd6182cfcd7ad3454558dde8f9..055907b7d4a0be91078f7ae7f93d6ee5860b80f4 100644
--- a/ivette/src/frama-c/plugins/region/memory.tsx
+++ b/ivette/src/frama-c/plugins/region/memory.tsx
@@ -58,8 +58,8 @@ function makeRecord(
}
interface Diagram {
- nodes: Dot.Node[];
- edges: Dot.Edge[];
+ nodes: readonly Dot.Node[];
+ edges: readonly Dot.Edge[];
}
function makeDiagram(regions: readonly Region.region[]): Diagram {
@@ -110,11 +110,23 @@ function makeDiagram(regions: readonly Region.region[]): Diagram {
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}` });
+function addSelected(
+ diag: Diagram,
+ node: Region.node | undefined,
+ label: string | undefined
+): Diagram {
+ if (node && label) {
+ const nodes = diag.nodes.concat({
+ id: 'Selected', label, title: "Selected Marker",
+ shape: 'note', color: 'selected'
+ });
+ const edges = diag.edges.concat({
+ source: 'Selected', target: `n${node}`, aligned: true,
+ headAnchor: 's', tailAnchor: 'n',
+ });
+ return { nodes, edges };
+ } else
+ return diag;
}
export interface MemoryViewProps {
@@ -125,9 +137,12 @@ export interface MemoryViewProps {
export function MemoryView(props: MemoryViewProps): JSX.Element {
const { regions = [], label, node } = props;
- const diagram = React.useMemo(() => makeDiagram(regions), [regions]);
- if (label && node) addSelected(diagram, label, node);
- return <Dot.Diagram {...diagram} />;
+ const baseDiagram = React.useMemo(() => makeDiagram(regions), [regions]);
+ const fullDiagram = React.useMemo(
+ () => addSelected(baseDiagram, node, label),
+ [baseDiagram, node, label]
+ );
+ return <Dot.Diagram {...fullDiagram} />;
}
// --------------------------------------------------------------------------
diff --git a/src/plugins/region/services.ml b/src/plugins/region/services.ml
index 0b5ab56eeec696b105255e42145de87b0b25027d..0604d92fb7da910be943af31f5de4f4b8fb21cd7 100644
--- a/src/plugins/region/services.ml
+++ b/src/plugins/region/services.ml
@@ -181,13 +181,13 @@ module Regions = Data.Jlist(Region)
(* --- Server API --- *)
(* -------------------------------------------------------------------------- *)
-let map_of_localizable ~local (loc : Printer_tag.localizable) =
+let map_of_localizable ?(atStmt=false) (loc : Printer_tag.localizable) =
let open Printer_tag in
match kf_of_localizable loc with
| None -> raise Not_found
| Some kf ->
let domain = Analysis.find kf in
- if local then
+ if atStmt then
match ki_of_localizable loc with
| Kglobal -> domain.map
| Kstmt s -> Stmt.Map.find s domain.body
@@ -236,25 +236,25 @@ let () =
let () =
Request.register
~package ~kind:`GET ~name:"regionsAt"
- ~descr:(Md.plain "Compute regions at the given marker")
- ~input:(module Data.Jpair(Kernel_ast.Marker)(Data.Jbool))
+ ~descr:(Md.plain "Compute regions at the given marker program point")
+ ~input:(module Kernel_ast.Marker)
~output:(module Regions)
~signals:[signal]
- begin fun (loc,local) ->
- try Memory.regions @@ map_of_localizable ~local loc
+ begin fun loc ->
+ try Memory.regions @@ map_of_localizable ~atStmt:true loc
with Not_found -> []
end
let () =
Request.register
~package ~kind:`GET ~name:"localize"
- ~descr:(Md.plain "Localize in the local (true) or global map (false)")
- ~input:(module Data.Jpair(Kernel_ast.Marker)(Data.Jbool))
+ ~descr:(Md.plain "Localize the marker in its map")
+ ~input:(module Kernel_ast.Marker)
~output:(module NodeOpt)
~signals:[signal]
- begin fun (loc,local) ->
+ begin fun loc ->
try
- let map = map_of_localizable ~local loc in
+ let map = map_of_localizable loc in
region_of_localizable map loc
with Not_found -> None
end