diff --git a/ivette/src/frama-c/plugins/region/memory.tsx b/ivette/src/frama-c/plugins/region/memory.tsx index 4fe581665e39665e9de03e98b64b3c4ed7a22727..2b38fe1acbe532113a27f458bb0a43fe2a30c023 100644 --- a/ivette/src/frama-c/plugins/region/memory.tsx +++ b/ivette/src/frama-c/plugins/region/memory.tsx @@ -47,7 +47,11 @@ function makeRecord( if (offset !== rg.offset) cells.push(`#${rg.offset - offset}b`); offset = rg.offset + rg.length; - cells.push({ label: rg.label, port }); + const label = + rg.cells < 1 ? `${rg.label} […]` : + rg.cells > 1 ? `${rg.label} [${rg.cells}]` : + rg.label; + cells.push({ label, port }); }); if (offset !== sizeof) cells.push(`#${sizeof-offset}b`);