diff --git a/ivette/src/frama-c/plugins/region/index.tsx b/ivette/src/frama-c/plugins/region/index.tsx index c733ef9e7d9a02bc8d7c855e971905eadef2b0a8..3bf4a449f4d090e5ca54729f46038ae513192bc3 100644 --- a/ivette/src/frama-c/plugins/region/index.tsx +++ b/ivette/src/frama-c/plugins/region/index.tsx @@ -42,7 +42,6 @@ function RegionAnalys(): JSX.Element { const [kfName, setName] = React.useState<string>(); const [pinned, setPinned] = React.useState(false); const [running, setRunning] = React.useState(false); - const [padding, setPadding] = React.useState(true); const setComputing = Dome.useProtected(setRunning); const scope = States.useCurrentScope(); const { kind, name } = States.useDeclaration(scope); @@ -84,15 +83,8 @@ function RegionAnalys(): JSX.Element { selected={pinned} onClick={() => setPinned(!pinned)} /> - <Tools.Filler /> - <Tools.Button - icon='ITEMS.LIST' - title='Show non-accessed ranges in compounds' - selected={padding} - onClick={() => setPadding(!padding)} - /> </Tools.ToolBar> - <MemoryView padding={padding} regions={regions} /> + <MemoryView regions={regions} /> </> ); } diff --git a/ivette/src/frama-c/plugins/region/memory.tsx b/ivette/src/frama-c/plugins/region/memory.tsx index 67336ef18aeee9d2b536af6fc50360b47de5cb54..4b091613708dba177d8a9d489089d7cab920bf02 100644 --- a/ivette/src/frama-c/plugins/region/memory.tsx +++ b/ivette/src/frama-c/plugins/region/memory.tsx @@ -32,7 +32,6 @@ function makeRecord( edges: Dot.Edge[], source: string, sizeof: number, - padding: boolean, ranges: Region.range[] ): Dot.Cell[] { if (ranges.length === 0) return []; @@ -42,23 +41,20 @@ function makeRecord( const port = `r${i}`; const target = `n${rg.data}`; edges.push({ source, sourcePort: port, target }); - if (padding && offset !== rg.offset) - cells.push(`${offset}..${rg.offset-1} ##`); + if (offset !== rg.offset) + cells.push(`${offset}..${rg.offset - 1} ##`); offset = rg.offset + rg.length; cells.push({ label: `${rg.offset}..${offset - 1} [${rg.cells}]`, port, }); }); - if (padding && offset !== sizeof) - cells.push(`${offset}..${sizeof-1} ##`); + if (offset !== sizeof) + cells.push(`${offset}..${sizeof - 1} ##`); return cells; } -function makeDiagram( - regions: readonly Region.region[], - padding: boolean, -): Dot.DiagramProps { +function makeDiagram(regions: readonly Region.region[]): Dot.DiagramProps { const nodes: Dot.Node[] = []; const edges: Dot.Edge[] = []; regions.forEach(r => { @@ -71,13 +67,15 @@ function makeDiagram( : (r.writes && r.reads) ? 'green' : r.writes ? 'pink' : r.reads ? 'grey' : 'white'; // --- Shape - const cells = makeRecord(edges, id, r.sizeof, padding, r.ranges); + const font = r.ranges.length > 0 ? 'mono' : 'sans'; + const cells = makeRecord(edges, id, r.sizeof, r.ranges); const shape = cells.length > 0 ? cells : undefined; - nodes.push({ id: id, color, label: r.label, title: r.title, shape }); + nodes.push({ id, font, color, label: r.label, title: r.title, shape }); // --- Roots + const R: Dot.Node = { id: '', shape: 'cds', font: 'mono', color: 'blue' }; r.roots.forEach(x => { const xid = `X${x}`; - nodes.push({ id: xid, label: x, shape: 'folder', color: 'blue' }); + nodes.push({ ...R, id: xid, label: x }); edges.push({ source: xid, target: id }); }); // --- Pointed @@ -91,14 +89,10 @@ function makeDiagram( export interface MemoryViewProps { regions: readonly Region.region[]; - padding?: boolean; } export function MemoryView(props: MemoryViewProps): JSX.Element { - const { regions, padding=true } = props; - const diagram = React.useMemo( - () => makeDiagram(regions, padding), - [regions, padding] - ); + const { regions } = props; + const diagram = React.useMemo(() => makeDiagram(regions), [regions]); return <Dot.Diagram {...diagram} />; } diff --git a/src/plugins/region/services.ml b/src/plugins/region/services.ml index c8b31e72d36f586f32673ce7b2b6baef761b5456..38550cc6615d9f10c3a59337a2274af002c242bf 100644 --- a/src/plugins/region/services.ml +++ b/src/plugins/region/services.ml @@ -112,7 +112,11 @@ struct if m.writes <> [] then Buffer.add_char buffer 'W' ; if m.pointed <> None then Buffer.add_char buffer '*' else if m.reads <> [] || m.writes <> [] then - Buffer.add_char buffer @@ typs_to_char m.types ; + begin + Buffer.add_char buffer '(' ; + Buffer.add_char buffer @@ typs_to_char m.types ; + Buffer.add_char buffer ')' ; + end ; Buffer.contents buffer let pp_typ_layout s0 fmt ty =