diff --git a/ivette/src/dome/renderer/frame/sidebars.tsx b/ivette/src/dome/renderer/frame/sidebars.tsx
index d205584d258d93a9aa54150a84ddbe81f27fb434..f7b332affdf2e55298907c528465e9bbbf934171 100644
--- a/ivette/src/dome/renderer/frame/sidebars.tsx
+++ b/ivette/src/dome/renderer/frame/sidebars.tsx
@@ -34,7 +34,7 @@ import { useFlipSettings } from 'dome';
import { Badge } from 'dome/controls/icons';
import { Label } from 'dome/controls/labels';
import { classes } from 'dome/misc/utils';
-import { Hbox, Hfill } from 'dome/layout/boxes';
+import { Hbox } from 'dome/layout/boxes';
import { IconButton, IconButtonProps } from 'dome/controls/buttons';
import './style.css';
@@ -110,6 +110,8 @@ export interface SectionProps {
disabled?: boolean;
/** Badge summary (only visible when folded). */
summary?: Badges;
+ /** Additional label, right-aligned. */
+ infos?: string;
/** Additional controls, (only visible when unfolded). */
rightButtonProps?: IconButtonProps;
/** Section contents. */
@@ -129,7 +131,7 @@ export interface SectionProps {
Sections with no items are not displayed.
*/
export function Section(props: SectionProps): JSX.Element | null {
- const { settings, defaultUnfold, unfold } = props;
+ const { settings, defaultUnfold, infos, unfold } = props;
const [state, flipState] = useFlipSettings(settings, defaultUnfold);
const icon = state ? 'TRIANGLE.DOWN' : 'TRIANGLE.RIGHT';
@@ -152,7 +154,7 @@ export function Section(props: SectionProps): JSX.Element | null {
icon={icon}
onClick={flipState}
/>
- <Hfill />
+ {infos && <div className='dome-xSideBarSection-infos'>{infos}</div>}
{visible ? rightButton : makeBadge(props.summary)}
</Hbox>
<div className='dome-xSideBarSection-content' style={{ maxHeight }}>
diff --git a/ivette/src/dome/renderer/frame/style.css b/ivette/src/dome/renderer/frame/style.css
index 73c306f4befbc3bba44117f08bc50efa35f17777..6ee566c0a2684df21fb5c9704a0d216e157a29f9 100644
--- a/ivette/src/dome/renderer/frame/style.css
+++ b/ivette/src/dome/renderer/frame/style.css
@@ -129,9 +129,17 @@
flex: 0 0 ;
}
+.dome-xSideBarSection-infos {
+ font-size: smaller;
+ color: var(--info-text-discrete);
+ padding-left: 4px;
+ padding-right: 4px;
+ display: block;
+}
+
.dome-xSideBarSection-filterButton {
margin: 0px;
- padding: 0px;
+ padding: 3px;
}
.dome-xSideBarSection-hideshow {
@@ -162,14 +170,6 @@
display: flex;
}
-.dome-xSideBarSection-info {
- color: var(--info-text-discrete);
- font-style: italic;
- padding-left: 20px;
- padding-right: 10px;
- display: block;
-}
-
/* -------------------------------------------------------------------------- */
/* --- SideBar Items --- */
/* -------------------------------------------------------------------------- */
diff --git a/ivette/src/frama-c/kernel/Globals.tsx b/ivette/src/frama-c/kernel/Globals.tsx
index 582875e68f93ec393c1b83c06cd1442d90202be2..88b47f820ed8ad20431d1fdae5141e3ab1722829 100644
--- a/ivette/src/frama-c/kernel/Globals.tsx
+++ b/ivette/src/frama-c/kernel/Globals.tsx
@@ -257,15 +257,15 @@ export default function Globals(): JSX.Element {
const noFunction =
<div className='dome-xSideBarSection-content'>
- <label className='dome-xSideBarSection-info'>
- {'There is no function to display.'}
+ <label className='globals-info'>
+ There is no function to display.
</label>
</div>;
const allFiltered =
<div className='dome-xSideBarSection-content'>
- <label className='dome-xSideBarSection-info'>
- {'All functions are filtered. Try adjusting function filters.'}
+ <label className='globals-info'>
+ All functions are filtered. Try adjusting function filters.
</label>
<Button {...filterButtonProps} label='Functions filters' />
</div>;
diff --git a/ivette/src/frama-c/kernel/Properties.tsx b/ivette/src/frama-c/kernel/Properties.tsx
index 476cb53b1d048dafa7efb1e76d457d081c8b5bd4..0b2bd023257d68cf2b6e7c66daa9e36fe0d845f9 100644
--- a/ivette/src/frama-c/kernel/Properties.tsx
+++ b/ivette/src/frama-c/kernel/Properties.tsx
@@ -38,7 +38,8 @@ import * as Models from 'dome/table/models';
import * as Arrays from 'dome/table/arrays';
import { Table, Column, ColumnProps, Renderer } from 'dome/table/views';
import { TitleBar } from 'ivette';
-import { Scroll, Folder } from 'dome/layout/boxes';
+import { Scroll } from 'dome/layout/boxes';
+import { Section } from 'dome/frame/sidebars';
import { RSplit } from 'dome/layout/splitters';
@@ -81,8 +82,8 @@ const DEFAULTS: { [key: string]: boolean } = {
'kind.axiomatic': true,
'kind.pragma': true,
'kind.others': true,
- 'alarms.alarms': true, // show properties that are alarms
- 'alarms.others': true, // show properties that are not alarms
+ 'source.alarms': true, // show properties that are alarms
+ 'source.others': true, // show properties that are not alarms
'alarms.overflow': true,
'alarms.division_by_zero': true,
'alarms.mem_access': true,
@@ -121,6 +122,31 @@ function useFilter(path: string): [boolean, () => void] {
);
}
+function resetFilters(prefix: string, b?: boolean) : void {
+ for (const key in DEFAULTS) {
+ if (key.startsWith(prefix)) {
+ const target = b ?? DEFAULTS[key];
+ const path = `ivette.properties.filter.${key}`;
+ Settings.setWindowSettings(path, target);
+ }
+ }
+ Reload.emit();
+}
+
+function filterSummary(prefix: string) : string {
+ let total = 0;
+ let enabled = 0;
+ for (const key in DEFAULTS) {
+ if (key.startsWith(prefix)) {
+ total ++;
+ if (filter(key)) enabled++;
+ }
+ }
+ if (enabled === 0) return 'none';
+ if (enabled === total) return 'all';
+ return `${enabled} / ${total}`;
+}
+
function filterStatus(
status: Properties.propStatus,
): boolean {
@@ -174,7 +200,7 @@ function filterKind(
function filterAlarm(alarm: string | undefined): boolean {
if (alarm) {
- if (!filter('alarms.alarms')) return false;
+ if (!filter('source.alarms')) return false;
switch (alarm) {
case 'overflow': return filter('alarms.overflow');
case 'division_by_zero': return filter('alarms.division_by_zero');
@@ -196,7 +222,7 @@ function filterAlarm(alarm: string | undefined): boolean {
default: return false;
}
}
- return filter('alarms.others');
+ return filter('source.others');
}
function filterEva(p: Property): boolean {
@@ -367,20 +393,51 @@ const Reload = new Dome.Event('ivette.properties.reload');
interface SectionProps {
label: string;
+ prefix?: string;
unfold?: boolean;
children: React.ReactNode;
}
-function Section(props: SectionProps): JSX.Element {
+async function onContextMenu(prefix:string): Promise<void> {
+ const items: Dome.PopupMenuItem[] = [
+ {
+ label: 'Reset to default',
+ onClick: () => resetFilters(prefix),
+ },
+ {
+ label: 'Select all',
+ onClick: () => resetFilters(prefix, true),
+ },
+ {
+ label: 'Deselect all',
+ onClick: () => resetFilters(prefix, false),
+ },
+ ];
+ Dome.popupMenu(items);
+}
+
+function FilterSection(props: SectionProps): JSX.Element {
const settings = `properties-section-${props.label}`;
+ const { label, prefix } = props;
+ const filterButtonProps =
+ prefix ? {
+ icon: 'TUNINGS',
+ title: `Configure filters`,
+ onClick: () => onContextMenu(prefix),
+ } : undefined;
+ const update = Dome.useForceUpdate();
+ Settings.useWindowSettingsEvent(update);
+ const summary = prefix ? filterSummary(prefix) : undefined ;
return (
- <Folder
- label={props.label}
+ <Section
+ label={label}
settings={settings}
defaultUnfold={props.unfold}
+ infos={summary}
+ rightButtonProps={filterButtonProps}
>
{props.children}
- </Folder>
+ </Section>
);
}
@@ -414,7 +471,7 @@ function PropertyFilter(): JSX.Element {
return (
<Scroll>
<CheckField label="Current function" path="currentFunction" />
- <Section label="Status" unfold>
+ <FilterSection label="Status" prefix="status" unfold>
<CheckField label="Valid" path="status.valid" />
<CheckField label="Valid under hyp." path="status.valid_hyp" />
<CheckField label="Unknown" path="status.unknown" />
@@ -424,8 +481,8 @@ function PropertyFilter(): JSX.Element {
<CheckField label="Untried" path="status.untried" />
<CheckField label="Dead" path="status.dead" />
<CheckField label="Inconsistent" path="status.inconsistent" />
- </Section>
- <Section label="Property kind">
+ </FilterSection>
+ <FilterSection label="Property kind" prefix="kind">
<CheckField label="Assertions" path="kind.assert" />
<CheckField label="Invariants" path="kind.invariant" />
<CheckField label="Variants" path="kind.variant" />
@@ -441,12 +498,12 @@ function PropertyFilter(): JSX.Element {
<CheckField label="Pragma" path="kind.pragma" />
<CheckField label="Assumes" path="kind.assumes" />
<CheckField label="Others" path="kind.others" />
- </Section>
- <Section label="Alarms">
- <CheckField label="Alarms" path="alarms.alarms" />
- <CheckField label="Others" path="alarms.others" />
- </Section>
- <Section label="Alarms kind">
+ </FilterSection>
+ <FilterSection label="Source" prefix="source">
+ <CheckField label="Alarms" path="source.alarms" />
+ <CheckField label="Others" path="source.others" />
+ </FilterSection>
+ <FilterSection label="Alarms kind" prefix="alarms">
<CheckField label="Overflows" path="alarms.overflow" />
<CheckField label="Divisions by zero" path="alarms.division_by_zero" />
<CheckField label="Shifts" path="alarms.shift" />
@@ -463,8 +520,8 @@ function PropertyFilter(): JSX.Element {
<CheckField label="Differing blocks" path="alarms.differing_blocks" />
<CheckField label="Separations" path="alarms.separation" />
<CheckField label="Overlaps" path="alarms.overlap" />
- </Section>
- <Section label="Eva">
+ </FilterSection>
+ <FilterSection label="Eva">
<CheckField
label="High-priority only"
path="eva.priority_only"
@@ -480,7 +537,7 @@ function PropertyFilter(): JSX.Element {
path="eva.ctrl_tainted_only"
title="Show only control-tainted properties according to the Eva taint domain"
/>
- </Section>
+ </FilterSection>
</Scroll>
);
}
diff --git a/ivette/src/frama-c/kernel/style.css b/ivette/src/frama-c/kernel/style.css
index 6a7da3a4b4270b277a699419ba5c908199d278a2..d0bb884d976534c1b7e815186ad50d8c66f3d603 100644
--- a/ivette/src/frama-c/kernel/style.css
+++ b/ivette/src/frama-c/kernel/style.css
@@ -56,6 +56,14 @@
/* --- Globals --- */
/* -------------------------------------------------------------------------- */
+.globals-info {
+ color: var(--info-text-discrete);
+ font-style: italic;
+ padding-left: 20px;
+ padding-right: 10px;
+ display: block;
+}
+
.globals-main label {
text-decoration: underline;
}